Monitor synthesis based on message sequence specification

OData support
Dr. Majzik István
Department of Measurement and Information Systems

In software development, it is extremely important to specify the requirements precisely, in order to implement and verify the application successfully. This statement is especially important at safety-critical systems, where a mistake or fault may easily lead to an accident.

One of the possible ways to detect the occurrence of runtime errors in computer systems is runtime verification. According to this method, the source code of the monitoring components (that perform the error detection) is generated based on the precisely specified requirements. The monitors observe the behavior of the running system, and signal whenever they notice an action that is not allowed by the requirements.

A proper solution for specifying requirements in an exact and intuitive way is to use message sequence charts. To monitor and verify our systems with the help of message sequence charts, we first construct an observer automaton, which signals whenever it notices a behavior that is different from the specification. The observer automaton can be used directly to generate the source code of the monitor component, which implements the actual error detection, so that we can perform the desired runtime verification.

My goal was to design and implement a tool that is able to construct the observer automaton based on the selected message sequence chart (scenario) language and then to demonstrate the systematic source code synthesis for the monitor components.


Please sign in to download the files of this thesis.