Santiago Romero, Research Intern, IMDEA Software Institute
Interest on runtime verification has grown in recent years and a lot of work has been focused on finding suitable formalisms to express the properties to be monitored. Many interesting properties such as correctness of procedures with respect to pre and post conditions and properties on the execution stack cannot be written in plain LTL, and a few alternatives have been presented to achieve it.
In this talk we present LOLA, a simple and expressive specification language that allows statistical information to be gathered along the trace. We also briefly describe the algorithm for online monitoring of asynchronous systems and how we extend this language to specify context and stack sensitive properties. Finally, we show how this extension of LOLA allows interesting properties to be precisely expressed by means of examples.
This is joint work with César Sánchez.