Rigorous State-Based Methods: 9th International Conference, ABZ 2023, Nancy, France, May 30–June 2, 2023, Proceedings

Preface
Organisation
Contents
Invited Papers
Refinements of Hybrid Dynamical Systems Logic
	1 Introduction
	2 Differential Dynamic Logic Ideas
	3 KeYmaera X Theorem Prover for Hybrid Systems
	4 Application Overview
	5 Conclusions and Future Work
	References
Using Deep Ontologies in Formal Software Engineering
	1 Introduction
		1.1 A Gentle Introduction into Isabelle/DOF
		1.2 The Novelty: Using HOL-Terms for Meta-data and Invariants
	2 Background
		2.1 The Isabelle/DOF Framework
		2.2 A Guided Tour Through ODL
		2.3 Term-Evaluations in Isabelle
	3 Term-Context Support, Invariants and Queries in DOF
	4 Proving Morphisms on Ontologies
	5 Related Work
	6 Conclusion and Future Work
	References
Selected Papers for Presentation and Publication
Pattern-Based Refinement Generation Through Domain Specific Languages
	1 Introduction
	2 Related Work
	3 Pattern-Based Refinement Proposals
		3.1 Introducing Counters
		3.2 Imposing Constraints on Machines
		3.3 Observation Pattern
	4 Development of the Example
	5 Conclusion
	References
Introducing Inductive Construction in B with the Theory Plugin
	1 Introduction
	2 Defining a Theory for Induction
		2.1 Rodin Theorems for Induction and Inductive Objects
		2.2 Enhancing Rodin with Theories
	3 Axiom Schema in Theory Plugin
		3.1 Axiom Schemas
		3.2 Strengths and Weaknesses
		3.3 Application to ZFC
	4 Conclusion
		4.1 Possible Rodin Improvements
		4.2 Future Work
	References
Validation of Formal Models by Interactive Simulation
	1 Introduction and Motivation
	2 Interactive Simulation
	3 VisB Diagrams
	4 Case Study
	5 Related Work
	6 Conclusion and Future Work
	References
Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems
	1 Introduction
	2 Case Study: Concurrent Hash Sets
	3 Local Proof Obligations for Invariants
	4 Local Proof Obligations for Refinement
	5 Related Work
	6 Conclusion
	References
Encoding TLA+ Proof Obligations Safely for SMT
	1 Introduction
	2 Formalizing TLA+'s Constant Fragment
	3 Encoding TLA+ for SMT
		3.1 Overview
		3.2 Recovering Formulas
		3.3 Axiomatization
	4 Evaluation
		4.1 Experiment and Results
		4.2 Discussion
	5 Conclusion
	References
Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines
	1 Introduction
	2 Motivating Example: MVM-Adapt
	3 MVM Adapt: Architecture and Models
		3.1 Adaptive Controller
		3.2 Adaptive Supervisor
	4 Related Work
	5 Conclusion
	References
Crucible Tools for Test Generation and Animation of Alloy Models
	1 Introduction
	2 Test Generation with Crucible
		2.1 Test Condition Generation
		2.2 Test Script Generation
	3 Animation with Crucible
		3.1 Animation DSL
	4 Results
	5 Conclusions and Future Work
	References
Modelling an Automotive Software System with TASTD
	1 Introduction
		1.1 TASTD
		1.2 TASTD Support Tools
		1.3 Distinctive Features of Our Modelling Approach
	2 Modelling Strategy
	3 Model Details
		3.1 Sensors ASTDs
		3.2 Actuators ASTDs
		3.3 Modelling Time Requirements
	4 Validation and Verification
	5 Specification Ambiguities and Flaws
	6 Comparison
	7 Conclusions
	References
TASTD: A Real-Time Extension for ASTD
	1 Introduction
	2 An Overview of TASTD
		2.1 Transition System
		2.2 TASTD Operators
	3 Illustrative Example
	4 TASTD Semantics
	5 Tool Support
	6 Related Work
	7 Conclusion
	References
Validation by Abstraction and Refinement
	1 Introduction
	2 Background
		2.1 Event-B
		2.2 Validation Obligations
	3 AVoiR Framework
		3.1 Step 1 - Creating an Abstraction
		3.2 Step 2 - Creating VOs
		3.3 Step 3 - Trickling Down Insights
	4 Case Study
		4.1 Abstraction
		4.2 Validating the Behavior
		4.3 Refining VOs
		4.4 Evaluation
	5 Related Work
	6 Conclusion and Future Work
	References
Verifying Event-B Hybrid Models Using Cyclone
	1 Introduction
	2 Current Architecture
	3 An Illustrative Example
	4 Experience Gained
	5 Future Direction
	References
Exploration of Reflective ASMs for Security
	1 Introduction
	2 Reflective ASMs
	3 Software to Hardware Binding Using Reflection
	4 Concluding Remarks
	References
Standalone Event-B Models Analysis Relying on the EB4EB Meta-theory
	1 Introduction
	2 Event-B
		2.1 Contexts and Machines (Tables1.a and 1.b)
		2.2 Event-B Extensions with Theories
	3 The EB4EB Framework
		3.1 The Event-B Meta-theory
		3.2 The Clock Example
		3.3 The Clock Machine as an Instance of EvtBTheo Theory
	4 POs for New Properties: Extending the Meta-theory
		4.1 Analysis Principle: New POs
		4.2 Deadlock-Freeness
		4.3 Invariant Weakness as a Non-intrusive Analysis
		4.4 Reachability
		4.5 Proof Assessment
	5 Positioning This Approach
		5.1 Related Work
		5.2 Advantages of the Approach
	6 Conclusion
	References
Adding Records to Alloy
	1 Introduction
	2 Motivating Example
		2.1 Example with the Proposed Extension
		2.2 Example in Plain Alloy
	3 Introducing Records
		3.1 Overview and Syntax
		3.2 Encoding and Semantics
		3.3 Visualization and Iteration
	4 Evaluation
	5 Conclusion
	References
Designing Critical Systems Using Hierarchical STPA and Event-B
	1 Introduction and Motivation
	2 Background
		2.1 Systems Theoretic Process Analysis (STPA)
		2.2 Event-B
		2.3 Tokeneer Case Study
	3 Overview of Systematic Hierarchical Analysis of Requirements for Tokeneer
	4 System Level
	5 Component Level
		5.1 Component Level: Door
		5.2 Component Level: Lock, Alarm, Card and Fingerprint
	6 Related Work
	7 Conclusion and Future Works
	References
Behavioural Theory of Reflective Algorithms
	1 Introduction
	2 Axiomatisation of Reflective Sequential Algorithms
	3 Reflective Sequential Abstract State Machines
	4 The Reflective Sequential ASM Thesis
	5 Concluding Remark
	References
Building Specifications in the Event-B Institution: A Summary
	1 Introduction
	2 The Institution for Event-B
	3 Refinement, Modularisation and Interoperability
	4 Conclusions and Future Work
	References
Verifying Temporal Relational Models with Pardinus
	1 Introduction
	2 A Pardinus Problem
	3 Iteration on Solutions
	4 Parallel Decomposition
	5 Evaluation
	6 Conclusion
	References
The ABZ 2023 Case Study
AMAN Case Study
	1 Introduction
	2 Overview of the AMAN Tool
		2.1 Prediction
		2.2 Spacing Requirements and Computation of a Landing Sequence
		2.3 AMAN User Interface
		2.4 Air-Traffic Controller Tasks
	3 The Landing Sequence User Interface
		3.1 AMAN Simplified User Interface
		3.2 AMAN Interaction
		3.3 Refined ATCo Tasks
	4 Requirements
		4.1 External Events
		4.2 Safety Requirements
		4.3 Automation Requirements
		4.4 Interaction Requirements
	5 Clarification Questions
	References
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations
	1 Introduction
	2 AMAN Model
	3 Verification
	4 Validation
	5 Domain-Specfic Views
	6 Lessons Learned
		6.1 VOs for Validation
		6.2 VOs in Requirement Elicitation
		6.3 VOs for Requirements Disambiguation
		6.4 Role of Verification
	7 Conclusion and Future Work
	References
Task Model Design and Analysis with Alloy
	1 Introduction
	2 Formalizing HAMSTERS with Alloy
		2.1 Structural Semantics
		2.2 Behavioral Semantics
		2.3 Composing Concrete Task Models with System Models
		2.4 Adding Erroneous Behavior
	3 The AMAN Case Study
		3.1 Task Model
		3.2 Interactive System Model
	4 Analysis of the AMAN Design
		4.1 Scenario Exploration
		4.2 Requirement Verification
	5 Related Work
	6 Conclusion
	References
Modeling and Verifying an Arrival Manager Using Event-B
	1 Introduction
	2 Event-B Method
	3 Modelling Strategy
		3.1 Control Abstraction
		3.2 Modeling Structure
		3.3 Modeling Temporal Properties
		3.4 Formalisation of the Requirements
	4 Model Details
		4.1 Machine M1
		4.2 Machine M2
		4.3 Machine M3
		4.4 Machine M5
		4.5 Machine M6
		4.6 Machine M7
	5 Validation and Verification
		5.1 Model Checking of the Specification
		5.2 Proof of the Specification
		5.3 Validation with Scenarios
		5.4 Visualisation
	6 Discussion
	7 Conclusion
	References
formal MVC: A Pattern for the Integration of ASM Specifications in UI Development
	1 Introduction
	2 The Asmeta Framework
	3 Formal Model-View-Controller
		3.1 A Simple Example: An UI for the Calculator
		3.2 Dealing with Wrong Actions
	4 The AMAN Case Study
		4.1 Formal (Asmeta) Model
		4.2 View
		4.3 Controller
	5 Discussion
	6 Related Work
	7 Conclusions
	References
Doctoral Symposium
Exploring a Methodology for Formal Verification of Safety-Critical Systems
	1 Introduction
	2 Problem Statement
	3 Proposed Methodology
		3.1 FRET-Guided Modelling
		3.2 FRET-Supported Verification
	4 Future Work
	References
Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
	1 Motivation and Problems
		1.1 Problem Domains
		1.2 Existing Workarounds and Their Issues
		1.3 Specific Problems of Any Solution
	2 Explored Solutions and Ongoing Work
		2.1 Softfloats
		2.2 Calculations with Sets
	3 Conclusion
	References
A Framework for Formal Verification and Validation of Railway Systems
	1 Context
	2 Motivation
	3 Objectives of Our Work
		3.1 Integration of the Domain Knowledge
		3.2 Extracting Safety Properties
		3.3 Specific Constraints at System Level
	4 Our Roadmap
	References
Reconstruction of TLAPS Proofs Solved by VeriT in Lambdapi
	1 Introduction
	2 Related Work
	3 Current Proposal
	4 Current Development
	References
Author Index