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].
Selected Related Publications
-
![[DOI]](https://computationalmodeling.info/wp/wp-content/plugins/papercite/img/external.png)
M. C. W. Geilen, “On the construction of monitors for temporal logic properties,” Electronic notes in theoretical computer science, vol. 55, iss. 2, pp. 181-199, 2001.
[Bibtex]@article{Gei01, title = {On the Construction of Monitors for Temporal Logic Properties}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {55}, number = {2}, pages = {181-199}, year = {2001}, note = {RV'2001, Runtime Verification (in connection with CAV '01)}, issn = {1571-0661}, doi = {https://doi.org/10.1016/S1571-0661(04)00252-X}, url = {https://www.sciencedirect.com/science/article/pii/S157106610400252X}, author = {M.C.W. Geilen} } - M. Geilen and D. Dams, “An on-the-fly tableau construction for a real-time temporal logic,” in Formal techniques in real-time and fault-tolerant systems, Berlin, Heidelberg, 2000, p. 276–290.
[Bibtex]@InProceedings{GD00, author="Geilen, Marc and Dams, Dennis", editor="Joseph, Mathai", title="An On-the-Fly Tableau Construction for a Real-Time Temporal Logic", booktitle="Formal Techniques in Real-Time and Fault-Tolerant Systems", year="2000", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="276--290", isbn="978-3-540-45352-9" } - M. Geilen, “An improved on-the-fly tableau construction for a real-time temporal logic,” in Computer aided verification, Berlin, Heidelberg, 2003, p. 394–406.
[Bibtex]@InProceedings{Gei03, author="Geilen, Marc", editor="Hunt, Warren A. and Somenzi, Fabio", title="An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic", booktitle="Computer Aided Verification", year="2003", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="394--406", isbn="978-3-540-45069-6" }
References
[1] M. C. W. Geilen, “On the construction of monitors for temporal logic properties,” Electronic notes in theoretical computer science, vol. 55, iss. 2, pp. 181-199, 2001.
[Bibtex]
M. C. W. Geilen, “On the construction of monitors for temporal logic properties,” Electronic notes in theoretical computer science, vol. 55, iss. 2, pp. 181-199, 2001. [Bibtex]
@article{Gei01,
title = {On the Construction of Monitors for Temporal Logic Properties},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {55},
number = {2},
pages = {181-199},
year = {2001},
note = {RV'2001, Runtime Verification (in connection with CAV '01)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/S1571-0661(04)00252-X},
url = {https://www.sciencedirect.com/science/article/pii/S157106610400252X},
author = {M.C.W. Geilen}
}[2] M. Geilen and D. Dams, “An on-the-fly tableau construction for a real-time temporal logic,” in Formal techniques in real-time and fault-tolerant systems, Berlin, Heidelberg, 2000, p. 276–290.
[Bibtex]
[Bibtex]
@InProceedings{GD00,
author="Geilen, Marc
and Dams, Dennis",
editor="Joseph, Mathai",
title="An On-the-Fly Tableau Construction for a Real-Time Temporal Logic",
booktitle="Formal Techniques in Real-Time and Fault-Tolerant Systems",
year="2000",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="276--290",
isbn="978-3-540-45352-9"
}[3] M. Geilen, “An improved on-the-fly tableau construction for a real-time temporal logic,” in Computer aided verification, Berlin, Heidelberg, 2003, p. 394–406.
[Bibtex]
[Bibtex]
@InProceedings{Gei03,
author="Geilen, Marc",
editor="Hunt, Warren A.
and Somenzi, Fabio",
title="An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic",
booktitle="Computer Aided Verification",
year="2003",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="394--406",
isbn="978-3-540-45069-6"
}[4] M. Hendriks, M. Geilen, A. R. B. Behrouzian, T. Basten, H. Alizadeh, and D. Goswami, “Checking metric temporal logic with trace,” in 2016 16th international conference on application of concurrency to system design (acsd), 2016, pp. 19-24.
[Bibtex]
M. Hendriks, M. Geilen, A. R. B. Behrouzian, T. Basten, H. Alizadeh, and D. Goswami, “Checking metric temporal logic with trace,” in 2016 16th international conference on application of concurrency to system design (acsd), 2016, pp. 19-24. [Bibtex]
@INPROCEEDINGS{HGBea16,
author={Hendriks, Martijn and Geilen, Marc and Behrouzian, Amir R. B. and Basten, Twan and Alizadeh, Hadi and Goswami, Dip},
booktitle={2016 16th International Conference on Application of Concurrency to System Design (ACSD)},
title={Checking Metric Temporal Logic with TRACE},
year={2016},
volume={},
number={},
pages={19-24},
doi={10.1109/ACSD.2016.13}
}