Synchronous stream runtime verification with uncertainties and assumptions

@mastersthesis {1480,
	title = {Synchronous stream runtime verification with uncertainties and assumptions},
	volume = {Doctoral Thesis},
	year = {2024},
	month = {09/2024},
	pages = {xv, 231 pages},
	type = {Doctoral Thesis},
	address = {L{\"u}beck},
	abstract = {<p>Runtime verification (RV) is a technique from the field of formal methods that aims at monitoring system executions for verification purposes. In particular, a so-called monitor is used, which evaluates a run of the system under scrutiny either at runtime (online monitoring) or afterwards (offline monitoring). The monitors used for this purpose are usually not programmed in a conventional way, but rather synthesized from a specification of the property to be monitored. A particular challenge, however, is that the specification languages used, do not directly provide a strategy to evaluate the specification, e.g. if the described properties depend on future events in the system. To produce optimal results, an online monitor would then require a strategy to consider all possible extensions of the current system execution. Also, the capabilities of a monitor often go beyond a simple evaluation of a given property over a fully observable system execution. For example, there may be so-called uncertainties, i.e. points in the execution where the monitor does not have access to exact data values, e.g. because sensors have failed or provide inaccurate measurements. There may also be additional knowledge about the monitored system or its environment, called assumptions. Taking these into account during monitoring can often lead to more accurate monitoring results. This thesis studies monitoring of synchronous properties, in the presence of uncertainties and assumptions. Synchronous properties are those that assign a property value to each monitor input, but not to the points in time between these inputs. In the thesis, the following aspects are addressed: First, a definition of synchronous properties is worked out, together with a notion of sound and perfect monitoring in various versions. Besides, it is shown how the stream runtime verification language LOLA can be used as a general formalism for synchronous properties. Building on this, a general framework for efficient online monitoring of LOLA specifications in the presence of uncertainties and assumptions and a concrete instantiation based on symbolic reasoning is presented. In particular, the thesis discusses how the framework can be used to show when perfect monitoring of certain LOLA fragments is possible and how to construct such monitors. The theory presented is essentially based on foundations from the field of abstract interpretation. Finally, three case studies and an implementation of the symbolic monitoring technique are used to demonstrate concrete application scenarios of the presented method. In addition, the potentials as well as shortcomings and possible extensions of the approach are discussed.</p>
},
	keywords = {Assumptions, Framework, Runtime verification, Symbolic Reasoning, Uncertainty},
	url = {https://epub.uni-luebeck.de/items/3de69933-574d-440e-afe3-d6b4c567642e},
	author = {Hannes Kallwies}
}