Dealing with different time scales in formal specifications

摘要

The authors motivate the need for allowing the consistent treatment of different time scales in formal specifications of time critical systems, with the purpose of enhancing the naturalness and practical usability of the notation. The approach to this issue is illustrated on TRIO, a temporal logic language for the specification of real-time systems. The authors briefly introduce TRIO and define an extension to the language which considers a temporal universe composed of various temporal domains of different time granularity. The semantics of the extended language is defined via translation mechanisms which allow one to interpret formulas referring to a larger time granularity in a finer temporal domain, and the main properties of such translations are discussed. Finally, a complete simple example of a system specified at various levels of granularity is presented.