A Proof-Based Ground Algebraic Meta-Model for Reasoning on ASTD in Event-B

Algebraic State Transition Diagram (ASTD) is a formal, graphical, state-based modeling language for the design of complex critical systems. It offers a set of process algebra operators to compose hierarchical state machines, streamlining modularity in system design. Despite advances in incorporating features such as local state variables and real time, ASTD tool support has primarily focused on design and testing. Recently, proof obligations for state invariant preservation were introduced, but the validity of these proof obligations was informally justified. To address this issue, this paper introduces an Event-B-based algebraic data-type, called EB[ASTD], formalising the operational semantics of ASTDs. Relying on a deep modelling strategy, this framework defines a ground model for the formal operational semantics of ASTDs and provides a proof-based mechanism allowing for reasoning on specific ASTDs defined as instances of this meta-model. It enables explicit manipulation of ASTD concepts and improves formal reasoning by integrating their syntax and semantics as Event- B algebraic theories. The designed tool relies on the Rodin platform to provide automated proof obligation generation, automatic and interactive verification, graphical animation, and model checking of ASTDs. In addition, it allows us to prove the validity of the generated ASTD proof obligations for state invariants, which reveals the core properties and theorems that ensure its reliability. Overall, EB[ASTD] provides a sound foundation for proving properties about ASTDs and operates effectively within the Rodin platform, designed for managing ASTD models and proofs.