Saddek Bensalem Yassine Lakhneck Axel Legay (Eds.) t f i r h c s t s e F From Programs 5 to Systems 1 4 8 S C N The Systems Perspective in Computing L ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis Grenoble, France, April 6, 2014 Proceedings 123 Lecture Notes in Computer Science 8415 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard DavidHutchison LancasterUniversity,UK TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA AlfredKobsa UniversityofCalifornia,Irvine,CA,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen TUDortmundUniversity,Germany DemetriTerzopoulos UniversityofCalifornia,LosAngeles,CA,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA GerhardWeikum MaxPlanckInstituteforInformatics,Saarbruecken,Germany Saddek Bensalem Yassine Lakhneck Axel Legay (Eds.) From Programs to Systems The Systems Perspective in Computing ETAPS Workshop, FPS 2014 in Honor of Joseph Sifakis Grenoble, France, April 6, 2014 Proceedings 1 3 VolumeEditors SaddekBensalem UniversityJosephFourier,VerimagLaboratory VerimagCentreÉquation 2,avenuedeVignate,38610Gières,France E-mail:[email protected] YassineLakhneck UniversityJosephFourier,VerimagLaboratory VerimagCentreÉquation 2,avenuedeVignate,38610Gières,France E-mail:[email protected] AxelLegay Inria,CampusUniversitairedeBeaulieu 35042RennesCedex,France E-mail:[email protected] Coverillustration:GerhardIllig,PLAKKADIVEN:Apan LicensedundertheCreativeCommonsAttribution-ShareAlike3.0Unported (//creativecommons.org/licenses/by-sa/3.0/deed.en)license. ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-54847-5 e-ISBN978-3-642-54848-2 DOI10.1007/978-3-642-54848-2 SpringerHeidelbergNewYorkDordrechtLondon LibraryofCongressControlNumber:2014933961 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ©Springer-VerlagBerlinHeidelberg2014 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartof thematerialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation, broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,andtransmissionorinformation storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodology nowknownorhereafterdeveloped.Exemptedfromthislegalreservationarebriefexcerptsinconnection withreviewsorscholarlyanalysisormaterialsuppliedspecificallyforthepurposeofbeingenteredand executedonacomputersystem,forexclusiveusebythepurchaserofthework.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheCopyrightLawofthePublisher’slocation, inistcurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Permissionsforuse maybeobtainedthroughRightsLinkattheCopyrightClearanceCenter.Violationsareliabletoprosecution undertherespectiveCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Whiletheadviceandinformationinthisbookarebelievedtobetrueandaccurateatthedateofpublication, neithertheauthorsnortheeditorsnorthepublishercanacceptanylegalresponsibilityforanyerrorsor omissionsthatmaybemade.Thepublishermakesnowarranty,expressorimplied,withrespecttothe materialcontainedherein. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Joseph Sifakis Preface This group of papers represents the proceedings of the “From Programs to Systems – The Systems Perspective in Computing” workshop (FPS 2014). The workshop was held in honor of Professor Joseph Sifakis in the framework of the 16th European Joint Conferences on Theory and Practice of Software in Grenoble, April 6th, 2014. Theworkshopprovidedaforumforresearchersandpractitionersfromacademia and industry to share their work, exchange ideas, and discuss the future direc- tions on a systems perspective in computing. Over the past decades, the focus of computing has been continuously shifting from programs to systems. Pro- grams can be represented as relations independent from the physical resources needed for their execution. Their behavior is often terminating, deterministic and platform-independent. On the contrary, systems are interactive. They con- tinuously interact with an external environment. Their behavior is driven by stimuli from the environment, which, in turn, is affected by their outputs. Systems are inherently complex and hard to design owing to unpredictable and subtle interactions with their environment, emergent behaviors, and oc- casional catastrophic cascading failures, rather than to complex data and al- gorithms. Compared to function software, their complexity is exacerbated by additional factors such as concurrent execution, uncertainty resulting from in- teractionwithunpredictableenvironments,heterogeneityofinteractionbetween hardwareand software, and nonrobustness (small variations in a certain part of the system can have large effects on overall system behavior). Theory of computation is, by its very nature, of little help for studying sys- tems.Evenifweperfectlyunderstandthepropertiesofaprogramandtheprop- erties of a hardware target platform, we have no theory to predict the behavior of the program running on the platform. FPS addresses the two following issues: Extending programing theory to systems (i)Towhatextentcanformaltechniquesforsoftwaredevelopmentbeadapted/ extended to system development? – Programcorrectness vs. system correctness; – Adapting SW engineering techniques to systems engineering; – Software modeling vs. system modeling; – How software verification techniques can be adapted to deal with quantita- tive properties? (ii) Foundations for system design – Missingresults(theory,methodsandtools)enablingrigoroussystemdesign; – Building faithful system models; VIII Preface – Adaptive resources management – Mixed criticality systems; – Design space exploration; – Automated implementation techniques for distributed or many-core platforms. JosephSifakisisaprofessorandthedirectoroftheRigorousSystemDesignLab- oratoryatEPFL.Hisworkischaracterizedbyanunusualrecurrentpattern:the problemisfirststudiedfromanabstract,foundationalpointofview,whichleads to methods and techniques for its solution, which, in turn, leads to an effective implementation that is successfully used in multiple industrial applications. Joseph Sifakis studied Electrical Engineering at the National Technical Uni- versityinGreece.Asastudenthewasinclinedtobemoreconcernedwiththeory thanwithpractice.HecametoGrenoblein1970forgraduatestudiesinPhysics. An encounter was decisive for his career: he met Professor Jean Kuntzmann, who was the Director of the Institute of Informatics and Applied Mathematics (IMAG). Joseph Sifakis interest in Computing grew and he decided to quit his studies in Physics and start undergraduate studies at IMAG. He did his Engi- neeringthesis undersupervisionofProfessorJeanKuntzmannonModellingthe timed behavior of circuits. After his Engineering thesis, he became interested in the theory of concurrency. From1974to1977JosephSifakisstudiedPetrinetsandothermodelsforcon- currentsystems.He obtainedoriginalandfundamentalresults onthe structural properties of Petri nets as well as on the performance evaluation of timed Petri nets. These results are extensively used today for scheduling data-flow systems. From 1977 to 1982 he switched his attention to program semantics and ver- ification. Dijkstras papers and books had a deep influence on his work as well as discussions with Michel Sintzoff who was working at that time on program verification. They drew him the idea of fixpoint characterization for temporal modalities, and once again his work yielded original results on the algorithmic verification of concurrent systems based on a fixpoint characterization of the modalitiesofabranchingtime temporallogic.Theseresultslaiddownthe foun- dations of model checking. His student Jean-Pierre Queille developed the first modelcheckerin1982.JosephSifakismetEdClarkeandAllenEmersonatCMU in November 1982 and they realized that they had been working independently on the same problem. In the autumn of 1983, Joseph Sifakis met Amir Pnueli at a workshop on the Analysis of Concurrent Systems, organized in Cambridge. This was the be- ginning of a continuous interaction and collaboration for more than 25 years. Joseph Sifakis and Amir Pnueli setup several European projects in collabora- tion with Willem-Paul de Roever, on system modeling and verification. They jointly organized with Ed Clarke, the Workshop on the Verification of Finite State Systems in Grenoble in 1989.This workshopis consideredas the first edi- tionoftheCAVConference.AmirPnuelifrequentlyvisitedVerimagforoverten years and Verimag researchers greatly benefited from his wisdom and support. Intheperiod1988-2000JosephSifakisextendedhisworktodealwithmodel- ing and verificationof real-time systems and hybrid systems. This included: the Preface IX study of hybrid systems and their verification techniques; the development and implementation of the KRONOS model checker, in collaboration with T. Hen- zinger, the first symbolic model checker for timed automata; the development and implementation of an efficient symbolic synthesis algorithm for timed sys- tems, in collaboration with O. Maler and A. Pnueli; the study of compositional modelingtechniquesforreal-timeschedulingbyusingpriorities.InJanuary1993, Joseph Sifakis founded the Verimag laboratory, a joint-venture between IMAG and Verilog SA. This has been an exciting and fruitful experience. Verimag has transferredthe Lustre languagedesignedby PaulCaspiandNicolasHalbwachs, to the SCADE synchronous programing environment. SCADE is being used by Airbus to develop safety critical systems and has become a de facto standard for aeronautics. SCADE has been qualified as a development tool by the FAA, EASA,andTransportCanadaunderDO-178BuptoLevelA.Itiscurrentlybeen commercializedbyEsterelTechnologies.Verimaghasalsotransferredfunctional testing and verification techniques to the ObjectGeode tool for modeling real- time distributed applications. This tool has been commercialized by Telelogic purchased by IBM in 2008. Since 1997, Verimag has been a public research laboratory, associated with CNRS and the University of Grenoble. It plays a prominent role in embedded systems by producing cutting-edge researchand leading researchinitiatives and projects in Europe. As the director of Verimag, Joseph Sifakis has sought a balance between basic and applied research. He has used resources from indus- trial contracts and collaborativeprojects to develop new researchactivities and strengthen the potential in basic research. For him, participation in industrial projectshasbeenasourceofinspiration.Itallowsthe definitionofnewresearch directions that are scientifically challenging and technically relevant. The virtu- ous cycle of interaction between research and applications has been the key to Verimag success. In the late 90s, Joseph Sifakis research interests progressively shifted from verification and formal methods to system design. He was convinced that for- mal verification was hitting a wall and only incremental improvements in the state-of-the-artcouldbe expected.He steppeddownfromtheSteeringCommit- tee of CAV and started a new research program on embedded systems design. Interactions with colleagues such as Hermann Kopetz, Lothar Thiele, Thomas Henzinger,AlbertoSangiovanniVincentelliandEdwardLee,contributedtoelab- orating a system perspective for Computing. He worked actively for setting up the Emsoft Conference and for organizing the Embedded Systems community inEuropethroughthe ArtistCoordinationMeasurefollowedbythe Artist2and ArtistDesign European Networks of Excellence. During this later period Joseph Sifakis has also played a leading role in the developmentand implementation ofthe BIP componentframeworkfor rigorous system design. The implementation consists of a language and a set of tools including source-to-source transformers, a compiler and the D-Finder tool for compositional verification. BIP is unique for its expressiveness. It can describe mixedhardware/softwaresystems.Itusesasmallandpowerfulsetofprimitives X Preface encompassing a general concept of system architecture. BIP was successfully used in several industrial projects, in particular for the componentization of legacysoftwareandthe automatic generationof implementations for many-core platforms. Joseph Sifakis is an active and visionary researcher in the area of system design.Hebelievesthatendowingdesignwithscientificfoundationsisatleastof equal importance as the quest for scientific truth in natural sciences. As one of hisclosecollaborators,Ihaveconstantlybenefitedfromhisadviceandguidance. I wish Joseph a long and productive career as a researcher and intellectual. DISTINCTIONS AND HONORS Turing Award 2007 Silver Medal of CNRS, 2001 Leonardo da Vinci Medal 2012 Grand Officer of the National Order of Merit, France, 2008 Commander of the Legion of Honnour, France, 2011 Award of the Greek Parliament for Commonwealth and Democracy, 2010 Commander of the Order of the Phoenix, Greece 2013 Award of the Town of Grenoble, 2008 Member of the French Academy of Sciences, 2010 Member of Academia Europea, 2008 Member of the French Academy of Engineering, 2008 Doctor Honoris Causa: EPFL, University of Athens, International Hellenic University Honorary Professor: University of Patras April 2014 Saddek Bensalem Yassine Lakhnech Axel Legay Table of Contents Model-Driven Information Flow Security for Component-Based Systems ........................................................ 1 Najah Ben Said, Takoua Abdellatif, Saddek Bensalem, and Marius Bozga Context-Bounded Analysis of TSO Systems ......................... 21 Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato A Model of Dynamic Systems ..................................... 39 Manfred Broy From Hierarchical BIP to Petri Calculus ............................ 54 Roberto Bruni, Herna´n Melgratti, and Ugo Montanari Programming and Verifying Component Ensembles................... 69 Rocco De Nicola, Alberto Lluch Lafuente, Michele Loreti, Andrea Morichetta, Rosario Pugliese, Valerio Senni, and Francesco Tiezzi Parametric and Quantitative Extensions of Modal Transition Systems ........................................................ 84 Uli Fahrenberg, Kim Guldstrand Larsen, Axel Legay, and Louis-Marie Traonouez Specification Theories for Probabilistic and Real-Time Systems ........ 98 Uli Fahrenberg, Axel Legay, and Louis-Marie Traonouez Compositional Branching-Time Measurements ....................... 118 Radu Grosu, Doron Peled, C.R. Ramakrishnan, Scott A. Smolka, Scott D. Stoller, and Junxing Yang Steps towards Scenario-Based Programming with a Natural Language Interface........................................................ 129 Michal Gordon and David Harel Assembly Theories for Communication-Safe Component Systems....... 145 Rolf Hennicker, Alexander Knapp, and Martin Wirsing Constructive Collisions ........................................... 161 Edward A. Lee