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 generic computational model called timed transition systems (TTMs), an abstract 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 [Manna & Pnuelli 92], which is simpler and more concise than the floating version. To this we add the real-time semantics and proof rules for dealing with hard time systems. A decomposition theorem for modular reasoning is provided. Hierachical modular development of systems using the heuristics and the toolset is illustrated with examples, including a mutual exclusion algorithm based on time bounds and real-time resource allocation. Timing constraints need not be known a priori. The heuristics are used to derive the timing constraints that will guarantee various properties such as mutual exclusion and real-time response. The development paradigms proposed in this paper including compositional reasoning, heuristics for verifying modules or decision procedures, and the support of a graphical toolset provides a feasible approach to the systematic development of real-time reactive systems.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.