Formal Methods for Industrial Critical Systems

STEFANIA GNESI is Director of Research and head of the Formal Methods and Tools Laboratory at ISTI-CNR (Istituto di Scienza e Tecnologie dell'Informazione-Consiglio Nazionale delle Ricerche) in Pisa, Italy. She was previously a lecturer in methods and tools for the specification and analysis of software systems at the University of Florence.TIZIANA MARGARIA is Full Professor in the Faculty of Mathematics and Natural Sciences of the University of Potsdam, where she holds the Chair of Service and Software Engineering at the Institute of Informatics. She has held positions at universities in Göttingen, Dortmund, and Passau, Germany, as well as in Sweden and Italy.

• FOREWORD by Mike Hinchey xiiiFOREWORD by Alessandro Fantechi and Pedro Merino xvPREFACE xviiCONTRIBUTORS xixPART I INTRODUCTION AND STATE OF THE ART 11 FORMAL METHODS: APPLYING {LOGICS IN, THEORETICAL} COMPUTER SCIENCE 3Diego Latella1.1 Introduction and State of the Art 31.2 Future Directions 9PART II MODELING PARADIGMS 152 A SYNCHRONOUS LANGUAGE AT WORK: THE STORY OF LUSTRE 17Nicolas Halbwachs2.1 Introduction 172.2 A Flavor of the Language 182.3 The Design and Development of Lustre and Scade 202.4 Some Lessons from Industrial Use 252.5 And Now . . . 283 REQUIREMENTS OF AN INTEGRATED FORMAL METHOD FOR INTELLIGENT SWARMS 33Mike Hinchey, James L. Rash, Christopher A. Rouff, Walt F. Truszkowski, and Amy K.C.S. Vanderbilt3.1 Introduction 333.2 Swarm Technologies 353.3 NASA FAST Project 393.4 Integrated Swarm Formal Method 413.5 Conclusion 55PART III TRANSPORTATION SYSTEMS 614 SOME TRENDS IN FORMAL METHODS APPLICATIONS TO RAILWAY SIGNALING 63Alessandro Fantechi, Wan Fokkink, and Angelo Morzenti4.1 Introduction 634.2 CENELEC Guidelines 654.3 Software Procurement in Railway Signaling 664.4 A Success Story: The B Method 704.5 Classes of Railway Signaling Equipment 714.6 Conclusions 805 SYMBOLIC MODEL CHECKING FOR AVIONICS 85Radu I. Siminiceanu and Gianfranco Ciardo5.1 Introduction 855.2 Application: The Runway Safety Monitor 875.3 A Discrete Model of RSM 955.4 Discussion 107PART IV TELECOMMUNICATIONS 1136 APPLYING FORMAL METHODS TO TELECOMMUNICATION SERVICES WITH ACTIVE NETWORKS 115María del Mar Gallardo, Jesús Martínez, and Pedro Merino6.1 Overview 1156.2 Active Networks 1166.3 The Capsule Approach 1176.4 Previous Approaches on Analyzing Active Networks 1186.5 Model Checking Active Networks with SPIN 1226.6 Conclusions 1297 PRACTICAL APPLICATIONS OF PROBABILISTIC MODEL CHECKING TO COMMUNICATION PROTOCOLS 133Marie Dufl ot, Marta Kwiatkowska, Gethin Norman, David Parker, Sylvain Peyronnet, Claudine Picaronny, and Jeremy Sproston7.1 Introduction 1337.2 PTAs 1347.3 Probabilistic Model Checking 1367.4 Case Study: CSMA/CD 1397.5 Discussion and Conclusion 146PART V INTERNET AND ONLINE SERVICES 1518 DESIGN FOR VERIFIABILITY: THE OCS CASE STUDY 153Johannes Neubauer, Tiziana Margaria, and Bernhard Steffen8.1 Introduction 1538.2 The User Model 1558.3 The Models and the Framework 1588.4 Model Checking 1598.5 Validating Emerging Global Behavior via Automata Learning 1618.6 Related Work 1708.7 Conclusion and Perspectives 1739 AN APPLICATION OF STOCHASTIC MODEL CHECKING IN THE INDUSTRY: USER-CENTERED MODELING AND ANALYSIS OF COLLABORATION IN THINKTEAM 179Maurice H. ter Beek, Stefania Gnesi, Diego Latella, Mieke Massink, Maurizio Sebastianis, and Gianluca Trentanni9.1 Introduction 1799.2 thinkteam 1829.3 Analysis of the thinkteam Log File 1849.4 thinkteam with Replicated Vaults 1899.5 Lessons Learned 2019.6 Conclusions 201PART VI RUNTIME: TESTING AND MODEL LEARNING 20510 THE TESTING AND TEST CONTROL NOTATION TTCN-3 AND ITS USE 207Ina Schieferdecker and Alain-Georges Vouffo-Feudjio10.1 Introduction 20710.2 The Concepts of TTCN-3 21010.3 An Introductory Example 21610.4 TTCN-3 Semantics and Its Application 21910.5 A Distributed Test Platform for the TTCN-3 22010.6 Case Study I: Testing of Open Service Architecture (OSA)/Parlay Services 22310.7 Case Study II: Testing of IP Multimedia Subsystem (IMS) Equipment 22510.8 Conclusion 23011 PRACTICAL ASPECTS OF ACTIVE AUTOMATA LEARNING 235Falk Howar, Maik Merten, Bernhard Steffen, and Tiziana Margaria11.1 Introduction 23511.2 Regular Extrapolation 23911.3 Challenges in Regular Extrapolation 24411.4 Interacting with Real Systems 24711.5 Membership Queries 25011.6 Reset 25311.7 Parameters and Value Domains 25611.8 The NGLL 26011.9 Conclusion and Perspectives 263References 264INDEX 269