Description

Safety-critical software systems are required to satisfy the timing constraints. Otherwise, this may lead to unwanted behavior which can result in critical consequences such as human casualties. Verification of the required timing properties of these systems is therefore important.

Timed automata can be used to model and analyze the timing behavior of real-time systems. One of the major challenges of model-checking is to obtain models detailed enough to express  the essential features of the system. Too detailed models may lead to state-explosion problem in model checkers. Therefore, it is very important to find the correct abstraction level.

In TIPS project, we have a model-driven tool framework to derive timed-automata models from Java source code. The framework can be extended with additional transformations on the intermediate models or even with new model types to get more useful and convenient timed-automata models for model checking such as models that generate feasible state space.

The aim of this master-bachelor project is to develop a method and related tool support in this framework to allow one to customize the abstraction level of the derived models.
 
Tasks:
- Proposing a method to customize the abstraction detail of derived models from the source code.
- Implementing the required tool support for this method to help the end-user/programmer.

Offerings:

- You will have an experience model-driven software engineering with most recent tools,
- You will learn about underlying mechanisms of Java source code, such as byte-code, JVM.