Lecture Notes in Computer Science 6418 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 MadhuSudan MicrosoftResearch,Cambridge,MA,USA DemetriTerzopoulos UniversityofCalifornia,LosAngeles,CA,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA GerhardWeikum MaxPlanckInstituteforInformatics,Saarbruecken,Germany Howard Barringer Ylies Falcone Bernd Finkbeiner Klaus Havelund Insup Lee Gordon Pace Grigore Ros¸u Oleg Sokolsky Nikolai Tillmann (Eds.) Runtime Verification First International Conference, RV 2010 St. Julians, Malta, November 1-4, 2010 Proceedings 1 3 VolumeEditors HowardBarringer UniversityofManchester,UK,E-mail:[email protected] YliesFalcone IRISA/INRIARennes,France,E-mail:[email protected] BerndFinkbeiner SaarlandUniversity,Saarücken,Germany,E-mail:fi[email protected] KlausHavelund JetPropulsionLaboratory,Pasadena,CA,USA, E-mail:[email protected] InsupLee UniversityofPennsylvania,Philadelphia,PA,USA,E-mail:[email protected] GordonPace UniversityofMalta,Malta,E-mail:[email protected] GrigoreRos¸u UniversityofIllinoisatUrbana-Champaign,Urbana,IL,USA E-mail:[email protected] OlegSokolsky UniversityofPennsylvania,Philadelphia,PA,USA E-mail:[email protected] NikolaiTillmann MicrosoftResearch,Redmond,WA,USA,E-mail:[email protected] LibraryofCongressControlNumber:2010966903 CRSubjectClassification(1998):D.2,F.2,D.2.4,D.1,F.3,D.3 LNCSSublibrary:SL2–ProgrammingandSoftwareEngineering ISSN 0302-9743 ISBN-10 3-642-16611-3SpringerBerlinHeidelbergNewYork ISBN-13 978-3-642-16611-2SpringerBerlinHeidelbergNewYork Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. springer.com ©Springer-VerlagBerlinHeidelberg2010 PrintedinGermany Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper 06/3180 Preface This volume contains the proceedings of the 2010 Runtime Verification confer- ence (RV 2010), which was held in St. Julians, Malta on November 1–4, 2010. The conference program included a mix of invited talks and peer reviewed pre- sentations, tutorials, and tool demonstrations. The 2010 Runtime Verification conference was a forum for researchers and industrial practitioners to presenttheories and tools for monitoring and analyz- ingsystem(softwareandhardware)executions,aswellasaforumforpresenting applicationsofsuchtoolstopracticalproblems.Thefieldofruntimeverification is often referred to under different names, including dynamic analysis, runtime analysis, and runtime monitoring, to mention a few. Runtime verification can be applied during the development of a system for the purpose of program un- derstanding, debugging, and testing, or it can be applied as part of a running system, for example for security or safety policy monitoring, and can further- morebe partofafaultprotectionframework.Anumberofsub-fieldsofruntime verification have emerged over time, such as specification languages and logics for execution analysis, dynamic analysis algorithms, program instrumentation, security monitoring,fault protection, specification mining, and dynamic system visualization.Runtimeverificationhasstrongconnectionstootherfieldsofcom- puter science research, such as combinations of static and dynamic analysis, aspect-oriented programming, and model-based testing. Runtime Verification events started with a workshop in 2001 and continued as an annual workshop series through 2009. The workshops were organized as satellite events to such established forums as CAV (2001–2003,2005–2006,and 2009), ETAPS (2004 and 2008), and AoSD (2007). In 2006, RV was organized jointlywiththe FATESworkshop(FormalAspects ofTesting).Theproceedings forRVfrom2001to2005werepublishedinElectronicNotesinTheoreticalCom- puter Science (ENTCS).Since2006,the RVproceedingshavebeenpublishedin Lecture Notes in Computer Science (LNCS). This year marks an important transition for RV from workshop to a stand- aloneconference.Inthe decadethat haspassedsince the inception ofthe series, the field has matured considerably and a sense of community has emerged. By broadening the event to a conference, we hoped to enlarge the community even further, increasing the visibility of RV events and making submission and par- ticipation more attractive to researchers. As we expected, the change to a conference received a welcome response from the community. RV 2010 received a record number of submissions, ex- ceeding the previous record twofold. Overall, 74 submissions were received, of which 15 were tutorial and tool demonstration proposals. All regular submis- sions were reviewed by the Program Committee, with each paper receiving at leastthreereviews.TheProgramCommitteeselected23papersforpresentation VI Preface at the conference. Tutorial and tool demonstration proposals were evaluated by the respective chairs with the help of external reviewers. Six tutorials and four tool demonstrations were selected. The organizers would like to thank the Program Committee for their hard workinevaluatingthepapers.Financialsupportfortheconferencewasprovided by the International Federation for Computational Logic, by the ARTIST Net- work of Excellence on Embedded Systems Design, by Microsoft Research, and bythe UniversityofIllinois.Wealsowouldliketo thankUniversityofMaltafor the extensive and competent help in handling local organization and providing registrationservices. Submission and evaluation of papers, as well as the prepa- rationofthisproceedingsvolumehasbeenhandledbytheEasyChairconference management service. We hope that the strong program of RV 2010 will provide a focal point for the RV community and foster collaborations with researchers in related fields. August 2010 Howard Barringer Klaus Havelund Insup Lee Grigore Ro¸su Oleg Sokolsky Gordon Pace Bernd Finkbeiner Nikolai Tillmann Ylies Falcone Conference Organization General Chairs Howard Barringer University of Manchester, UK Klaus Havelund NASA/JPL, USA Insup Lee University of Pennsylvania, USA Program Chairs Grigore Ro¸su UniversityofIllinois,Urbana-Champaign,USA Oleg Sokolsky University of Pennsylvania, USA Local Organization Chair Gordon Pace University of Malta, Malta Tutorials Chair Bernd Finkbeiner Saarland University, Germany Tool Demonstrations Chair Nikolai Tillmann Microsoft Research, USA Publicity Chair Ylies Falcone INRIA Rennes, France Program Committee Jamie Andrews University of Western Ontario, Canada Thomas Ball Microsoft Research Redmond, USA Saddek Bensalem Verimag, France Eric Bodden Technical University Darmstadt, Germany Rance Cleaveland University of Maryland, USA Mads Dam KTH, Sweden Matthew Dwyer University of Nebraska, USA Bernd Finkbeiner Saarland University, Germany Cormac Flanagan University of California at Santa Cruz, USA VIII Conference Organization Patrice Godefroid Microsoft Research Redmond, USA Jean Goubault-Larrecq ENS Cachan, France Susanne Graf Verimag, France Radu Grosu State University of New York at Stony Brook, USA Lars Grunske Swinburne University of Technology, Australia Rajiv Gupta University of California at Riverside, USA John Hatcliff Kansas State University, USA Mats Heimdahl University of Minnesota, USA Sarfraz Khurshid University of Texas at Austin, USA Kim Larsen Aalborg University, Denmark Martin Leucker Technical University Muenchen, Germany Paul Miner NASA Langley, USA Greg Morrisett Harvard University, USA Brian Nielsen Aalborg University, Denmark Klaus Ostermann University of Marburg, Germany Corina Pasareanu NASA Ames Research Center, USA Doron Peled Bar Ilan University, Israel Martin Rinard Massachussets Institute of Technology, USA Wolfram Schulte Microsoft Research Redmond, USA Koushik Sen University of California at Berkeley, USA Peter Sestoft University of Copenhagen, Denmark Scott Smolka State University of New York at Stony Brook, USA Serdar Tasiran Koc University, Turkey Shmuel Ur IBM Haifa Research Laboratory,Israel Willem Visser University of Stellenbosch, South Africa Mahesh Viswanathan University of Illinois at Urbana-Champaign, USA Brian Williams MIT, USA External Reviewers Ayman Amin Reinhold Heckmann Andrea Avancini Xiaowan Huang Marina Biberstein Pallavi Joshi Benedikt Bollig Lars Kuhtz Elie Bursztein Axel Legay Christoph Csallner Gurvan Le Guernic Ru¨diger Ehlers Jay Ligatti Tayfun Elmas Changhui Lin Peter Faymonville Nicolas Markey Min Feng Brink van der Merwe Jaco Geldenhuys Marius Mikuˇcionis Alexander Gruler Petur Olsen Conference Organization IX Chang-Seo Park Nadia Tawbi Suzette Person Suresh Thummalapenta Pavithra Prabhakar Chen Tian Kishore Pusukuri Margus Veanes Anders P. Ravn Tomas Vojnar Christian Schallhart Yan Wang Justin Seyster Tao Xie Ali Sezgin Razieh Zaeem Junaid Siddiqui Pengcheng Zhang Emmanuel Sifakis Table of Contents I. Invited Papers Automatic Requirement Extraction from Test Cases.................. 1 Chris Ackermann, Rance Cleaveland, Samuel Huang, Arnab Ray, Charles Shelton, and Elizabeth Latronico Code Contracts for .NET: Runtime Verification and So Much More .... 16 Mike Barnett Visual Debugging for Stream Processing Applications................. 18 Wim De Pauw, Mihai Le¸tia, Bu˘gra Gedik, Henrique Andrade, Andy Frenkiel, Michael Pfeifer, and Daby Sow Runtime Verification in Context: Can Optimizing Error Detection Improve Fault Diagnosis? ......................................... 36 Matthew B. Dwyer, Rahul Purandare, and Suzette Person Contracts for Scala............................................... 51 Martin Odersky Runtime Analysis and Instrumentation for Securing Software (Abstract) .............................................. 58 R. Sekar II. Tutorials Run-Time Verification of Networked Software........................ 59 Cyrille Valentin Artho Clara: Partially Evaluating Runtime Monitors at Compile Time: Tutorial Supplement ............................................. 74 Eric Bodden and Patrick Lam You Should Better Enforce Than Verify............................. 89 Yli`es Falcone Runtime Verification for the Web: A Tutorial Introduction to Interface Contracts in Web Applications .................................... 106 Sylvain Hall´e and Roger Villemaire Statistical Model Checking: An Overview ........................... 122 Axel Legay, Benoˆıt Delahaye, and Saddek Bensalem Runtime Verification with the RV System ........................... 136 Patrick Meredith and Grigore Ro¸su