Formal refinement of extended state machines

TL;DR

This paper introduces a methodology combining graphical ASTD notation with Event-B formal specifications to improve understanding and refinement of system behavior, demonstrated through a railway case study.

Contribution

It proposes a novel coupling of ASTD with Event-B for incremental refinement, enhancing readability and proof management in formal system development.

Findings

Improved readability of formal specifications.

Reduced proof complexity through combined notation.

Effective case study validation with railway system.

Abstract

In a traditional formal development process, e.g. using the B method, the informal user requirements are (manually) translated into a global abstract formal specification. This translation is especially difficult to achieve. The Event-B method was developed to incrementally and formally construct such a specification using stepwise refinement. Each increment takes into account new properties and system aspects. In this paper, we propose to couple a graphical notation called Algebraic State-Transition Diagrams (ASTD) with an Event-B specification in order to provide a better understanding of the software behaviour. The dynamic behaviour is captured by the ASTD, which is based on automata and process algebra operators, while the data model is described by means of an Event-B specification. We propose a methodology to incrementally refine such specification couplings, taking into account new refinement relations and consistency conditions between the control specification and the data specification. We compare the specifications obtained using each approach for readability and proof complexity. The advantages and drawbacks of the traditional approach and of our methodology are discussed. The whole process is illustrated by a railway CBTC-like case study. Our approach is supported by tools for translating ASTD's into B and Event-B into B.