Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends (Lecture Notes in Computer Science, 12479)

✍ Scribed by Tiziana Margaria (editor), Bernhard Steffen (editor)

• Publisher: Springer
• Year: 2021
• Tongue: English
• Leaves: 273
• Category: Library

✦ Synopsis

The four-volume set LNCS 12476 - 12479 constitutes the refereed proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, which was planned to take place during October 20–30, 2020, on Rhodes, Greece. The event itself was postponed to 2021 due to the COVID-19 pandemic.

The papers presented were carefully reviewed and selected for inclusion in the proceedings.

Each volume focusses on an individual topic with topical section headings within the volume:

Part I, Verification Principles:
Modularity and (De-)Composition in Verification; X-by-Construction: Correctness meets Probability; 30 Years of Statistical Model Checking; Verification and Validation of Concurrent and Distributed Systems.

Part II, Engineering Principles:
Automating Software Re-Engineering; Rigorous Engineering of Collective Adaptive Systems.

Part III, Applications:
Reliable Smart Contracts:State-of-the-art, Applications, Challenges and Future Directions; Automated Verification of Embedded Control Software; Formal methods for DIStributed COmputing in future RAILway systems.

Part IV, Tools and Trends:
From Verification to Explanation; Engineering of Digital Twins for Cyber-Physical Systems; Software Verification Tools.

✦ Table of Contents

Introduction
Organization
Contents – Part IV
From Verification to Explanation
From Verification to Explanation (Track Introduction)
1 Introduction
2 Context
3 Contributions in this Track
References
An Algorithm to Compute a Strict Partial Ordering of Actions in Action Traces
1 Motivation
2 Preliminaries
3 Algorithm to Analyze Action Orders in Action Traces
4 Case Study
5 Conclusion
References
TraceVis: Towards Visualization for Deep Statistical Model Checking
1 Introduction
2 Related Work
3 Background: DSMC20 and Racetrack
4 Visualization Concept
5 Visualizing Probabilities
6 Visualizing Policy Traces
7 Case Study
8 Conclusion
References
Engineering of Digital Twins for Cyber-Physical Systems
Engineering of Digital Twins for Cyber-Physical Systems
1 Introduction
2 Contributions
3 Concluding Remarks
References
Understanding Digital Twins for Cyber-Physical Systems: A Conceptual Model
1 Introduction
2 Running Example
3 Overview
4 Physical Twin and Digital Twin
4.1 Physical Twin
4.2 Digital Twin
5 Evolution and Uncertainty
5.1 Evolution
5.2 Uncertainty
6 Life-Cycle
7 Related Work
8 Conclusion
References
Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins
1 Introduction
2 The Need for Digital Twins and Tolerance
3 The Agricultural Vehicle Case Study
3.1 Vehicle Kinematics
3.2 Controller
3.3 Deployed System
3.4 Statistical Analysis
3.5 Runtime Monitoring
3.6 What-If Analysis
4 Conclusion
References
Designing Distributed Control with Hybrid Active Objects
1 Introduction
2 A Short Overview of ABS
2.1 The Time Model of Timed ABS
2.2 The Model API
3 Hybrid Abstract Behavioral Specification Language
3.1 Syntax and Semantics
3.2 Analyzability
4 Models for Distributed Control
4.1 Internal Control
4.2 Predictive Control
5 Discussion: Hybrid Active Objects in Relation to Co-simulation and Digital Twins
5.1 Relation to Co-simulation
5.2 Relation to Digital Twins
6 Conclusion
References
Towards a Digital Twin - Modelling an Agricultural Vehicle
1 Introduction
2 Materials and Methods
2.1 Functional Mockup Interface
2.2 Digital Twin Tool-Chain
2.3 The Robotti Model
3 Results
3.1 Scenario 1: Changing Track Width
3.2 Scenario 2: Loading the Three-Point Linkage
4 Discussion and Future Work
4.1 Soil–Machine Interaction
4.2 Co-simulation and Digital Twins
4.3 Desktop-Version of Robotti
4.4 Concluding Remarks
References
Digital Modelling in the Railways
1 Introduction
2 Terminology
3 Modelling Infrastructure
3.1 Categories
3.2 Rails
3.3 Dynamics
3.4 Timetables
4 Modelling Safety
4.1 Automatic Pilot - Braking
4.2 Estimating Maintenance Periods
4.3 Formal Data Validation
4.4 Proving Interlocking (Model-Checking, Installation-Based)
4.5 Modelling Design Reasoning
5 Convergence and Relevance
6 Conclusion and Perspectives
References
Engineering a Digital Twin for Manual Assembling
1 Introduction
2 Assembly Workstation Digital Twin Concept
3 Implementation Issues
4 Machine Learning Capabilities
4.1 Human Emotions
4.2 Context-Based Predictors for the Assembly Sequences
5 Conclusions and Future Work
References
Towards Digital Twins for Knowledge-Driven Construction Progress and Predictive Safety Analysis on a Construction Site
1 Introduction
1.1 Related Work
2 Automatic Construction Progress Analysis
2.1 Explaining Sensor Data via Abductive Reasoning
2.2 Answer Set Programming (ASP)
2.3 Abductive Reasoning Using Answer Set Programming
3 From Physical Twin to Digital Twin: The Framework and Workflow
3.1 Three Framework Modules
4 Functional Demonstration with Trajectory Data from a Construction Site
5 From Manual to Automatic Safety Analysis
5.1 Formalising Safety Building Codes for Automatic Safety Analysis
5.2 The Shape of Meaningful ``Empty Spaces'' in Construction Safety
6 Reasoning About Safety in 4D BIM Construction Plans
6.1 Functional Demonstration of Safety Analysis
7 Concluding Remarks and Future Work
References
Software Verification Tools
Software Verification Tools (Track Introduction)
1 Introduction
2 Contributions with Published Papers in the Track
3 Conclusion
References
Benchmarking Open-Source Static Analyzers for Security Testing for C
1 Introduction
2 Previous Work on Benchmarking SAST Tools for C
3 Prevalence of C-Related Vulnerability Patterns
4 SAST Tool Evaluation Method
4.1 Tested Open-Source SAST Tools
4.2 Evaluation Datasets
4.3 Evaluation Procedure for Synthetic Test Cases
4.4 Trial on Production Software
5 Results and Discussion
5.1 Effect of Severity Thresholds
5.2 Tools' Recall on SFP Clusters
5.3 Overall SAST Tool Accuracy
5.4 SAST Tool Overlap
5.5 Trial on Production Software
6 Threats to Validity
7 Conclusion
References
Verification of Liveness and Safety Properties of Behavioral Programs Using BPjs
1 Introduction
2 Problem Formulation
3 Model Driven Engineering with BP
3.1 Conforming with Safety Properties
3.2 Deadlock Detection
3.3 Liveness Requirements
4 Evaluation
5 Related Work
6 Conclusion
References
On Correctness, Precision, and Performance in Quantitative Verification
1 Introduction
2 Languages, Formalisms, and Properties
3 Correctness and Precision
3.1 Correctness Challenges
3.2 Correct Algorithms
3.3 Correctness in QComp 2020
4 Participating Tools
5 Performance Evaluation
5.1 Quantile Plots
5.2 Scatter Plots
6 Conclusion
References
Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees
1 Introduction
2 Preliminaries
2.1 Modal Transition Systems
2.2 Parallel Composition and Weakest Specification
2.3 Alphabet View
2.4 Linear Temporal Logic Model Checking
3 Hardness
4 Negative Verification Tasks
4.1 Initial Green Contract Construction
4.2 Iterated Decomposition
5 Positive Verification Tasks
5.1 Initial Modal Contract Construction
5.2 Iterated Decomposition
6 Conclusion and Outlook
References
Author Index