Reactive system represents a broad class of real complex systems that are frequently found in daily life. Due to the complex nature of reactive systems, investigating formal methods for their behavior specification presents real challenges....[ Read more ]

Reactive system represents a broad class of real complex systems that are frequently found in daily life. Due to the complex nature of reactive systems, investigating formal methods for their behavior specification presents real challenges.

Traditional method for specifying such systems is by the 'state-events' approach. Finite State Machine (FSM) is a classical model that is mostly adopted. However, the capabilities of FSM is limited, especially when practical complicated systems have to be modelled.

In this thesis, an extended FMS called ACHE-FSM is proposed. This new model has the capability to specify complex systems with concurrent constructs in a hierarchical and modular fashion. As a result, a structural and effective specification of complex reactive systems can be achieved.

Moreover, a new logic grammar is described for studying the dynamic behaviors and performing analysis on reactive systems. It is called Constraint Narrowing Grammar (CNG). CNG combines concepts from logic programming, rewriting and lazy evaluation. The non-deterministic and non-terminating properties of CNG make it a nice formalism to model infinite behaviors of reactive systems.

We show that there is a direct mapping from ACHE-FSM to CNG. Through the mapping, a programming language semantics can be provided to the model. The resulting grammar is hence an executable behavioral specification as well as an analytic tool for ACHE-FSM.