Communicating X-machines: A practical approach for formal and modular specification of large systems

An X-machine is a general computational machine that can model: (a) non-trivial data structures as a typed memory tuple and (b) the dynamic part of a system by employing transitions, which are not labelled with simple inputs but with functions that operate on inputs and memory values. The X-machine formal method is valuable to software engineers since it is rather intuitive, while at the same time formal descriptions of data types and functions can be written in any known mathematical notation. These differences allow the X-machines to be more expressive and flexible than a Finite State Machine. In addition, a set of X-machines can be viewed as components, which communicate with each other in order to specify larger systems. This paper describes a methodology as well as an appropriate notation, namely X-machine Description Language (XMDL), for building communicating X-machines from existing stand-alone X-machine models. The proposed methodology is accompanied by an example model of a traffic light junction, which demonstrates the use of communicating X-machines towards the incremental modelling of large-scale systems. It is suggested that through XMDL, the practical development of such complex systems can be split into two separate activities: (a) the modelling of stand-alone X-machine components and (b) the description of the communication between these components. The approach is disciplined, practical, modular and general in the sense that it subsumes the existing methods for communicating X-machines.