Intro
Preface
Organization
Contents
Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect
1 Introduction
2 Related Work
3 MBSD, Sparx Enterprise Architect and UMC
3.1 Sparx Enterprise Architect
3.2 UML Model Checker
4 Methodology
5 Case Study
5.1 Model Checking Sparx EA Models
6 Lessons Learned and Limitations
7 Conclusion
References
The 4SECURail Case Study on Rigorous Standard Interface Specifications
1 Introduction
2 The Demonstrator Case Study

2.1 The 4SECURail Case Study
2.2 The Formalization of the Case Study
3 Cost-Benefit Analysis
4 Discussion and Conclusions
References
Statistical Model Checking for P
1 Introduction
2 An Overview of P
2.1 An Overview of P and its Semantics
2.2 A Case Study: A Bike Sharing System
3 Statistical Model Checking with MultiVeStA
4 Integration of P and MultiVeStA
5 A Case Study
5.1 Verifying Quantitative Properties of the Bikes Example
5.2 On the Scalability of Statistical Model Checking
6 Concluding Remarks
References

Pattern-Based Verification of ROS 2 Nodes Using UPPAAL
1 Introduction
2 Background
2.1 ROS 2
2.2 Timed Automata and UPPAAL
3 Modeling and Verification of ROS 2 Nodes in UPPAAL
4 Evaluation of Pattern-Based Verification
5 Related Work
6 Conclusions and Future Work
References
Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers
1 Introduction
2 Preliminaries
2.1 Railway Interlocking System and its Object Manager Subsystem
2.2 Component Integration and Test Generation Approach

2.3 VIATRA Query Language
3 Configuring Message Queues for Component Interactions
4 Property Specification Using Model Queries
5 Practical Evaluation
6 Related Work
7 Conclusion and Future Work
References
Refinement of Systems with an Attacker Focus
1 Introduction
2 Modelling Systems and Attacks
3 Attacker Objectives
4 Refinement Checking
5 Implementation
6 Case Study
6.1 Amazon Delivery
6.2 Duqu Malware
7 Conclusion
References
Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control
1 Introduction

2 Case House and Problem Statement
3 Buffer Tank and Mixing Loop Thermodynamics
4 System Modelling in Uppaal Stratego
4.1 Buffer Tank Modelling in Uppaal Stratego
4.2 Online Synthesis
5 Experimental Evaluation
5.1 Evaluation Setup
5.2 Buffer Tank Quality Assessment
5.3 Buffer Tank Evaluations with Intelligent Stratego Controller
5.4 Mixing Loop Evaluations with Intelligent Stratego Controller
6 Conclusion
References
Automated Property-Based Testing from AADL Component Contracts
1 Introduction
2 Background
3 Example