Temporal Logics for Real-Time System Specification

Metadata languages

Title Temporal Logics for Real-Time System Specification

Subject real time systems specification, formal methods, tilco, uml

Description real time systems specification, formal methods, tilco, uml

Description The specification of reactive and real-time systems must be supported by formal mathematically founded methods to be satisfactory and reliable Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formulae including temporal constraints, events, and the relationships between the two. In the last years, temporal logics have reached a high degree of expressiveness, Most of the temporal logics proposed in the last few years can be used for specifying of reactive systems, although not all are suitable for specifying real time systems. In this paper, we present a series of criteria for assessing the capabilities of temporal logics for the specification, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness. the logic's order, the presence of a metric for time, the type of temporal operators, the fundamental time entity, and the structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer a set of typical specifications has been identified and used with most of the temporal logics considered, thus presenting the reader with a number of real examples.

Technical

Classification

IPR information

Location

New Menu

Related objects by text

Comments

collection's Playback

Metadata

Actions

Search Filter

Content

Organize Personal Collection

Classification