دانلود کتاب Integrated Formal Methods: 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings (Lecture Notes in Computer Science)

فهرست مطالب :

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