Runtime verification based on sequence diagrams

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

The number and the responsibility of the IT systems around us are increasing day by day. In the other hand, these systems’ size and complexity are increasing too. For this reasons, there is bigger demand to develop tools, which provide a simply way for the software engineers to specify and check the requirements of the systems in formal form.

While solving this issue, the model-driven software development comes to the fore. During the using this way of developing, the developers can create some kinds and levels of system’s model, and after that they can generate code from the models. It is possibly to carry out inspections just on the models in the model-driven development, which means more reliability.

For safety-critical systems, runtime verification is more and more often is used, which is able to explore the fault of planning and implementation too. If needed, it can stop of modify the behaviour of the system.

My purpose in my thesis is to develop a runtime verification supporter tool, which is a good fit for the model-driven development. There are more technology and standard is already available for this goals, and many of them are widespread. I implemented a tool with the using and connecting this things, that is provides to specify the requirements of the system in a high level of formalism, named UML sequence diagram. From this high level formalism, it generates the C++ code of an automaton with ability to runtime verification in more iteration steps.

Fort the implementation of these, more constraints was needed to add to sequence diagrams. Some part of them I determined based on the algorithm, which I reused and supplemented.

I am going to present the usability of my tool with a case study at the end of my thesis.


Please sign in to download the files of this thesis.