The complexity of IT and safety-critical systems has increased rapidly in recent years. In the field of software engineering, this led to the increasing number of lines of source code. For example, on an Airbus A380 airplane several million lines of code are responsible for the safety of the passengers. In addition, the rich functional requirements necessitates the development of distributed systems to be able to handle complexitiy and provide efficiency.
Therefore in the latest years the model-based approach became an important paradigm in the field of distributed and safety-critical systems. The goal of this approach is to provide a means to develop models and automatize the the generation of the implementation from the high level models.
Testing and analyzing the correct behavior of such systems with the conventional approaches usually requires big amount of manual effort. However, the model-driven approach can also provide means to apply formal methods that allows the discovery of both design and behavioral errors in an early stage of development.
In my thesis I overview the model based systems engineering, focusing on the xtUML language that provides a state-machine based approach. The usability of the language is demonstrated with a distributed railway-control safety-critical case study. The design models are transformed into formal models, so the correctness of the models are verified using temporal logic expressions by a widely used formal model checker framework called UPPAAL.