Communicating X-machines: From theory to practice

Formal modeling of complex systems is a non-trivial task, especially if a formal method does not facilitate separate development of the components of a system. This paper describes a methodology of building communicating X-machines from existing stand-alone X-machine models and presents the theory that drives this methodology. An X-machine is a formal method that resembles a finite state machine but can model non-trivial data structures. This is accomplished by incorporating a typed memory tuple into the model as well as transitions labeled with functions that operate on inputs and memory values. A set of X-machines can exchange messages with each other, thus building a communicating system model. However, existing communicating X-machines theories imply that the components of a communicating system should be built from scratch. We suggest that modeling of complex systems can be split into two separate and distinct activities: (a) the modeling of standalone X-machine components and (b) the description of the communication between these components. This approach is based on a different view of the theory of communicating X-machines and it leads towards disciplined, practical, and modular development. The proposed methodology is accompanied by an example, which demonstrates the use of communicating X-machines towards the modeling of large-scale systems.