Developing large, distributed software systems require precise planning. From defining the system requirements and creating a more or less formal specification to the concrete implementation and testing there are many steps to go through. Software developments are usually made according to precise processes, so called life-cycles. Whether the development process is based on the waterfall, spiral or V-model the correct and safe behaviour is crucial, especially as embedded and cloud-based systems are becoming more and more popular.
The Model Driven Architecture, as a software development methodology defines guidelines and standards in order to achieve this goal, but from designing the model to formally verifying its behavioral properties several steps must be taken. These steps can be partially or completely automated by model transformations.
In my thesis, I overview several tools, every one covering a certain part of the whole process and using different modelling formalisms. This includes tools for both high-level design modelling (Yakindu Statechart Tools, MentorGraphics's BridgePoint, Papyrus) and verification (UPPAAL, VERUM's ASD:Suite) purposes.
In case of complex, distributed systems the verification of the model's behaviour is yet not so trivial. Model checker tools encounter difficulties, like state-space explosion of complex data-flow analysis even with small scale models. Therefore, abstraction layers must be introduced when transforming a design model into a formal model. A possibility to bridge the abstraction gap between the two levels, Intermediate Modelling formalisms could be introduced. In the thesis, I examine a possible approach, using the Action Language for Foundational UML (ALF) as an intermediate modelling language.