Specifying reactive systems with attributed finite state machines

An attributed finite state machine (AFSM) model for the behavioral specification of reactive systems is introduced. The basic idea is to attach attributes to the states of state machines in order to express values of system data and to define attribute computation in a functional way. A specification in an AFSM consists of a collection of state transition rules. Each of these rules specifies three aspects of a reactive system: (1) the dynamic behavior, (2) the data computation and (3) the time constraints of the reactive system. The dynamic behavior is specified by state transitions responding to external stimuli, and the data computation is performed according to functional attribute definitions. The time constraints are specified operationally in terms of the temporal relations that exist between the external stimuli and the system responses. Furthermore, the hierarchy of states based on superstates and the concurrency among independent system components, are introduced according to the method of Statecharts. These mechanisms provide an effective way to decompose and specify complex systems in a structured way. To show the effectiveness of the AFSM model, an assembly system is specified with respect to the abovementioned aspects.