Modeling and verification of distributed real-time systems using periodic finite state machines

Finite State Machine (FSM) models are widely used to specify the operations of computer systems. Since the basic FSM model is timeless, it is not possible to model within the basic FSM framework system properties that are dependent on the progression of real time, such as the duration of computations or the limited temporal validity of real-time data. To overcome these limitations, efforts have been made to modify the FSM model to include some notion of time. It is the objective of this paper to expand existing work on basic FSMs and timed automata to include the concept of a sparse global time base as a central element of the model. We call such an extended FSM model a Periodic Finite State Machine (PFSM) model. The PFSM model incorporates the notions of state variables, global time, periodic clock constraints, and time-triggered activities. Thereby, PFSMs enable a concise and intuitive representation of distributed control systems and reduce the gap between a modeled system and its implementation.