Temporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.
|Journal||Electronic Notes in Theoretical Computer Science|
|Publication status||Published - 2001|
|Event||RV'01-First Workshop on Runtime Verification - Paris, France|
Duration: 23 Jul 2001 → 23 Jul 2001
Bibliographical notePart of special issue:
RV'2001, Runtime Verification (in connection with CAV '01)
Edited by Klaus Havelund, Grigore Rosu