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

Description

This book constitutes the refereed proceedings of the 9th International Conference on Rigorous State-Based Methods, ABZ 2023, held in Nancy, France, in May 2023.  The 12 full and 7 short papers included in this volume were carefully reviewed and selected from 47 submissions. The proceedings also include 4 PhD symposium contributions. They deal with state-based and machine-based formal methods, mainly Abstract State Machines (ASM), Alloy, B, TLA+, VDM, and Z.  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