Specification of a Gas Station using a Formalism Integrating Formal Datatypes within State Diagrams

In this paper, we propose a generic approach for inte-grating datatypes expressed using formal specification lan-guages within state diagrams. Our main motivations are (i) to be able to model dynamic aspects of complex systems with graphical user-friendly languages, and (ii) to be able to specify in a formal way and at a high abstraction level the datatypes pertaining to the static aspects of such sys-tems. The dynamic aspects may be expressed using state diagrams (such as UML or SDL) and the static aspects may be expressed using either algebraic specifications or state oriented specifications (such as Z or B). Our approach in-troduces a flexible use of datatypes. It also may take into ac-count different semantics for the state diagrams. We herein focus on a case study to demonstrate the pragmatism of our approach