Specification of Real-Time Systems


Activation-Oriented Specification of Real-Time Systems

Vered Gafni, Amiram Yehudai, and Yishai A. Feldman
Dept. of Computer Science
Tel Aviv University
69978 Tel Aviv, Israel

Appeared in: Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Lübeck, Germany, 19-23, September 1994


We present MASS, a declarative language for specifying the reactive behavior of real-time systems. The basic primitive of the language is the task, which is the interface between the reactive and sequential aspects of the specification. The purely computational meaning of a task (as an I/O transformation) is given outside MASS using standard specification languages for sequential computations. The reactive aspects of real-time systems are expressed in MASS through causal and temporal relations between events that signal task terminations. Hierarchical systems are obtained by refining tasks, specifying them as sub-systems in MASS.

MASS is given a formal semantics in a trace model augmented with explicit representation of causes. A synchronous execution model conforming with the formal semantics makes MASS specifications executable. A development system based on this model allows both simulation of (possibly incomplete) specifications and the generation of complete target applications (given code for the sequential computations of tasks). We have successfully used MASS in a case study involving several robots and a complex conveyer system.