Rigorous State-Based Methods : 9th International Conference, ABZ 2023, Nancy, France, May 30–June 2, 2023, Proceedings / edited by Uwe Glässer, Jose Creissac Campos, Dominique Méry, Philippe Palanque.

Format:

Book

Author/Creator:

Glässer, Uwe.

Contributor:

Creissac Campos, Jose.

Méry, Dominique.

Palanque, Philippe.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 14010

Language:

English

Subjects (All):

Machine theory.

Formal Languages and Automata Theory.

Local Subjects:

Formal Languages and Automata Theory.

Physical Description:

1 online resource (386 pages)

Edition:

1st ed. 2023.

Place of Publication:

Cham : Springer Nature Switzerland : Imprint: Springer, 2023.

Summary:

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. .

Contents:

Pattern-based Refinemnt Generation Through Domain Specifi Languages

Inductive Construction in B with the Theory Plugin

Validation of Formal Models by Interactive Simulation

Thread-Local, Step-Local Proof Obligations for Refnement of State-Based Concurrent Systems

Encoding TLA+ Proof Obligations Safely for SMT

Compositional I/O Abstract State Machines

Crucible Tools for Test Generation and Animation of Alloy Models

Modelling an Automotive Software System with TASTD

TASTD a real-time extension for ASTD

Validation by Abstraction and Refiement

Verifying Event-B Hybrid Models using Cyclone

Exploration of Reflectie ASMs for Security

Standalone Event-B models analysis relying on the EB4EB meta-theory

Adding records to Alloy

Designing Secure Systems using Hierarchical STPA and Event-B

Behavioural Theory of Reflectie Algorithms

Specification in the Event-B Institution

Verifying temporal relational models with Pardinus

AMAN Case Study

Analysis of a Safety-critical Interactive System through VOs

Task Model Design and Analysis with Alloy

Modeling and Verifying an Arrival Manager using Event-B

Formal MVC: a Pattern for the Integration of ASM Specification in UI Development

Exploring a methodology for formal verificatio of safety-critical systems

Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems

A framework for formal verificatio and validation of railway systems

Reconstruction of TLAPS proofs solved by veriT in Lambdapi.

Notes:

Description based on publisher supplied metadata and other sources.

Other Format:

Print version: Glässer, Uwe Rigorous State-Based Methods

ISBN:

9783031331633

OCLC:

1379238051