Formal Methods For Industrial Critical Systems: 24th International Conference, Fmics 2019, Amsterdam, The Netherlands, August 30-31, 2019, Proceedings (lecture Notes In Computer Science)

This book constitutes the proceedings of the 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019, held in Amsterdam, The Netherlands, in August 2019. The 9 regular papers presented in this volume were carefully reviewed and selected from 15 submissions. The conference also featured invited talks by Jaco van de Pol (Aarhus University, and Twente University), jointly with CONCUR, and Holger Hermanns (Universität des Saarlandes) and a special session on (commercial) formal methods in industry. The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications. Preface 6 Organization 8 Abstracts 10 Concurrent Algorithms and Data Structures for Model Checking 11 Power in Low Earth Orbit. Verified 12 Contents 14 Modelling and Analysing ERTMS L3 Moving Block Railway Signalling with Simulink and UPPAAL SMC 15 1 Introduction 15 2 ERTMS L3 Moving Block Railway Signalling 18 3 Simulink Model of ERTMS L3 Moving Block 21 4 UPPAAL Model of ERTMS L3 Moving Block 22 5 Analyses of ERTMS L3 Moving Block 29 6 Lessons Learned 31 7 Conclusion 32 References 33 Formal Modelling and Verification of an Interlocking Using mCRL2 36 1 Introduction 36 2 Railway Signalling Systems 37 3 mCRL2 Model of an Interlocking 39 3.1 Modelling Data and Predicates 39 3.2 Modelling the Behaviour of the Interlocking and the Field Elements 41 4 Formal Verification of the mCRL2 Model 42 4.1 Requirements 42 4.2 Verification Toolchain 44 4.3 Results 45 5 Model-Based Testing to Validate Model 46 6 Discussion and Conclusions 48 6.1 Lessons Learned 48 6.2 Research Challenges for mCRL2 and JTorX 49 6.3 Further Research for Development of Signalling Systems 50 6.4 Concluding Remarks on Formal Methods in Railway Signalling 51 References 51 A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas 54 1 Introduction 54 2 Related Work 56 3 Preliminaries 57 3.1 Fundamentals of Railway Operations 57 3.2 Fault Trees 58 3.3 Markov Chains 59 4 DFT Model for Railway Station Reliability Analysis 60 4.1 DFT Model for Railway Station 60 4.2 DFT Models for Infrastructure Components 61 4.3 Failure Rates 64 5 Quality Metrics for Railway Station Areas 65 6 Application Scenarios 66 6.1 Test Cases 66 6.2 Input Data 67 6.3 Results and Discussion 67 7 Conclusion 70 References 70 Multiple Analyses, Requirements Once: 73 1 Introduction 73 2 Related Work 75 3 Pattern-Based Requirement Specification Language 76 4 Pattern-Based Requirement Specification Tool 79 5 Requirement Specification Export to Verification Tools 81 5.1 Export to SLDV 81 5.2 Export to BTC EmbeddedPlatform 84 5.3 Export to Textual Requirements 84 5.4 Export to SV-Comp-style C Code 85 6 Requirement-Based Test Vector Generation 85 7 Conclusion and Future Work 86 A Appendix 87 References 87 The Impact of Requirement Splitting on the Efficiency of Supervisory Control Synthesis 90 1 Introduction 90 2 Preliminaries 92 2.1 Automata 92 2.2 Supervisory Control Theory 93 3 Modeling Guideline and Theoretical Substantiation 95 3.1 Theoretical Substantiation 96 3.2 Conflicting Supervisors 97 4 Demonstration with Case Study of Infrastructural System 98 5 Four Case Studies with Experimental Results 102 5.1 Case Studies Description 102 5.2 Results 103 6 Conclusion and Future Work 104 References 104 Incremental Development of a Safety Critical System Combining formal Methods and DSMLs 107 1 Introduction 107 2 Application Context 109 3 Coloured Petri-Nets: From Modeling to Proofs 110 3.1 Main Concepts 110 3.2 Level 1: Simple Train Movements 111 3.3 Extraction of B Specifications 112 4 A Railway Domain-Specific Modeling Language 114 4.1 Railway Meta-Model 114 4.2 Formal Model 115 5 Putting It All Together 117 5.1 Incremental Development of Operational Semantics 119 6 Conclusion 122 References 122 Probabilistic Verification for Reliable Network-on-Chip System Design 124 1 Introduction 124 2 Motivation 125 3 Related Work 126 4 Conflict Resolution in Central Routers 127 5 Formal Model of the Central Router 128 6 Abstract Models and Refinement 130 7 Including Idle Cycles in the Abstract Model 133 8 Verification Results 134 9 Conclusion 137 References 138 A Simulator for LLVM Bitcode 141 1 Introduction 141 2 Related Work 142 2.1 Comparison to Symbolic Debuggers 143 3 LLVM Bitcode 144 3.1 Verification Extensions 145 3.2 Program Memory 146 3.3 Relating Bitcode to Source Code 147 3.4 Debug Graph 148 4 Working with Data 148 4.1 Starting Points 148 4.2 Typing the Heap 149 4.3 Relating Data and Control 150 5 Navigating the State Space 150 5.1 Stepping Forward 151 5.2 Going Back 152 5.3 Inspecting the Stack 152 5.4 Thread Interleaving 153 5.5 Simulating Counterexamples 153 6 Implementation 154 6.1 User Interface 154 6.2 Programming Language Support 155 7 Conclusion 155 References 156 Verification of Decision Making Software in an Autonomous Vehicle: An Industrial Case Study 157 1 Introduction and Related Work 157 2 Problem Description 159 3 Supervisory Control Theory 161 3.1 Nonblocking Verification 162 3.2 Verification of LSM in Supremica 162 4 Model Checking 164 4.1 Temporal Logic of Actions 164 4.2 Verification of LSM in TLA+ 165 5 Deductive Verification 166 5.1 SPARK 167 5.2 Verification of LSM in SPARK 167 6 Insights and Discussion 169 7 Conclusion 171 References 172 Author Index 174 Front Matter ....Pages i-xv Modelling and Analysing ERTMS L3 Moving Block Railway Signalling with Simulink and Uppaal SMC (Davide Basile, Maurice H. ter Beek, Alessio Ferrari, Axel Legay)....Pages 1-21 Formal Modelling and Verification of an Interlocking Using mCRL2 (Mark Bouwman, Bob Janssen, Bas Luttik)....Pages 22-39 A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas (Matthias Volk, Norman Weik, Joost-Pieter Katoen, Nils Nießen)....Pages 40-58 Multiple Analyses, Requirements Once: (Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow)....Pages 59-75 The Impact of Requirement Splitting on the Efficiency of Supervisory Control Synthesis (Martijn Goorden, Joanna van de Mortel-Fronczak, Michel Reniers, Wan Fokkink, Jacobus Rooda)....Pages 76-92 Incremental Development of a Safety Critical System Combining formal Methods and DSMLs (Akram Idani, Yves Ledru, Abderrahim Ait Wakrime, Rahma Ben Ayed, Simon Collart-Dutilleul)....Pages 93-109 Probabilistic Verification for Reliable Network-on-Chip System Design (Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Rajesh Jayashankara Shridevi, Koushik Chakraborty, Sanghamitra Roy et al.)....Pages 110-126 A Simulator for LLVM Bitcode (Petr Ročkai, Jiří Barnat)....Pages 127-142 Verification of Decision Making Software in an Autonomous Vehicle: An Industrial Case Study (Yuvaraj Selvaraj, Wolfgang Ahrendt, Martin Fabian)....Pages 143-159 Back Matter ....Pages 161-161