Integrated Formal Methods

Name: Integrated Formal Methods | 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings
Brand: Springer
Price: 80.24 EUR
Availability: OnlineOnly

17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings

Maurice H. ter Beek Rosemary Monahan(Editor)

Springer (Publisher)

Published on 1. June 2022

XV, 373 pages

E-Book

PDF with digital watermarking

System requirements

978-3-031-07727-2 (ISBN)

€80.24incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Side Channel Secure Software (Abstract of Invited Talk)
Contents
Invited Presentations
Verifying Autonomous Systems
1 Introduction
2 A Cognitive Agent Decision Maker
3 Verifying Autonomous Choices
3.1 The MCAPL Framework
4 The Problem with Environments
5 Compositional Verification
5.1 Module Level vs. System Level Properties
5.2 Combining Results
6 Conclusion
References
Empowering the Event-B Method Using External Theories
1 Introduction
2 Invariants and Well-Definedness (WD)
3 Overview of Event-B
3.1 Contexts and Machines (Tables1b and 1c)
3.2 Event-B Extensions with Theories
4 An Illustrative Case Study
5 Invariant Preservation: Core Event-B
6 Data Type Theory-Based Invariant Preservation
6.1 An Event-B Datatype Based Domain-Specific Theory (Step 1)
6.2 An Event-B Instantiation Context (Step 2)
6.3 A Domain-Specific Event-B Machine (Step 3)
7 The Proof Process
8 Revisited Event-B Models for LTS
8.1 A Data Type for LTS (Step 1)
8.2 An Instanciation Context for LTS (Step 2)
8.3 A Data Type Specific Machine for LTS (Step 3)
8.4 Proof Process
9 Conclusion
References
Cooperative and Relational Verification
Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
1 Introduction
2 Summary
2.1 Verification Approaches
2.2 Gaps in the Requirements
2.3 Post-implementation Verification
3 Conclusions and Future Work
References
Formal Specification and Verification of JDK's Identity Hash Map Implementation
1 Introduction
2 Preliminaries
3 The Verification Subject: JDK's IdentityHashMap
4 Specification and Verification of the IdentityHashMap
4.1 Mechanic Proof
5 Engineering Specifications Using Lightweight Analyses
5.1 Bounded Analysis for Auxiliary Specifications
5.2 Unit Tests for Property Specifications
6 Discussion
6.1 Empirical Identification of Verification Challenges
6.2 Discovered Bugs and Recommendations
7 Conclusion
References
Reusing Predicate Precision in Value Analysis
1 Introduction
2 Programs and Precisions
3 From Predicate Precision to Initial Value Precision
4 Evaluation
4.1 Experimental Setup
4.2 Experimental Results
5 Related Work
6 Conclusion
References
Certified Verification of Relational Properties
1 Introduction
2 Syntax and Semantics of the L Language
2.1 Notation for Locations, States, and Procedure Contracts
2.2 Syntax for Expressions and Commands
2.3 Operational Semantics
3 Functional Correctness
4 Relational Properties
5 Verification Condition Generation for Hoare Triples
5.1 Verification Condition Generator
5.2 Hoare Triple Verification
6 Verification of Relational Properties
7 Related Work
8 Conclusion
References
B Method
Reachability Analysis and Simulation for Hybridised Event-B Models
1 Introduction
2 The State-Of-The-Art in CPS V&V
3 Framework for CPS Design and Analysis
4 Preliminaries
4.1 Event-B and Hybridised Event-B
4.2 Reachability Analysis and JuliaReach
4.3 Simulink and Stateflow
5 Case Study: Railway Signalling System
5.1 Continuous Rolling Stock Model
5.2 Communication-Based Railway Signalling Model
6 Case Study: Formal Development
6.1 Event-B Model Development and Verification
6.2 Train Model Simulation and Validation
7 Conclusions and Future Work
References
Operation Caching and State Compression for Model Checking of High-Level Models
1 Introduction
2 Current State of Model Checking for B
2.1 Prolog Default Model Checker
2.2 TLC Backend
2.3 LTSMin Backend
3 Compression and Other Improvements
3.1 Timeouts
3.2 Reducing Stored Transitions
3.3 State Compression
4 Operation Caching
5 Experiments
6 Discussion and Conclusion
References
Time
Conservative Time Discretization: A Comparative Study
1 Introduction
2 Problem Statement
3 Discretization Methods
3.1 Notation
3.2 Methods for Nonlinear Systems
3.3 Common Structure of Methods for Linear Systems
3.4 First-Order d/dt Method
3.5 First-Order Zonotope Method
3.6 Correction-Hull Method
3.7 First-Order Method
3.8 Forward-Backward Method
3.9 Forward-Only Method
3.10 Combining Methods
3.11 Application to High-Dimensional Systems
3.12 Application to Time-Varying Systems
4 Problem Transformations
4.1 Homogenization
4.2 Shrinking the Time Step
5 Efficient Implementation
5.1 The Concept of a Lazy Set
5.2 Computation of Matrix Functions
5.3 Simplification of the Set Representation
6 Experimental Evaluation
6.1 Setup
6.2 Models
6.3 Visual Evaluation of Varying Parameters
6.4 Quantitative Evaluation by Scaling
6.5 Summary
7 Conclusion
References
Untangling the Graphs of Timed Automata to Decrease the Number of Clocks
1 Introduction
2 Timed Automata
3 Constructing a Better Automaton
3.1 Building a Tree from a Timed Automaton
3.2 Untangling Trees: An Overview
3.3 Step One: Computing the Real Cost and Group Analysis
3.4 Step Two: Untangling
3.5 Obtaining the Final Automaton
4 Implementation and Experimental Results
5 Stepping Outside TAS
6 Conclusions
References
Probability
Probabilistic Model Checking of BPMN Processes at Runtime
1 Introduction
2 Models
3 Probabilistic Model Checking of BPMN
3.1 Overview
3.2 BPMN Process Monitoring
3.3 Transforming LTS into PTS
4 Tool Support
4.1 Tool
4.2 Case Study
4.3 Additional Experiments for Performance Evaluation
5 Related Work
6 Conclusion
References
HyperPCTL Model Checking by Probabilistic Decomposition
1 Introduction
2 Preliminaries
2.1 HyperPCTL Syntax
2.2 HyperPCTL Semantics
3 A Probabilistic Decomposition Approach
4 Probabilistically Dependent Markov Chains
4.1 Time and Memory Complexity
5 Case Studies and Evaluation
6 Conclusion and Future Work
References
Learning and Synthesis
Learning Finite State Models fromRecurrent Neural Networks
1 Introduction
2 Preliminaries
3 Automata Extraction from RNNs
3.1 Test-Based Learning from RNNs
3.2 Equivalence Queries from a Practical Perspective
3.3 Research Questions
4 Experiments on Learning Automata from RNNs
4.1 Learning Models of RNNs Trained on Tomita Grammars
4.2 Learning Models of RNNs Trained on Balanced Parentheses
4.3 Analyzing RQ2 on the Tomita 3 Grammar
5 Related Work
6 Conclusion
References
Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
1 Introduction
2 Concurrent Update Synthesis
2.1 Routing Policy
2.2 Concurrent Update Synthesis Problem
3 Optimisation Techniques
3.1 Topological Decomposition
3.2 Collective Update Classes
4 Translation to Petri Games
4.1 Petri Games
4.2 Translation Intuition
4.3 Translation of Network Topology and Routings
4.4 Policy Translation
4.5 Reachability Objective and Translation Correctness
5 Experimental Evaluation
5.1 Results
6 Conclusion
References
Security
Verified Password Generation from Password Composition Policies
1 Introduction
2 Current Password Generation Algorithms
2.1 Password Composition Policies
2.2 Random Password Generation
3 Verified Password Generation
3.1 Reference Implementation
3.2 Formal Proofs
4 Case Study: From Apple Password Rules to Verified Password Generation in Bitwarden
4.1 Apple's Password Autofill Rules
4.2 Jasmin Password Generator
4.3 Integration with Bitwarden
5 Related Work
6 Conclusion
References
A Policy Language to Capture Compliance of Data Protection Requirements
1 Introduction
2 Main Principles of the GDPR
3 A Policy Language for Main Data Protection Principles
4 Taxonomies as Tree Structures
5 Policy Compliance
6 Proof of Concept Implementation
7 Case Study: Health Wearable
8 Analysis of Related Work
9 Conclusion and Future Work
References
Static Analysis and Testing
Extending Data Flow Coverage to Test Constraint Refinements
1 Introduction
2 Motivation Examples
3 Background
4 The Required k-Use Chains
5 Related Work and Conclusions
References
Scalable Typestate Analysis for Low-Latency Environments
1 Introduction
2 Bit-Vector Typestate Analysis
2.1 Annotation Language
2.2 Bit-Vector Finite Automata
3 Compositional Analysis Algorithm
4 Evaluation
5 Related Work
6 Concluding Remarks
References
PhD Symposium Presentations
Studying Users' Willingness to Use a Formally Verified Password Manager
1 Introduction
2 Current Work
2.1 First Study
2.2 Second Study
3 Conclusion and Impact
References
Modeling Explanations in Autonomous Vehicles
1 Introduction
2 Related Work and Current Progress
3 Conclusion and Future Work
References
A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller
1 Overview
2 Three-Phase Methodology
3 `FRET-Guided' Modelling
4 Future Work
References
A Dialogue Interface for Low Code Program Evolution
1 Introduction
2 Approach
3 Conclusions
References
Simple Dependent Types for OSTRICH
1 Introduction
2 Approach
3 Conclusions
References
SNITCH: A Platform for Information Flow Control
1 Introduction
2 Approach
3 Conclusion
References
Machine-Assisted Proofs for Institutions in Coq
1 Introduction
2 Mathematical Background and Contributions
3 Conclusions and Future Work
References
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Integrated Formal Methods

Description

More details

Other editions

Additional editions

Content

System requirements