Time-constrained reactive automata: a novel development methodology for embedded real-time systems
Azer Bestavros · 1992
In this thesis we propose a treatment based on the Time-constrained Reactive Automata (TRA) model--a novel formalism suitable for the specification, validation, verification, and implementation of embedded systems. Using the TRA model, an embedded system is viewed as a set of asynchronously interacting automata (TRAs), each representing an autonomous system entity. TRAs are input enabled; they interact by signaling events on their output channels and by reacting to events signaled on their input channels. The behavior of a TRA is governed by time-constrained causal relationships between computation-triggering events. The TRA model is compositional and allows time, control, and computation non-determinism. The TRA model allows the representation of both the external environment and the programmed system along with the available computational resources in a unique framework making it possible to prove safety and liveness properties and study transient and steady state performances of embedded real-time control systems. In particular, using the TRA formalism there is no conceptual distinction between a system and a property; both are specified as formal objects. This reduces the verification process to that of establishing correspondences--preservation and implementation--between such objects. ${\cal CLEOPATRA}$ is a specification language based entirely on the TRA formalism. It features a C-like imperative syntax for the description of computation, which makes it easier to incorporate in real applications already using C; it is object-based, thus advocating modularity, reusability, and off-the shelf hierarchical programming of embedded systems. ${\cal CLEOPATRA}$ is semantically sound. In particular, its objects can be transformed, mechanically and unambiguously, into formal TRA objects for verification purposes. We have developed a compiler that allows specifications written in ${\cal CLEOPATRA}$ to be executed in simulated time, thus providing a valuable tool for validation purposes. We have used the TRA development methodology in the design, simulation, and analysis of various systems--specifically asynchronous digital circuits, sensori-motor activity management for autonomous systems, and intelligent controllers. Our experience has confirmed the suitability of this novel methodology for the specification, verification, and validation of embedded and time-critical applications. (Abstract shortened with permission of author.)