Mehdi Dastani Marjan Sirjani (Eds.) 2 9 Fundamentals 3 9 S C of Software Engineering N L 6th International Conference, FSEN 2015 Tehran, Iran, April 22–24, 2015 Revised Selected Papers 123 Lecture Notes in Computer Science 9392 Commenced Publication in 1973 Founding and Former Series Editors: Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen EditorialBoard David Hutchison Lancaster University, Lancaster, UK Takeo Kanade Carnegie Mellon University, Pittsburgh, PA, USA Josef Kittler University of Surrey, Guildford, UK Jon M. Kleinberg Cornell University, Ithaca, NY, USA Friedemann Mattern ETH Zürich, Zürich, Switzerland John C. Mitchell Stanford University, Stanford, CA, USA Moni Naor Weizmann Institute of Science, Rehovot, Israel C. Pandu Rangan Indian Institute of Technology, Madras, India Bernhard Steffen TU Dortmund University, Dortmund, Germany Demetri Terzopoulos University of California, Los Angeles, CA, USA Doug Tygar University of California, Berkeley, CA, USA Gerhard Weikum Max Planck Institute for Informatics, Saarbrücken, Germany Moreinformationaboutthisseriesathttp://www.springer.com/series/7408 · Mehdi Dastani Marjan Sirjani (Eds.) Fundamentals of Software Engineering 6th International Conference, FSEN 2015 Tehran, Iran, April 22–24, 2015 Revised Selected Papers ABC Editors MehdiDastani MarjanSirjani IntelligentSystems SchoolofComputerScience UtrechtUniversity ReykjavikUniversity Utrecht Reykjavik TheNetherlands Iceland ISSN0302-9743 ISSN1611-3349 (electronic) LectureNotesinComputerScience ISBN978-3-319-24643-7 ISBN978-3-319-24644-4 (eBook) DOI10.1007/978-3-319-24644-4 LibraryofCongressControlNumber:2015949443 LNCSSublibrary:SL2–ProgrammingandSoftwareEngineering SpringerChamHeidelbergNewYorkDordrechtLondon (cid:2)c IFIPInternationalFederationforInformationProcessing2015 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartofthe materialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation,broad- casting,reproduction onmicrofilmsorinanyotherphysicalway,andtransmissionorinformationstorage andretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodologynowknown orhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher, theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbook arebelievedtobetrueandaccurateatthedateofpublication. Neitherthepublishernortheauthorsorthe editorsgiveawarranty,expressorimplied,withrespecttothematerialcontainedhereinorforanyerrorsor omissionsthatmayhavebeenmade. Printedonacid-freepaper SpringerInternationalPublishingAGSwitzerlandispartofSpringerScience+BusinessMedia (www.springer.com) Preface The present volume contains the proceedings of the sixth IPM International Conference on Fundamentals of Software Engineering (FSEN), held in Tehran, Iran, April 22–24,2015.This event, FSEN 2015,wasorganizedby the Schoolof Computer Science at the Institute for Researchin Fundamental Sciences (IPM) in Iran, in cooperation with ACM SIGSOFT and IFIP WG 2.2. The topics of interest span all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry andpromotingtheirintegrationwithpracticalengineeringtechniques.ThePro- gramCommittee ofFSEN2015consistedof46topresearchersfrom38different academic institutes in 17 countries. We received a total of 62 submissions from 22countriesoutofwhichwehaveaccepted14regularpapers,5shortpapersand 6 posters. Each submission was reviewed by at least 3 independent referees, for its quality, originality, contribution, clarity of presentation, and its relevance to the conference topics. These proceedings include the regular and short papers, as well as two papers by the invited speakers. Three distinguished keynote speakers delivered their lectures at FSEN 2015. PaolaInverardigaveatalkon“AutomatedIntegrationofService-OrientedSoft- ware Systems”, Holger Giese presentedhis work on “TowardsSmart Systems of Systems”,andJohnHughesgaveapresentationon“ExperienceswithProperty- Based Testing: Testing the Hard Stuff and Staying Sane.” WethanktheInstituteforResearchinFundamentalSciences(IPM),Tehran, Iran for their financial support and local organization of FSEN 2015. We also thank the members of the Program Committee for their time, effort, and ex- cellent contributions to making FSEN a quality conference. We thank Hossein Hojjatforhishelpinpreparingthisvolume.Lastbutnotleast,ourthanksgoto the authors and conference participants, without whom FSEN 2015 would not have been possible. July 2015 Mehdi Dastani Marjan Sirjani Organization Program Committee Mohammad Abdollahi Azgomi IranUniversityofScienceandTechnology,Iran Gul Agha University of Illinois at Urbana-Champaign, USA Christel Baier Technical University of Dresden, Germany Ezio Bartocci Vienna University of Technology, Austria Borzoo Bonakdarpour McMaster University, Canada Marcello Bonsangue Leiden University, Netherlands Mario Bravetti University of Bologna, Italy Michael Butler University of Southampton, UK Fabiano Dalpiaz Utrecht University, Netherlands Mehdi Dastani Utrecht University, Netherlands Frank De Boer CWI, Netherlands Erik De Vink Technische Universiteit Eindhoven, Netherlands Klaus Dr¨ager Oxford University, UK Wan Fokkink Vrije Universiteit Amsterdam, Netherlands Masahiro Fujita University of Tokyo, Japan Maurizio Gabbrielli University of Bologna, Italy Fatemeh Ghassemi University of Tehran, Iran Jan Friso Groote Eindhoven University of Technology, Netherlands Kim Guldstrand Larsen Aalborg University, Denmark Hassan Haghighi Shahid Beheshti University, Iran Holger Hermanns Saarland University, Germany Hossein Hojjat Cornell University, USA Mohammad Izadi Sharif University of Technology, Iran Mohammad Mahdi Jaghoori CWI, Netherlands Einar Broch Johnsen University of Oslo, Norway Joost-Pieter Katoen RWTH Aachen University, Germany Narges Khakpour KTH Royal Institute of Technology, Sweden Ramtin Khosravi University of Tehran, Iran Zhiming Liu Birmingham City University, UK Jose Meseguer University of Illinois at Urbana-Champaign, USA Hassan Mirian-Hosseinabadi Sharif University of Technology, Iran Ugo Montanari Universita` di Pisa, Italy VIII Organization Peter Mosses Swansea University, UK Mohammadreza Mousavi Halmstad University, Sweden Ali Movaghar Sharif University of Technology, Iran Peter Olveczky University of Oslo, Norway Jose Proenca Katholieke Universiteit Leuven, Belgium Niloofar Razavi University of Toronto, Canada Wolfgang Reisig Humboldt-Universit¨at zu Berlin, Germany Philipp Ruemmer Uppsala University, Sweden Gwen Salau¨n INRIA Grenoble, France Cesar Sanchez IMDEA Software Institute, Spain Wendelin Serwe INRIA Grenoble, France Marjan Sirjani Reykjavik University, Iceland Meng Sun Peking University, China Carolyn Talcott SRI International, USA Samira Tasharofi University of Illinois at Urbana-Champaign, USA Tayssir Touili CNRS, LIPN, France Danny Weyns Linnaeus University, Sweden Additional Reviewers Aflaki, Saba Li, Xiaoshan Amini, Morteza Mafi, Zohreh Azadbakht, Keyvan Mashayekhi, Hoda Bartocci, Ezio Mauro, Jacopo Beohar, Harsh Melgratti, Hernan Boudjadar, Jalil Moelle, Andre Bruni, Roberto Motallebi, Hassan Bucchiarone, Antonio Nooraee, Maryam Dalvandi, Mohammadsadegh Nyman, Ulrik Dan, Li Petre, Luigia Devismes, St´ephane Sammartino, Matteo Din, Crystal Chang Savicks, Vitaly Entezari Maleki, Reza Schlatte, Rudolf Evans, Cain Serbanescu, Vlad Nicolae Fernandez Anta, Antonio Su¨rmeli, Jan Giallorenzo, Saverio Talebi, Mahmoud Helvensteijn, Michiel Tapia Tarifa, Silvia Lizeth Heydarnoori, Abbas Varshosaz, Mahsa Jensen, Peter Gjøl Vignudelli, Valeria Keramati, Hossein V¨ollinger, Kim Keshishzadeh, Sarmen Ye, Lina Klein, Joachim Zelji´c, Aleksandar Klueppelholz, Sascha Contents Towards Smart Systems of Systems ................................ 1 Holger Giese, Thomas Vogel, and Sebastian Wa¨tzoldt Automated Integration of Service-Oriented Software Systems .......... 30 Marco Autili, Paola Inverardi, and Massimo Tivoli Software Architecture Modeling and Evaluation Based on Stochastic Activity Networks................................................ 46 Ali Sedaghatbaf and Mohammad Abdolahi Azgomi Applicative Bisimulation and Quantum λ-Calculi .................... 54 Ugo Dal Lago and Alessandro Rioli Modeling and Efficient Verification of Broadcasting Actors ............ 69 Behnaz Yousefi, Fatemeh Ghassemi, and Ramtin Khosravi A Theory of Integrating Tamper Evidence with Stabilization .......... 84 Reza Hajisheykhi, Ali Ebnenasir, and Sandeep S. Kulkarni A Safe Stopping Protocol to Enable Reliable Reconfiguration for Component-Based Distributed Systems ............................. 100 Mohammad Ghafari, Abbas Heydarnoori, and Hassan Haghighi Efficient Architecture-Level Configuration of Large-Scale Embedded Software Systems ................................................ 110 Razieh Behjati and Shiva Nejati Benchmarks for Parity Games ..................................... 127 Jeroen J.A. Keiren A Behavioural Theory for a π-calculus with Preorders ................ 143 Daniel Hirschkoff, Jean-Marie Madiot, and Xian Xu Incremental Realization of Safety Requirements: Non-determinism vs. Modularity...................................................... 159 Ali Ebnenasir Analyzing Mutable Checkpointing via Invariants ..................... 176 Deepanker Aggarwal and Astrid Kiehn High Performance Computing Applications Using Parallel Data Processing Units ................................................. 191 Keyvan Azadbakht, Vlad Serbanescu, and Frank de Boer Improved Iterative Methods for Verifying Markov Decision Processes ... 207 Jaber Karimpour, Ayaz Isazadeh, MohammadSadegh Mohagheghi, and Khayyam Salehi X Contents A Pre-congruence Format for XY-simulation ........................ 215 Harsh Beohar and Mohammad Reza Mousavi Tooled Process for Early Validation of SysML Models Using Modelica Simulation ...................................................... 230 Jean-Marie Gauthier, Fabrice Bouquet, Ahmed Hammad, and Fabien Peureux Can High Throughput Atone for High Latency in Compiler-Generated Protocol Code? .................................................. 238 Sung-Shik T.Q. Jongmans and Farhad Arbab Painless Support for Static and Runtime Verification of Component- Based Applications............................................... 259 Nuno Gaspar, Ludovic Henrio, and Eric Madelaine Linear Evolution of Domain Architecture in Service-Oriented Software Product Lines ................................................... 275 Sedigheh Khoshnevis and Fereidoon Shams An Interval-Based Approach to Modelling Time in Event-B ........... 292 Gintautas Sulskus, Michael Poppleton, and Abdolbaghi Rezazadeh From Event-B Models to Dafny Code Contracts ..................... 308 Mohammadsadegh Dalvandi, Michael Butler, and Abdolbaghi Rezazadeh Author Index.................................................. 317