Rigorous State-Based Methods : 10th International Conference, ABZ 2024, Bergamo, Italy, June 25–28, 2024, Proceedings / edited by Silvia Bonfanti, Angelo Gargantini, Michael Leuschel, Elvinia Riccobene, Patrizia Scandurra.

Format:

Book

Contributor:

Bonfanti, Silvia, editor.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 14759

Language:

English

Subjects (All):

Machine theory.

Computer engineering.

Computer networks.

Application software.

Logic programming.

Compilers (Computer programs).

Formal Languages and Automata Theory.

Computer Engineering and Networks.

Computer and Information Systems Applications.

Logic in AI.

Compilers and Interpreters.

Local Subjects:

Formal Languages and Automata Theory.

Computer Engineering and Networks.

Computer and Information Systems Applications.

Logic in AI.

Compilers and Interpreters.

Physical Description:

1 online resource (404 pages)

Edition:

1st ed. 2024.

Place of Publication:

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

Summary:

This book constitutes the refereed proceedings of the 10th International Conference on Rigorous State-Based Methods, ABZ 2024, held in Bergamo, Italy, during June 25–28, 2024. The 29 papers included in this volume were carefully reviewed and selected from 47 submissions. They were organized in topical sections as follows: research papers; short research papers; case study; doctoral symposium.

Contents:

1 Invited Talk

Formal Methods and Tools Applied in the Railway Domain

2 Research Papers

Formal Modeling and Analysis of Apache Kafka in Alloy 6

Event-B Development of Modelling Human Intervention Request in Self- Driving Vehicle Systems

Alloy Goes Fuzzy

Transpilation of Petri-nets into B: Shallow and Deep Embeddings

A Lean Reflective Abstract State Machine Definition

Loose Observation in Event-B

Modal Extensions of the Logic of Abstract State Machines

An Analysis of the Impact of Field-Value Instance Navigation in Alloy’s Model Finding

From Concept to Code: Unveiling a Tool for Translating Abstract State Machines into Java Code

3 Short Research Papers

An Event-B Formal Model for Access Control and Resource Management of Serverless Apps

Property Ownership Formal Modelling Using Event-B and iUML-B

A Modeling and Verification Framework for Ethereum Smart Contracts

Semantics Formalisation – From Event-B Contexts to Theories

Using Symbolic Execution to Transform Turbo Abstract State Machines into Basic Abstract State Machines

Multi-model Animation with Jeb

Meta-Programming Event-B: Advancing Tool Support and Language Extensions

Event-B as DSL in Isabelle and HOL

ThoR: An Alloy5-based DSL for Interactive Theorem Proving in Coq

Verifying HyperLTL properties in Event-B

Small Step Incremental Verification of Compilers

Designing Exception Handling using Event-B

4 Case Study

The Mechanical Lung Ventilator Case Study

Real-Time CCSL: Application to the Mechanical Lung Ventilator

An Event-B Model of a Mechanical Lung Ventilator

Modelling the Mechanical Lung Ventilation System using TASTD

Modelling and Analysing a Mechanical Lung Ventilator in mCRL2

FRETting and Formal Modelling: A Mechanical Lung Ventilator

5 Doctoral Symposium

From Event-B to Lambdapi

Proof Construction and Checking on Evolving Abstract State Machines .

Notes:

Includes bibliographical references and index.

ISBN:

3-031-63790-9