Formal Methods for Industrial Critical Systems: 27th International Conference, FMICS 2022, Warsaw, Poland, September 14–15, 2022, Proceedings (Lecture Notes in Computer Science, 13487)

This book constitutes the proceedings of the 27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022, which took place in Warsaw, Poland, in September 2022. The 13 full papers included in this book were carefully reviewed and selected from 22 submissions. They were organized in topical sections as follows: Certification; industrial use cases; testing and monitoring; and methodology. Preface 6 Organization 7 Contents 9 Invited Keynote Talks 11 Reinforcement Learning with Guarantees that Hold for Ever 12 1 Learning from Rewards 12 2 Learning with -Regular Objectives 13 2.1 Good-for-MDP Automata 13 2.2 From GFM Büchi Automata to Reachability and RL 14 3 Related Work 14 References 15 Supporting Railway Innovations with Formal Modelling and Verification 17 References 19 Certification 21 Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification 22 1 Introduction 22 2 Certification Preamble 23 3 Related Work 24 4 Monotony Analysis 25 4.1 Goal of the Analysis 26 4.2 MILP Formulation 27 4.3 Verification Procedure 29 5 Case Study: Braking Distance Estimation 32 5.1 Description of the Case Study 32 5.2 Experimentation 34 6 Conclusion 36 References 37 Generating Domain-Specific Interactive Validation Documents 39 1 Introduction and Motivation 39 2 Validation Workflow 41 3 Static VisB HTML Export 42 4 Dynamic HTML Export: Code Generation to HTML and JavaScript 43 4.1 Graphical User Interface 45 4.2 Applicability of JavaScript Code Generation 46 5 Case Studies 48 6 Related Work 51 7 Conclusion and Future Work 53 References 54 Deductive Verification of Smart Contracts with Dafny 57 1 Introduction 57 2 Verification of Closed Smart Contracts 59 3 Verification Under Adversarial Conditions 65 3.1 Aborting a Computation 65 3.2 Reasoning with Arbitrary External Calls 66 4 Conclusion 71 References 71 Industrial Use Cases 74 Towards Reusable Formal Models for Custom Real-Time Operating Systems 75 1 Introduction 75 2 Preliminaries 76 2.1 Core Components of Real-Time Operating Systems 76 2.2 Uppaal Timed Automata 77 3 Related Work 79 4 Reusable Formal Models for Custom RTOS 80 4.1 Formalization of Tasks 82 4.2 Formalization of Cyclic Handlers 83 4.3 Events and Timing Behavior 84 4.4 Configurable Formal Scheduler Model 85 4.5 Modeling Sensor Inputs and Communication 86 5 Case Study: Search and Rescue Robots 86 6 Conclusion 89 References 90 Formal Verification of an Industrial UML-like Model using mCRL2 92 1 Introduction 92 2 Cordis Models 94 2.1 Class Diagrams 94 2.2 State Machine Diagrams 95 3 Cylinder 97 4 Model Checking Cordis Models Using mCRL2 99 4.1 Translation to mCRL2 99 4.2 Formal Verification of Requirements 102 4.3 Results 104 5 Discussion 104 6 Concluding Remarks 106 References 107 Chemical Case Studies in KeYmaera X 109 1 Introduction 109 2 Background 109 2.1 Differential Dynamic Logic 110 2.2 KeYmaera X 111 3 Results 111 3.1 Controlled Irreversible Reactions 111 3.2 Uncontrolled Reversible Reactions 117 4 Related Work 121 5 Conclusion 123 References 123 Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining 127 1 Introduction 127 2 Related Work 128 3 Identification of Capacity Bottlenecks 129 3.1 Method 129 3.2 Results 129 4 Analysing Delay Propagations 130 4.1 Goals and Overview 130 4.2 Episode Mining 131 4.3 Algorithm and Implementation 135 4.4 Adaptations 135 5 Evaluation Results 137 6 Conclusions and Outlook 138 References 138 Testing and Monitoring 140 Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production 141 1 Introduction 141 1.1 Limitations and Contributions 143 2 Related Work 144 3 Methodology 145 3.1 Intermediate Representation 146 3.2 Bounded Symbolic Execution 147 3.3 Shadow Symbolic Execution 149 4 Evaluation 152 5 Conclusion 155 References 156 Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers 159 1 Introduction 159 2 Preliminaries 161 3 Running Example 163 3.1 Formalization of Road Traffic Rules with LTL MS 164 3.2 Scenario and Trace Encoding (Static and Dynamic Objects) 166 4 Monitoring Model Construction 167 5 Empirical Evaluation 171 6 Related Work 172 7 Conclusion and Future Work 173 References 173 Model-Based Testing of Internet of Things Protocols 176 1 Introduction 176 1.1 Related Work 177 1.2 Contributions 178 2 Preliminaries 178 2.1 Internet of Things 178 2.2 Model-Based Testing 178 2.3 Axini Modeling Platform (AMP) 180 3 MBT in the Context of IoT 180 3.1 IoT Testing Challenges 180 3.2 Positioning MBT in IoT 180 4 The AMP MBT Environment to Test BLE IoT Systems 181 4.1 SUT 181 4.2 Model Creation 182 4.3 AML Model Example 183 4.4 Adapter 186 5 Testing BLE Using AMP 186 5.1 Assumption 186 5.2 Test Generation Configurations 187 5.3 Conformance Experiment 187 5.4 Model Assumption Experiment 188 6 Discussion 189 7 Conclusion 190 7.1 Future Work 190 References 191 Methodology 194 Formally Verifying Decompositions of Stochastic Specifications 195 1 Introduction 195 2 Problem Illustration 196 3 A Theory for Specifying Stochastic Behavior 199 3.1 Traces and Behaviors 199 3.2 Specifications 201 3.3 Trace Automata 201 3.4 Probabilistic Automaton Contracts 203 4 Verification of Refinement 205 5 Case Study 207 6 Related Work 209 7 Conclusions 209 References 210 Verification of Behavior Trees using Linear Constrained Horn Clauses 213 1 Introduction 213 2 Related Works 214 3 Preliminaries 215 3.1 Behavior Trees 216 3.2 Constrained Horn Clauses 217 4 Encoding of Behavior Trees 217 4.1 Idea 217 4.2 Action Node 218 4.3 Condition Node 219 4.4 Sequence Node 219 4.5 Sequence Node with Memory 220 4.6 Selector Node 221 4.7 Parallel Node 221 4.8 Root Node 223 4.9 Safety Property 223 4.10 Environment 223 5 Experiments 224 5.1 Benchmark 224 5.2 Discussion 225 6 Conclusion and Outlook 226 References 226 A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems 228 1 Introduction 228 2 Background 230 2.1 Software Behavior 230 2.2 State Machines 230 2.3 State Machine Comparison 231 3 Behavioral Comparison Methodology 232 3.1 Level 1: Model Set Variants 233 3.2 Level 2: Model Set Variant Relations 234 3.3 Level 3: Model Set Variant Differences 235 3.4 Level 4: Model Variants 236 3.5 Level 5: Model Variant Relations 236 3.6 Level 6: Model Variant Differences 237 4 Evaluation 237 4.1 Case Study 1: Legacy Component Technology Migration 237 4.2 Case Study 2: System Behavior Matching Recipe 239 5 Conclusions and Future Work 243 References 243 Author Index 246