| Summary: | Model transformations are programs that generate models or code from models. When model transformations are used in software development, the correctness of these programs is very important, thus , they need to be verified. Verifying model transformations is even more important when model transformations are used to develop safety- or mission-critical systems. There are many issues that make verifying model transformations a challenging task such as the difficulty in generating test models and test oracles, and the challenge of proposing approaches that are applicable to model transformations written in different types of languages. This research proposes an approach known as IMCAT to verify model transformations by model checking the output model/code. This approach automatically annotates the generated output with assertions and verifies properties by checking these assertions. Using this indirect method allows the approach to be used to verify different model transformations, regardless of the language used to write them. Verifying a model transformation indirectly is also less complex than direct verification because the latter requires the translation of the transformation language, models and metamodels into a format that can be checked by the model checker. Furthermore, technologies for model checking models/code are well-established. However, IMCAT also has a problem with state space explosion, which is a well-known limitation when model checking complex models and code. This research addresses this issue by proposing heuristics to select suitable state space reduction techniques from models and design patterns. The selected reduction technique is later used to reduce the state space of the system being model checked. The verification approach is evaluated by verifying two commercial UML State Machine-to-Java code generators to demonstrate that IMCAT can verify code generators developed in different languages. The approach also comes with guidelines to select suitable state space reduction techniques from UML models and behavioural design patterns. Using three systems as case studies, these heuristics are evaluated by model checking the three large systems using the selected reduction techniques. The result shows that the state space of each system is reduced, thus, concluding that the selected techniques are suitable and the heuristics to select them are appropriate.
|
|---|
