Run-Time Verification

Run-time verification is a method where desired or undesired properties of a system are monitored during run-time of the system. As the system is in operation, a monitor observes the trace of system and decides on-the-fly if the property holds, or does not hold, or cannot yet be decided.

Properties can be specified in different ways, but often a form of temporal logic is used. If quantitative time is relevant for the property it is a timed temporal logic. If temporal logic is used, a monitor (in software or hardware) should be generated from the logic property. For temporal logic this is usually done in the form of a finite state automaton. The construction of such an automaton is usually derived from a tableau construction to decide satisfiability of a logical formula [1][2][3].

Trace based verification can also be performed post-run-time, if a trace has been collected from the system during run-time [4].

References

  1. M. C. W. Geilen (2001): On the Construction of Monitors for Temporal Logic Properties. In: Electronic Notes in Theoretical Computer Science, vol. 55, no. 2, pp. 181-199, 2001, ISSN: 1571-0661, (RV'2001, Runtime Verification (in connection with CAV '01)).
  2. Marc Geilen and Dennis Dams (2000): An On-the-Fly Tableau Construction for a Real-Time Temporal Logic. In: Joseph, Mathai (Ed.): Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 276โ€“290, Springer Berlin Heidelberg, Berlin, Heidelberg, 2000, ISBN: 978-3-540-45352-9.
  3. Marc Geilen (2003): An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic. In: Hunt, Warren A.; Somenzi, Fabio (Ed.): Computer Aided Verification, pp. 394โ€“406, Springer Berlin Heidelberg, Berlin, Heidelberg, 2003, ISBN: 978-3-540-45069-6.
  4. Martijn Hendriks and Marc Geilen and Amir R. B. Behrouzian and Twan Basten and Hadi Alizadeh and Dip Goswami (2016): Checking Metric Temporal Logic with TRACE. In: 2016 16th International Conference on Application of Concurrency to System Design (ACSD), pp. 19-24, 2016.

Selected Related Publications

2016

Hendriks, Martijn; Geilen, Marc; Behrouzian, Amir R. B.; Basten, Twan; Alizadeh, Hadi; Goswami, Dip

Checking Metric Temporal Logic with TRACE Proceedings Article

In: 2016 16th International Conference on Application of Concurrency to System Design (ACSD), pp. 19-24, 2016.

Links | BibTeX

2003

Geilen, Marc

An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic Proceedings Article

In: Hunt, Warren A.; Somenzi, Fabio (Ed.): Computer Aided Verification, pp. 394โ€“406, Springer Berlin Heidelberg, Berlin, Heidelberg, 2003, ISBN: 978-3-540-45069-6.

BibTeX

2002

Geilen, M. C. W.

Formal techniques for verification of complex real-time systems PhD Thesis

Electrical Engineering, 2002, ISBN: 90-386-1930-8.

Links | BibTeX

2001

Geilen, M. C. W.

On the Construction of Monitors for Temporal Logic Properties Journal Article

In: Electronic Notes in Theoretical Computer Science, vol. 55, no. 2, pp. 181-199, 2001, ISSN: 1571-0661, (RV'2001, Runtime Verification (in connection with CAV '01)).

Links | BibTeX

2000

Geilen, Marc; Dams, Dennis

An On-the-Fly Tableau Construction for a Real-Time Temporal Logic Proceedings Article

In: Joseph, Mathai (Ed.): Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 276โ€“290, Springer Berlin Heidelberg, Berlin, Heidelberg, 2000, ISBN: 978-3-540-45352-9.

BibTeX