| dc.description.abstract | In runtime verification, the behavior of a program or system is verified by automatically checking a specification expressed as a property in temporal logic on a finite execution trace.
Understanding why a property is satisfied or violated is crucial in order to identify and repair defects and refine the specification, but for long traces and complex properties this may be difficult.
Eclipse TRACE4CPS™ is an open-source tool for the visualization and analysis of timed execution traces, with functionality for verification of real-time properties in a language based on Metric Temporal Logic (MTL).
It uses informative prefix semantics to check whether the property is TRUE or FALSE, or NON-INFORMATIVE if the trace was truncated before a verdict could definitively be determined.
Intermediate values of the checking procedure can be visualized in the trace view as an explanation of the verdict.
In this thesis, the presentation of the results of runtime verification in TRACE4CPS is improved in three ways, in order to increase the understandability of verdicts.
First, the verification algorithm of TRACE4CPS is extended using a lattice-based four-valued informative prefix semantics to determine whether a NON-INFORMATIVE property is satisfied or violated so far (STILL_TRUE, STILL_FALSE).
Secondly, the explanation features are extended to allow arbitrary subformulas of the property and the real-time constraints of the temporal operators to be visualized in an interactive visual explanation process.
Finally, a method for finding the cause of LTL property violations based on Halpern and Pearl's definition of causality is extended to find the causes of timed MTL properties with FALSE or STILL_FALSE verdicts.
These are then used to generate more concise and accurate universal visual explanations of property violations. | |
