Statechart based monitor generation for C++ environments

OData support
Supervisor:
Vörös András
Department of Measurement and Information Systems

The aim of this work is to present a method for the generation of runtime monitoring components from the statechart language of the theta frontend, and give an example implementation in the form of an Eclipse plugin.

Safety critical software engineering employs methods that try to eliminate implementation errors which could lead to faulty behaviour, and minimize the impact of a hardware component’s breakdown. To avoid design and implementation errors, developers can use formal verification of (formally described) requirements. The handling of hardware errors can also be incorporated in the models themselves - however, this leads to larger models and reduces the abstraction of the system, making the verification process more complex (if it can be verified at all). Another possible solution to handling errors is to use runtime monitoring components - components that monitor properties of the system which can be used to detect potentially erroneous behaviour. Should malfunctions be detected, the monitoring component can take steps to minimize the impact of the malfunction.

The work presented in this thesis extends the toolkit of developers by providing a solution for the generation of low level, memory and CPU efficient monitoring components, using a statechart formalism. Some of their use cases could include reporting or recording of observable variables, signaling the current state of the system, or adding an extra layer of safety logic -- with low development overhead.

Statecharts were chosen as most engineers are already familiar with their formalism, and they are abstract enough to allow a compact but meaningful description of systems. The statechart language of the Theta frontend is close to the one described in the UML standard - with a moderate amount of extensions and a few limitations. C++ allows the monitors to run in resource restricted environments while maintaining code readability. To assess the performance of the generated monitors, measurements were also made, using models from a few dozen to a few thousand states and transitions.

Downloads

Please sign in to download the files of this thesis.