We present a compositional methodology for specification and proof using Interval Temporal Logic (ITL). After given an introduction to ITL, we show how fixpoints of various ITL operators provide a flexible way to modularly reason about safety and liveness. In addition, some new techniques are described for compositionally transforming and refining ITL specifications. We also consider the use of ITL's programming language subset Tempura as a tool for testing the kinds of specifications dealt with here.
CITATION STYLE
Moszkowski, B. C. (1998). Compositional reasoning using interval temporal logic and tempura. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1536, pp. 439–464). Springer Verlag. https://doi.org/10.1007/3-540-49213-5_17
Mendeley helps you to discover research relevant for your work.