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
N° accessi 576
Formato document
Tipo pdf
Accessibile sulle piattaforme PC, iPhone/iPad, Android, Windows Phone 7