Formal Methods and Software Engineering: 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24–27, 2022, Proceedings (Lecture Notes in Computer Science)

✍ Scribed by Adrian Riesco (editor), Min Zhang (editor)

• Publisher: Springer
• Year: 2022
• Tongue: English
• Leaves: 454
• Category: Library

✦ Synopsis

This book constitutes the proceedings of the 23rd International Conference on Formal Engineering Methods, ICFEM 2022, held in Madrid, Spain, in October 2022. The 16 full and 4 short papers presented together with 1 doctoral symposium paper in this volume were carefully reviewed and selected from 41 submissions. The papers cover for research in all areas related to formal engineering methods, such as verification and validation, software engineering, formal specification and modeling, software security, and software reliability.

✦ Table of Contents

Preface
Organization
Model Checking Quantum Markov Chains (Abstract)
Contents
Bridging Formal Methods and Machine Learning with Global Optimisation
1 Introduction
2 Preliminaries
3 V-Model for Machine Learning
4 Specification Language
5 Properties
5.1 Generalisation
5.2 Uncertainty
5.3 Robustness
5.4 Data Poisoning
5.5 Backdoor
5.6 Model Stealing
5.7 Membership Inference
5.8 Model Inversion
5.9 Interpretability
5.10 Fairness
6 Verification of Properties
6.1 Estimation of Posterior Distribution P(W|d) Through MCMC
6.2 Estimation of Posterior Distribution P(W|d) Through Variational Inference
6.3 Estimation of Data Distribution D and Distribution of Predictive Labels P(|d,w)
6.4 Eu () or Vu ()
6.5 DKL(,) or ||-||p
6.6 t and t
7 Related Works
8 Conclusions
References
Canonical Narrowing for Variant-Based Conditional Rewrite Theories
1 Introduction
2 Preliminaries
3 Implementation
3.1 Our Previous Narrowing Command
3.2 Automatic Transformation of Conditional Rules
4 Experiments
4.1 Model of a Bank Account
4.2 Model of a Communication Channel
5 Conclusions and Future Work
References
Modular Analysis of Tree-Topology Models
1 Introduction
2 Tree Synchronisation Systems
2.1 LTS Networks and Synchronisation Topologies
3 Compact Representations of State Spaces of Live-Reset and Sync-Deadlock Trees
3.1 Constructions for Two-level Trees
3.2 Reduced Sum-of-Squares for Any Tree Height
4 The General Case and Local Products
5 Experiments
6 Conclusion
References
Non-linear Optimization Methods for Learning Regular Distributions
1 Introduction
2 Preliminaries
3 Learning a Regular Distribution from a Sample
3.1 Learning the Structure
3.2 Learning the Probabilities
4 Experimental Results
4.1 Learning Randomly Generated Probabilistic Automata
4.2 Learning a Model of an Agent's Traces in a Maze
5 Conclusion
A Appendix
B Appendix
References
Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory Model
1 Introduction
2 An Imperative Language with Instruction Reordering
2.1 Reordering in C
3 Transformation to Sequential or Parallel Form
4 Reasoning About Concurrent C
4.1 Examples
5 Further Extensions
6 Related Work
7 Conclusions
A Syntax and Semantics Definitions
References
Creusot: A Foundry for the Deductive Verification of Rust Programs
1 Introduction
1.1 Example: A Polymorphic Sorting Function
1.2 Contributions
2 Specifying and Proving Programs Using Prophecies
2.1 Background Logic
2.2 Borrows and Prophecies
3 Handling Rust Function Bodies
3.1 Translating Owned Pointers
3.2 Translating Borrows to Prophecies in Why3
4 Support for Rust Traits
4.1 Specifying Trait Behavior
4.2 The Resolve Trait
4.3 Specifying with Models: The Model Trait
5 Experimentation and Evaluation
6 Related Work
References
Generation of a Reversible Semantics for Erlang in Maude
1 Introduction
2 Background
2.1 The Erlang Language
2.2 Maude
2.3 Derivation of the Reversible Semantics
3 Formalizing Erlang in Maude
3.1 Equational Theory
3.2 Expression Management
3.3 Rewriting Rules
4 Generating the Reversible Semantics
4.1 Format of the Non-reversible Semantics
4.2 Transformation to the Syntax
4.3 Generating the Reversible Semantics
5 Correctness
6 Rollback Semantics
7 Conclusion, Related and Future Work
References
Program Slicing Techniques with Support for Unconditional Jumps
1 Introduction
2 Background
3 The Pseudo-predicate Program Dependence Graph
4 Program Slicing Techniques that Conflict with the PPDG
4.1 Representation of Procedure Calls
4.2 Object-Oriented Program Slicing
4.3 Exception Handling and Conditional Control Dependence
5 Implementation
6 Related Work
7 Conclusions
References
Formal Verification of the Inter-core Synchronization of a Multi-core RTOS Kernel
1 Introduction
1.1 Related Works
1.2 Choice of the Model
1.3 Contribution and Outline
2 Trampoline RTOS
2.1 Calling Operating System Services
2.2 Executing a Multi-core Service Call
3 High-Level Colored Time Petri Nets
3.1 Definition of High-Level Colored Time Petri Nets
3.2 Example of HCTPN
4 RTOS and Application Model
4.1 Principles of Modeling
4.2 RTOS Model
4.3 Application Model
5 Formal Verification
5.1 Case Studies
5.2 Correction of the Error
6 Conclusion
References
SMT-Based Model Checking of Industrial Simulink Models
1 Introduction
2 Simulink
3 SMT-Based Model Checking
4 SMT-LIB Encoding of Simulink Models
4.1 Exact Encoding of Machine-Representable Numbers
4.2 Encoding of Complex Simulink Models
4.3 Implementation of the Encoder
5 Model Checking Methods
6 Experimental Evaluation
6.1 Results
6.2 Discussions
7 Related Work
8 Conclusions
References
PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification
1 Introduction
2 Protocol Specifications and Transition Systems
3 Haskell Parallelisation Strategies
4 Parallel Strategies for Search Trees
4.1 parTreeBuffer: A Buffered Parallel Strategy for Search Trees
4.2 Enhanced parTreeBuffer
4.3 parTreeChunkSubtrees
4.4 hybridSubtrees
4.5 Strategies with Annotation
4.6 Comparison
4.7 Enabling the Verification of Protocols with Algebraic Operators
5 Conclusion and Future Work
References
A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures
1 Introduction
2 Background
2.1 Cache Side-Channel Attacks
2.2 Mutual Information
2.3 Isabelle/HOL
3 Methodology Overview
3.1 Threat Model
3.2 Architecture
4 Design of Reasoning Framework
4.1 Interface Layer—An Abstract State Machine
4.2 Noninterference Layer
4.3 Unwinding Conditions
5 Application of Our Methodology: A Case-study
5.1 The General Cache Layouts Specification
5.2 The RP Cache Specification
5.3 Security Verification of RP Cache
6 Security Verification Results and Analysis
7 Conclusions and Future Work
References
Refined Modularization for Bounded Model Checking Through Precondition Generation
1 Introduction
2 Preliminaries
3 Bird's Eye View of the Method
4 Module Extension by Caller Inclusion
5 Refined Modularization Through Preconditions
5.1 Generation of Enumerative Preconditions Based on BMC
5.2 Learning General Preconditions from Data Points
5.3 Subsumption of Preconditions
6 Evaluation
6.1 Evaluation Results
6.2 Comparison to Polyspace
7 Related Work
8 Conclusion
References
TTT/ik: Learning Accurate Mealy Automata Efficiently with an Imprecise Symbol Filter
1 Introduction
2 Related Work
3 System Model
4 Background: Active Automata Learning and TTT
5 The TTT/ik Method
5.1 False Accept Handling
5.2 Extended Counterexample Analysis
5.3 Opportunistic Discriminator Search
6 Evaluation
6.1 Accuracy
6.2 Efficiency
7 Conclusion and Future Work
References
A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency
1 Introduction
2 Semantic Model
2.1 Syntax of CPS with Shared-Variable Concurrency
2.2 Trace Model
2.3 Specification
3 Proof System
3.1 Auxiliary Rules
3.2 Proof Rules for Basic Commands
3.3 Proof Rules for Compound Constructs
4 Case Study
4.1 Description of BMS
4.2 Proof for BMS
5 Conclusion and Future Work
References
Theorem Proving for Maude Specifications Using Lean
1 Introduction
2 Preliminaries
2.1 Rewriting Logic and Maude
2.2 Dependent Type Theory and Lean
3 The Translation
4 The Translation Tool
4.1 Proving the Associativity of the Sum
5 Example: The Dining Philosophers
6 Related Work
7 Conclusions and Future Work
A Proof of Proposition 1
References
On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
1 Introduction
2 Preliminaries
3 Problem Scope
4 Discover Modeling Errors
4.1 Exploiting Controller
4.2 Unchallenged Controller
5 Results
6 Related Work
7 Conclusion
References
Declassification Predicates for Controlled Information Release
1 Introduction
2 Exisiting Approaches
2.1 Non-interference
2.2 Delimited Release
2.3 Localized Delimited Release
3 Declassification Predicates
4 Enforcing Qualified Release
5 Dafny Encoding
6 Conclusion
A Soundness
References
Trace Refinement in B and Event-B
1 Introduction
2 Formal Methods B and Event-B
2.1 Refinement
2.2 ProB
3 Trace Refinement Concept
3.1 Trace Refinement in B
3.2 Trace Refinement in Event-B
4 BERT
4.1 Trace Refinement for B
4.2 Trace Refinement for Event-B
4.3 Practical Limitations and Optimizations
5 Case Studies
5.1 Pitman Arm Controller
5.2 Automotive Adaptive Exterior Light System
5.3 Threat to Validity
6 Lessons Learned
7 Related Work
8 Conclusion and Future Work
References
Model Checking B Models via High-Level Code Generation
1 Introduction and Motivation
2 Code Generation for Model Checking
2.1 Extension of Generated Code
2.2 Model Checking Features
3 Limitations of High-Level Code Generation
4 Empirical Evaluation of the Performance
5 More Related Work
6 Conclusion and Future Work
A Benchmarks
References
On Probabilistic Extension of the Interaction Theory
1 Introduction
2 Randomized Calculi and the Bisimulation
2.1 Randomized Value-Passing Calculus
2.2 Randomized C
2.3 Branching Bisimulation Congruence
3 Generalized Equality Theory
3.1 Absolute Equality for Randomized Process Models
3.2 External Characterization for =RVPC
3.3 External Characterization for =RC
4 Generalized Expressiveness Theory
4.1 Subbisimilarity for Randomized Process Models
4.2 Expressiveness of the Probabilistic Operator
4.3 Expressiveness Between Randomized Models
5 Concluding Remarks
A Proofs for Generalized Equality Theory
A.1 Proof of Theorem 1
A.2 Proof of Theorem 2
B Proofs for Generalized Expressiveness Theory
B.1 Proof of Proposition 3
References
Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages
1 Introduction
2 Preliminaries
3 Weighted Automata Extraction Scheme
3.1 Outline
3.2 Missing Rows Complementing
3.3 Context-Aware Enhancement
4 Data Augmentation
5 Experiments
6 Related Work
7 Conclusion
References
RoboCert: Property Specification in Robotics
1 Introduction
2 Related Work
3 RoboChart
4 RoboCert Sequence Diagrams
5 Well-Formedness and Semantics
5.1 Well-Formedness
5.2 Semantics
6 Tool Support
7 Conclusions
References
Formally Verified Animation for RoboChart Using Interaction Trees
1 Introduction
2 RoboChart
3 Interaction Trees
4 RoboChart Semantics in Interaction Trees
5 Code Generation, Animation, and Case Studies
6 Related Work
7 Conclusions
References
Machine-Checked Executable Semantics of Stateflow
1 Introduction
1.1 Related Work
2 A Brief Review of Stateflow
2.1 An Example of Stateflow
2.2 Stateflow Constructs
2.3 Execution Cycle of a State
3 Syntax and Semantics of Stateflow
3.1 Syntax of Stateflow Models
3.2 Configurations
3.3 Semantics
3.4 Determinism of the Semantics
4 Automatic Execution of Stateflow Charts
5 Experimental Results
6 Conclusion
References
Correction to: On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
Correction to: Chapter “On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic” in: A. Riesco and M. Zhang (Eds.): Formal Methods and Software Engineering, LNCS 13478, https://doi.org/10.1007/978-3-031-17244-1_17
Author Index