ABZ'21

ABZ 2021 (Ulm, Germany)

8th International Conference on Rigorous State-Based Methods

A Modeling and Verification Framework for Security Protocols

Abstract Bad design decisions in security protocols can drastically affect the robustness of the protection given by protocols, causing the introduction of vulnerabilities and leak of information. My PhD project aims to reduce the possibility of introducing flaws supporting designers and engineers with a user-friendly formal verification framework, with various options for both model construction and verification.

About the Concolic Execution and Symbolic ASM Function Promotion in CASM

Abstract Abstract State Machines (ASMs) are a well-known state based formal method to describe systems at a very high level and can be executed either through a concrete or symbolic interpretation.

Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application

Abstract Digitalisation and innovation among the railway systems entail effort-demanding challenges, especially when considering how crucial it is to verify safety requirements and proof security levels. The early Verification and Validation (V&V) of railway systems detect critical issues and avoid severe consequences due to software failure.

Event-B Formalization of Event-B Contexts

Abstract This paper presents an Event-B meta-modelisation of an Event-B project restricted to its context hierarchy which introduces the functional part of a development through sets, constants, axioms and theorems. We study the proposal of a new mechanism for Event-B.

Extending ASMETA with Time Features

Abstract ASMs and the ASMETA framework can be used to model and analyze a variety of systems, and many of them rely on time constraints. In this paper, we present the ASMETA extension to deal with model time features.

Extensible Record Structures in Event-B

Abstract Event-B is a state-based formal method for system development. The Event-B mathematical language does not support a syntax for the direct definition of structured types such as records. This paper proposes extending the Event-B language with direct record definitions.

Formal Meta Engineering Event-B: Extension and Reasoning The EB4EB Framework

Abstract State-based Formal methods have been used to design and verify the development of complex software systems for a long time. Such methods are underpinned with solid mathematical concepts. Document If you cannot see the document below, the PDF document is most likely not freely accessible.

Formalizing and Analyzing System Requirements of Automatic Train Operation over ETCS Using Event-B

Abstract The European Railway Traffic Management System (ERTMS) aims at the replacement of incompatible national railway traffic management systems in Europe. A part of ERTMS is the European Train Control System (ETCS).

Formalizing the Institution for Event-B in the Coq Proof Assistant

Abstract We formalize a fragment of the theory of institutions sufficient to establish basic facts about the institution for Event-B, and its relationship with the institution for first-order predicate logic. We prove the satisfaction condition for and encode the institution comorphism embedding in .

Proving the Safety of a Sliding Window Protocol with Event-B

Abstract This paper presents an Event-B modeling of the general version of the Sliding Window Protocol (SWP). SWPs ensure reliable data transfer over unreliable media by routing frames together with their indexes.

Sterling: A Web-Based Visualizer for Relational Modeling Languages

Abstract We introduce Sterling, a web-based visualization tool that provides interactive views of relational models and allows users to create custom visualizations using modern JavaScript libraries like D3 and Cytoscape. We outline its design goals and architecture, and describe custom visualizations developed with Sterling that enable verification studies of scientific software used in production.

The CamilleX Framework for the Rodin Platform

Abstract We present the CamilleX framework for the Rodin platform in this paper. The framework provides a textual representation and persistence for the Event-B modelling constructs. It supports direct extensions to the Event-B syntax such as machine inclusion and record structures, as well as indirect extensions provided by other plugins such as UML-B diagrams.

Towards ASM-Based Automated Formal Verification of Security Protocols

Abstract In the security protocols domain, formal verification is more and more highly demanded to guarantee security assurance: humans increasingly depend on the use of connected devices in their daily life, so they must be protected against possible threats and accidents.

Towards Refinement of Unbounded Parallelism in ASMs Using Concurrency and Reflection

Abstract The BSP bridging model can be exploited to support MapReduce processing. This article describes how this can be realised using a work-stealing approach, where an idle processor can autonomously grab a thread from a partially ordered pool of open threads and execute it.

Unbounded Barrier-Synchronized Concurrent ASMs for Effective MapReduce Processing on Streams

Abstract MapReduce supports the processing of large data sets in parallel. It has been shown that MapReduce is an example for the use of the bulk synchronous parallel (BSP) bridging model, a model for parallel computation on a fixed set of processors comprising alternating computation and communication phases.

Validation of Formal Models by Timed Probabilistic Simulation

Abstract The validation of a formal model consists of checking its conformance with actual requirements. In the context of (Event-) B, some temporal aspects can typically be validated by LTL or CTL model checking, while other properties can be validated via interactive animation or trace replay.

Verifying System-Level Security of a Smart Ballot Box

Abstract Event-B, a refinement-based formal modelling language, has traditionally focused on safety, but now increasingly finds a new role in developing secure systems. In this paper we take a fresh look at security and focus on what security means for the system rather than looking at detailed protocols.

Adaptive Exterior Light and Speed Control System (ABZ 2020)

This document describes two systems from the automotive domain: an adaptive exterior light system (ELS) and a speed control system (SCS). This specification is based on the SPES XT running example.