Linked e-resources
Details
Table of Contents
Intro
Preface
Organization
Invited Talks
Cooperative Verification
Taming Monsters with Dragons: A Fractal Approach to Digital Twin Pipelines
Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community
Some Applications of Formal Methods
Contents
Model Checking and Semantics
An Efficient Customized Clock Allocation Algorithm for a Class of Timed Automata
1 Introduction
2 Timed automata
3 The Class TADS
4 The Notion of Optimality
5 Finding an Optimal Allocation of Clocks
5.1 Liveness Analysis of Clocks
5.2 Clock Allocation
5.3 The Clock Allocation Algorithm
5.4 Generating Clock Constraints and Clock Resets
6 Related Work and Conclusions
References
Formalization of Functional Block Diagrams Using HOL Theorem Proving
1 Introduction
2 Preliminaries
2.1 Formal ET Modeling
2.2 Formal ET Probabilistic Analysis
3 Functional Block Diagrams
4 FBD Formalization
4.1 Formal FBD Modeling
4.2 Formal FBD Probabilistic Analysis
5 Conclusions
References
Generation and Synthesis
A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching
1 Introduction
2 Basic Definitions
3 Expansion and Transformation
3.1 Unrolling
3.2 Recursion Elimination
4 Term Generation
4.1 Soundness of Term Generation
5 Quick-Checking Properties
6 Related Work
7 Conclusion
References
Automatic Generation of Verified Concurrent Hardware Using VHDL
1 Introduction
1.1 Related Work
2 Theoretical Background
2.1 CSP
2.2 VHDL
3 CSP to VHDL Translation
3.1 Translation Overview
3.2 Restrictions
4 Tool Support
5 Case Study
6 Conclusion
References
Synthesis of Implementations for Divide-and-Conquer Specifications
1 Introduction
2 Preliminaries
3 From Divide-and-Conquer Specifications to Their Implementations
3.1 The Synthesis Rule
4 Case Study: Deriving an Implementation of a Greedy Algorithm
4.1 Weighted Matroids and Their Bases
4.2 Establishing max-basisI as a Divide-and-Conquer Specification
4.3 Implementations of Decomposition and Composition
5 Related Work
6 Conclusions and Outlook
A The Three Auxiliary Lemmas
References
Verification and Solvers
Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover
1 Introduction
2 Background
2.1 Block Diagrams and MDD
2.2 Running Example
Simple Actuator System (SAS)
2.3 Formal Verification and CSP
2.4 tock-CSP
2.5 Roscoe and Dathi's Compositional Deadlock Analysis Theory
2.6 CSP-Prover
3 Mechanised Compositional Verification of Timed Process Networks
3.1 Time-Stop Free Processes
3.2 Time-Stop Free Process Networks
3.3 Mechanisation in CSP-Prover
4 From Simulink to tock-CSP
5 Conclusion and Future Works
References
Preface
Organization
Invited Talks
Cooperative Verification
Taming Monsters with Dragons: A Fractal Approach to Digital Twin Pipelines
Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community
Some Applications of Formal Methods
Contents
Model Checking and Semantics
An Efficient Customized Clock Allocation Algorithm for a Class of Timed Automata
1 Introduction
2 Timed automata
3 The Class TADS
4 The Notion of Optimality
5 Finding an Optimal Allocation of Clocks
5.1 Liveness Analysis of Clocks
5.2 Clock Allocation
5.3 The Clock Allocation Algorithm
5.4 Generating Clock Constraints and Clock Resets
6 Related Work and Conclusions
References
Formalization of Functional Block Diagrams Using HOL Theorem Proving
1 Introduction
2 Preliminaries
2.1 Formal ET Modeling
2.2 Formal ET Probabilistic Analysis
3 Functional Block Diagrams
4 FBD Formalization
4.1 Formal FBD Modeling
4.2 Formal FBD Probabilistic Analysis
5 Conclusions
References
Generation and Synthesis
A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching
1 Introduction
2 Basic Definitions
3 Expansion and Transformation
3.1 Unrolling
3.2 Recursion Elimination
4 Term Generation
4.1 Soundness of Term Generation
5 Quick-Checking Properties
6 Related Work
7 Conclusion
References
Automatic Generation of Verified Concurrent Hardware Using VHDL
1 Introduction
1.1 Related Work
2 Theoretical Background
2.1 CSP
2.2 VHDL
3 CSP to VHDL Translation
3.1 Translation Overview
3.2 Restrictions
4 Tool Support
5 Case Study
6 Conclusion
References
Synthesis of Implementations for Divide-and-Conquer Specifications
1 Introduction
2 Preliminaries
3 From Divide-and-Conquer Specifications to Their Implementations
3.1 The Synthesis Rule
4 Case Study: Deriving an Implementation of a Greedy Algorithm
4.1 Weighted Matroids and Their Bases
4.2 Establishing max-basisI as a Divide-and-Conquer Specification
4.3 Implementations of Decomposition and Composition
5 Related Work
6 Conclusions and Outlook
A The Three Auxiliary Lemmas
References
Verification and Solvers
Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover
1 Introduction
2 Background
2.1 Block Diagrams and MDD
2.2 Running Example
Simple Actuator System (SAS)
2.3 Formal Verification and CSP
2.4 tock-CSP
2.5 Roscoe and Dathi's Compositional Deadlock Analysis Theory
2.6 CSP-Prover
3 Mechanised Compositional Verification of Timed Process Networks
3.1 Time-Stop Free Processes
3.2 Time-Stop Free Process Networks
3.3 Mechanisation in CSP-Prover
4 From Simulink to tock-CSP
5 Conclusion and Future Works
References