Preface
Organization
Abstracts of Invited Talks
A Survey of Bidding Games on Graphs
Applying Formal Methods in Industrial Railway Applications at Thales
Safe Reinforcement Learning using Probabilistic Shields
Contents
FMICS 25th Anniversary
The 2020 Expert Survey on Formal Methods
1 Introduction
2 Survey Methodology
2.1 Participants
2.2 Questions
2.3 Survey
2.4 Answers
2.5 Comments
2.6 Terminology
3 Assessment of Formal Methods
3.1 System Design
3.2 Quality Assessment
3.3 Expected Benefits
3.4 Relation to Cybersecurity
3.5 Missed Opportunities
4 Formal Methods in Research
4.1 Overall Evaluation
4.2 Foundational Nature
4.3 Main Criticisms
4.4 Topic Relevance
4.5 Research Priorities
4.6 Software Development
5 Formal Methods in Industry
5.1 Impact Evaluation
5.2 Technology Readiness
5.3 Return on Investment
5.4 Most Effective Framework
5.5 Limiting Factors
5.6 Research-Industry Gap
5.7 Design Life Cycle
5.8 Dissemination Players
5.9 Academic Policies
6 Formal Methods in Education
6.1 Course Level
6.2 Importance Level
6.3 Course Format
6.4 Course Organisation
6.5 Tool Usage
7 Future of Formal Methods
7.1 Future Dissemination
7.2 Future Users
7.3 Promising Applications
7.4 Potential Competitors
7.5 Major Breakthroughs
8 Conclusion
9 Position Statements
References
Quantitative Analysis andΒ Cyber-Physical Systems
Verifiable and Scalable Mission-Plan Synthesis for Autonomous Agents
1 Introduction
2 Preliminaries
2.1 Timed Automata and UPPAAL
2.2 UPPAAL STRATEGO
2.3 Reinforcement Learning
3 Problem Description: An Autonomous Quarry
3.1 Problem Analysis
3.2 Uncertainties and Scalability of Mission Planning
4 MCRL: Combining Model Checking and Reinforcement Learning in UPPAAL
4.1 Timed-Automata-Based Model for Mission-Plan Synthesis
4.2 MCRL Method Description
5 Experimental Evaluation
6 Discussion
7 Related Work
8 Conclusions and Future Work
References
Skylines for Symbolic Energy Consumption Analysis
1 Introduction
2 Methodology
3 The SECA Language
3.1 Syntax
3.2 Semantics
4 Energy-Aware Symbolic Execution
4.1 The Energy-Aware Symbolic Execution Semantics
4.2 Evaluation of Expressions
4.3 Execution of Statements
5 Merging Skylines
6 A Real-World Example: Line-Following Robot
7 Related Work
8 Discussion and Future Work
References
Formally Verified Timing Computation for Non-deterministic Horizontal Turns During Aircraft Collision Avoidance Maneuvers
1 Introduction
1.1 Non-deterministic Turn-to-Bearing Kinematics
2 Literature Review
3 Reasoning Foundations for Turn-to-Bearing Maneuvers
3.1 Library Interface
3.2 Trigonometric Properties
3.3 Turn-to-Bearing Path Properties
4 Reasoning About the Timing of Intersecting Turns
4.1 Pointwise Collision Timing
4.2 Path Length Properties
4.3 Exact Timing Wavefront
5 Conclusion
References
An Actor-Based Approach for Security Analysis of Cyber-Physical Systems
1 Introduction
2 An Actor-Based Modeling Language: Rebeca
3 Methodology
3.1 Building the Rebeca Model of the Cyber-Physical System
3.2 Attack Modeling
3.3 Model Checking and Security Analysis
4 Attack Classification
5 The SWaT Case Study and Evaluation
5.1 Security Objectives and Threats
5.2 SWaT Actor Model
5.3 The Rebeca Model of the SWaT System
5.4 Attack Models in Rebeca
5.5 Model Checking and Security Analysis
6 Related Work
7 Conclusion and Future Work
References
Formal Verification ofΒ Industrial Systems
Scalable Detection of Amplification Timing Anomalies for the Superscalar TriCore Architecture
1 Introduction
2 Tracking Amplification Timing Anomalies
2.1 Amplification Timing Anomalies
2.2 UCLID5 Modeling and Verification Tool
2.3 Basic Canonical Pipeline Model
3 Canonical Pipeline Model for the TriCore Architecture
3.1 Dual Pipeline and Stalling Logic
3.2 Store Buffer
3.3 Store Buffer and Dependent Loads
3.4 Write-after-Write Dependencies and Structural Hazards
4 Evaluations
4.1 Basic TriCore Model
4.2 Data Dependencies
4.3 Analysis of a Provided Counter-Example
4.4 Code-Specific Verification
5 Related Work
6 Conclusion and Future Work
References
A Formally Verified Plasma Vertical Position Control Algorithm
1 Introduction
2 Background
2.1 Tokamak Reactors
2.2 Vertical Stabilization
2.3 Differential Dynamic Logic
2.4 Example: Ball Suspended in Cylinder
3 The T-15 Vertical Stabilization Controller
4 The Model
5 The Analysis
5.1 The Proof Calculus of Differential Dynamic Logic
5.2 Proof Structure
5.3 Safety in the Steady State
5.4 Proving the System Remains Safe While Approaching the Reference Value
6 Related Work in Formal Methods
6.1 Applications of Formal Methods in Power Plants and Similar Control Systems
6.2 Hybrid Systems Case Studies and Tools
7 Conclusion
References
The First Twenty-Five Years of Industrial Use of the B-Method
1 Introduction
2 B for Software: The Early Days and Industrial Uptake
2.1 Early Adoption
2.2 Driverless Metro Software: MΓ©tΓ©or and Its Successors
2.3 Code Generation for Hardware
3 B for System Modelling
4 B for Data Validation
5 Projects Outside the Railway Domain
6 B-Method Tools Throughout the Years
7 Discussion and Conclusions
References
A Safety Flasher Developed with the CLEARSY Safety Platform
1 Introduction
2 Terminology
3 Introduction to the B Method
4 CLEARSY Safety Platform
4.1 CSSP Starter Kit
4.2 CSSP Core
4.3 Services
4.4 Safety Case
4.5 Safety Related Application Conditions
5 The Safety Flasher
6 Conclusion and Perspectives
References
Temporal Logic andΒ Model Checking
Formal Verification of OIL Component Specifications using mCRL2
1 Introduction
2 OIL
2.1 A Brief Introduction to OIL
2.2 Validity of OIL Component Specifications
3 Model Checking OIL Specifications with mCRL2
3.1 Translation to mCRL2
3.2 Implementation of the Translation
3.3 Formal Verification of Validity Requirements
4 Experiments
4.1 The EPC Case
4.2 The AGA Case
5 Discussion of Results
6 Conclusion
References
Temporal-Logic Query Checking over Finite Data Streams
1 Introduction
2 Background and Related Work
2.1 Temporal Logic
2.2 Query Checking
2.3 Data Streams
3 Finite LTL Query Checking
4 From Finite LTL Queries to Automata
4.1 From Finite LTL to PNFAs
4.2 From Finite LTL Queries to FQAs
4.3 Composing PNFAs and FQAs
5 Shattering FQAs
5.1 Shattering Propositional Queries
5.2 Computing Shattering Conditions for FQAs
6 Solving QC(, [var])
6.1 Query Checking Single Data Streams
6.2 Query Checking Multiple Data Streams
7 Experimental Results
8 Conclusions and Future Work
References
Verification of a Failure Management Protocol for Stateful IoT Applications
1 Introduction
2 Failure Management Protocol
2.1 Application Model
2.2 Protocol Managers
2.3 Failure Management Protocol
2.4 Recovery Phase
3 Model Checking
3.1 Specification
3.2 Properties
3.3 Experiments
3.4 Detected Issues
4 Related Work
5 Concluding Remarks
References
Author Index