Specifying and Verifying Real-Time Re-active Systems in TTM/RTTL

from: ftp.cs.yorku.ca:/pub/TECH-REPORTS Abstract: TTM/RTTL is a comprehensive framework for the specification, development and verification of real-time reactive programs and devices found in embedded, safety critical, or concurrent systems. The framework consists of a specification language called real-time temporal logic (RTTL), and a sound and relatively complete proof system and proof methodology. The framework has heuristics, which have been mechanized using constraint logic, for aiding the designer in the systematic development of infinite state systems, and decision procedures for automatic verification of finite state systems. A toolset called StateTime provides automated support for visual specification, simulation and verification in the framework. The original version of RTTL was based on the floating version of temporal logic for fair transition systems. In this paper, we recast RTTL in the anchored framework of Manna and Pnueli [21], which is simpler and more concise than th