Communicating reactive state machines : design, model and implementation

This paper proposes a language, called Communicating Reactive State Machines (CRSM), useful for describing behaviors of real-time distributed controllers. The characteristic features of this language are that it has a pictorial syntax, a precise formal semantics and an efficient implementation. CRSM is based on Argos, a language proposed for centralized real-time controllers. Argos is extended by including a primitive for communication between Argos programs. This communication primitive is based upon the communication primitive of CSP. A precise mathematical model, called communicating boolean automata (CBA) based upon the boolean automata model of Argos is developed, A number of operations over CBA have been defined to model the constructs of CRSM and a notion of bisimulation equivalence is also defined. CBA would form the basis for automatic verification of CRSM. An outline of an implementation of CRSM is also given. Copyright (C) 1998 IFAC