Dealing with different time scales in formal specifications
- 9 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We 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. Our approach to this issue is illustrated on TRIO, a temporal logic language for the specification of Real-Time systems. We 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 us to interpret formulas referring to a larger time granularity in a finer temporal domain, and the main properties of such translations are discussed. Finally we present a complete simple example of a system specified at various levels of granularity.Keywords
This publication has 12 references indexed in Scilit:
- Introduction to the ISO specification language LOTOSPublished by Elsevier ,2003
- TRIO, a logic formalism for the specification of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A methodology for an incremental, logical specification of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Dealing with different time granularities in formal specifications of real-time systemsReal-Time Systems, 1991
- A unified high-level Petri net formalism for time-critical systemsIEEE Transactions on Software Engineering, 1991
- TRIO: A logic language for executable specifications of real-time systemsJournal of Systems and Software, 1990
- Statecharts: a visual formalism for complex systemsScience of Computer Programming, 1987
- Principles of OBJ2Published by Association for Computing Machinery (ACM) ,1985
- Testing Formal Specifications to Detect Design ErrorsIEEE Transactions on Software Engineering, 1985
- A Methodology for the Design and Implementation of Communication ProtocolsIEEE Transactions on Communications, 1976