Lecture Notes in Computer Science 7226 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 Alwyn E. Goodloe Suzette Person (Eds.) NASA Formal Methods 4th International Symposium, NFM 2012 Norfolk, VA, USA, April 3-5, 2012 Proceedings 1 3 VolumeEditors AlwynE.Goodloe SuzettePerson NASALangleyResearchCenter MS130,HamptonVA23681,USA E-mail:{a.goodloe,suzette.person}@nasa.gov ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-28890-6 e-ISBN978-3-642-28891-3 DOI10.1007/978-3-642-28891-3 SpringerHeidelbergDordrechtLondonNewYork LibraryofCongressControlNumber:2012933117 CRSubjectClassification(1998):D.2.4,D.2,D.3,F.3,D.1 LNCSSublibrary:SL2–ProgrammingandSoftwareEngineering ©Springer-VerlagBerlinHeidelberg2012 Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply, evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevantprotectivelaws andregulationsandthereforefreeforgeneraluse. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Preface This publication contains the proceedings of the 4th NASA Formal Methods Symposium(NFM2012),heldApril3–5,2012,inNorfolk,VA,USA.TheNASA Formal Method Symposium is a forum for theoreticians and practitioners from academia,industry,andgovernment,with the goalof identifying challengesand providing solutions to achieving assurance in mission- and safety-critical sys- tems. Within NASA, for example, such systems include autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transporta- tion(NextGen),andautonomousrendezvousanddockingforspacecraft.Rapidly increasingcodesizeandemergingparadigms,suchasautomatedcodegeneration andsafetycases,bringnewchallengesandopportunitiesforsignificantimprove- ment. Also gaining increasing importance in NASA applications is the use of more rigorous software test methods and code analysis techniques, founded in theory. The focus of the symposium is understandably on formal methods, their foundation, current capabilities, as well as their current limitations. The NASA FormalMethodsSymposiumisanannualeventthatwascreatedtohighlightthe state of the art in formal methods, both in theory and practice. The series was originallystartedastheLangleyFormalMethodsWorkshop,andwasheldunder that name in 1990, 1992, 1995, 1997, 2000, and 2008. In 2009, the first NASA Formal Methods Symposium was organized by NASA Ames Research Center, and took place at Moffett Field, CA. This year, the symposium was organized by NASA Langley Research Center, and held in Norfolk, VA. The topics covered by NFM 2012 included but were not limited to: theorem proving, symbolic execution, model-based engineering, real-time and stochastic systems,modelchecking,abstractionand abstractionrefinement,compositional verificationtechniques,staticanddynamicanalysistechniques,faultprotection, cyber security,specification formalisms,requirements analysis,and applications of formal techniques. Two types of papers were considered: regular papers describing fully devel- oped work and complete results or case studies, and short papers describing tools,experience reports,and workin progressor preliminaryresults. The sym- posiumreceived93submissions(66regularpapersand27shortpapers),ofwhich the committee selected 36 papers (26 regular papers and 10 short papers). All submissions went through a rigorous review process. In addition to the refereed papers, the symposium featured three invited talks and a panel session. The invited talks were presented by Andrew Appel from Princeton University, on “Verified Software Toolchain,” Patrick Cousot from E´cole Normale Sup´erieure, Paris, and New York University, on “Formal Verification by Abstract Interpretation,” and Cesare Tinelli from the Univer- sity of Iowa, on “SMT-Based Model Checking.” The panel, composed of Mike VI Preface Lowry(NASA Ames), Klaus Havelund(NASA/JPL), and Ricky Butler (NASA Langley), discussed the history and current application of formal methods at NASA. The organizersaregratefulto the authorsforsubmitting their workto NFM 2012 and to the invited speakers for sharing their insights. NFM 2012 would not have been possible without the collaboration of the Steering Committee, Program Committee, and external reviewers, and the general support of the NASA Formal Methods community. Special thanks go to Raymond Meyer for the graphical design of NFM 2012 visual material and the NFM 2012 website, which can be found at http://shemesh.larc.nasa.gov/nfm2012/index.html. January 2012 Alwyn Goodloe Suzette Person Organization Program Committee Nikolaj Bjorner Microsoft Research, USA Jonathan P. Bowen Museophile Limited, UK Julia Braman NASA- Johnson Space Center, USA Ricky Butler NASA Langley Research Center, USA Rance Cleaveland University of Maryland, USA Darren Cofer Rockwell Collins, USA Ewen Denney SGT/NASA Ames, USA Dino Distefano Queen Mary, University of London, UK Jin Song Dong National University of Singapore, Singapore Jean-Christophe Filliatre CNRS, France Dimitra Giannakopoulou NASA Ames, USA Alwyn Goodloe NASA Langley Research Center, USA Eric Goubault CEA/Saclay, France George Hagen NASA Langley Research Center, USA John Hatcliff Kansas State University, USA Klaus Havelund Jet PropulsionLaboratory,California Institute of Technology, USA Mats Heimdahl University of Minnesota, USA Gerard Holzmann JPL, USA Joe Hurd Galois, Inc., USA Bart Jacobs Katholieke Universiteit Leuven, Belgium Ken Mcmillan Cadence Berkeley Labs, USA Eric Mercer Brigham Young University, USA Cesar Munoz National Aeronautics and Space Administration, USA Anthony Narkawicz NASA Langley, USA Natasha Neogi National Institute of Aerospace, USA Corina Pasareanu CMU/NASA Ames Research Center, USA Charles Pecheur UC Louvain, Belgium Suzette Person NASA Langley Research Center, USA Kristin Yvonne Rozier NASA Ames Research Center, USA Natarajan Shankar SRI International, USA Oleg Sokolsky University of Pennsylvania, USA Sofiene Tahar Concordia University, USA Oksana Tkachuk Fujitsu Laboratories of America Willem Visser Stellenbosch University, South Africa Michael Whalen University of Minnesota, USA Virginie Wiels ONERA / DTIM, France Jim Woodcock University of York, UK VIII Organization Additional Reviewers Ancona, Davide Liu, Liya Aridhi, Henda Mahboubi, Assia Ayoub, Anaheed Mhamdi, Tarek Belt, Jason Miller, Sheena Beringer, Lennart Miner, Paul Bouissou, Olivier Mullier, Olivier Brotherston, James Namjoshi, Kedar Busard, Simon Owre, Sam Combefis, Sebastien Pai, Ganesh Cruanes, Simon Paskevich, Andrei Cuoq, Pascal Rocha, Camilo Denman, William Rozier, Eric Di Vito, Ben Rungta, Neha Dubreil, Jeremy Sana´n, David Florian, Mihai Schrammel, Peter Gawanmeh, Amjad Shi, Ling Gui, Lin Siminiceanu, Radu Haucourt, Emmanuel Smans, Jan Holloway,C. Michael Song, Songzheng Jourdan, Jacques-Henri Spitters, Bas Khan-Afshar, Sanaz Tan, Tian Huat King, Andrew Vanoverberghe, Dries Le Gall, Tristan Wang, Shaohui Lemay, Michael Zhang, Shaojie Leslie, Rebekah Zheng, Manchun Table of Contents SMT-Based Model Checking ...................................... 1 Cesare Tinelli Verified Software Toolchain (Abstract).............................. 2 Andrew W. Appel Formal Verification by Abstract Interpretation....................... 3 Patrick Cousot Quantitative Timed Analysis of Interactive Markov Chains............ 8 Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuha¨ußer Lessons Learnt from the Adoption of Formal Model-Based Development .................................................... 24 Alessio Ferrari, Alessandro Fantechi, and Stefania Gnesi Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines ......................................... 39 Karolina Zurowska and Juergen Dingel Inferring Definite Counterexamples through Under-Approximation ..... 54 J¨org Brauer and Axel Simon Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging............................................. 70 Ross Gore and Paul F. Reynolds Jr. Rigorous PolynomialApproximation Using Taylor Models in COQ ..... 85 Nicolas Brisebarre, Mioara Jolde¸s, E´rik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pa¸sca, Laurence Rideau, and Laurent Th´ery Enhancing the Inverse Method with State Merging ................... 100 E´tienne Andr´e, Laurent Fribourg, and Romain Soulat Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages ....................................... 106 Alexander Herz and Kalmer Apinis Testing Static Analyzers with Randomly Generated Programs ......... 120 Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, and Xuejun Yang X Table of Contents Compositional Verification of Architectural Models................... 126 Darren Cofer, Andrew Gacek, Steven Miller, Michael W. Whalen, Brian LaValley, and Lui Sha A Safety Case Pattern for Model-Based Development Approach........ 141 Anaheed Ayoub, Baek-Gyu Kim, Insup Lee, and Oleg Sokolsky PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL ........................................... 147 Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Lo¨ıc Garoche, Eric Feron, Gilberto Perez, and Pablo Ascariz Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements (Preliminary Results)............................................. 162 Wenbin Li, Jane Huffman Hayes, and Mirosl(cid:3)aw Truszczyn´ski Some Steps into Verification of Exact Real Arithmetic ................ 168 Norbert Th. Mu¨ller and Christian Uhrhan Runtime Verification Meets Android Security........................ 174 Andreas Bauer, Jan-Christoph Ku¨ster, and Gil Vegliach Specification in PDL with Recursion ............................... 181 Xinxin Liu and Bingtian Xue Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study .................................. 195 Aditi Tagore, Diego Zaccai, and Bruce W. Weide Sound Formal Verification of Linux’s USB BP Keyboard Driver........ 210 Willem Penninckx, Jan Tobias Mu¨hlberg, Jan Smans, Bart Jacobs, and Frank Piessens Learning Markov Models for Stationary System Behaviors............. 216 Yingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen, Kim Guldstrand Larsen, and Brian Nielsen The Use of Rippling to Automate Event-B Invariant Preservation Proofs.......................................................... 231 Yuhui Lin, Alan Bundy, and Gudmund Grov Thread-Modular Model Checking with Iterative Refinement ........... 237 Wenrui Meng, Fei He, Bow-Yaw Wang, and Qiang Liu