Real-Time Interactions: An Abstract Notation for Specifying and Analysing the Timing Properties of Real-Time Systems

摘要

It is difficult to characterize, and analyze the consistency of, the temporal requirements of real-time systems. This paper describes a notation, called Real-time Interactions, which supports the description of abstract system models and their timing constraints early in the development process. A semantic for the notations is given in CSP enabling system properties to be explored using the FDR2 model checker. The utility of the notations has been demonstrated by model checking properties of a fragment of a design of an air launched missile system.