Temporal Logics for Real-Time System Specification

Lingua dei metadati

Titolo Temporal Logics for Real-Time System Specification

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

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

Descrizione 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.

Tecnico

Classificazione

IPR: informazioni

Luogo

New Menu

Related objects by text

Commenti

collection's Playback

Metadata

Azioni

Filtri di Ricerca

Contenuti

Organizza collezioni personali

Classificazione