|Thesis abstract: |
The Unified Modeling Language (UML) is a general-purpose platform-independent modeling language, created and managed by the Object Management Group (OMG). UML has transformed from a relatively basic descriptive tool to a sophisticated prescriptive one that can be used to specify, analyze and implement complex software systems. UML offers a heterogeneous set of diagrams to describe the different views of a software system during the Model-Driven Development (MDD) process.
Model defects are a significant concern in the Model-Driven Development paradigm, as model transformations and code generation may propagate errors to other notations where they are harder to detect and trace. There are formal verification techniques that can check the correctness of models. Verification results often reveal unexpected behaviors in the models, which if left unresolved, may lead to a tremendous cost in the later stages of the development.
A problem in formal verification techniques is that their high computational complexity can limit their scalability. The main goal of this research is to enable formal verification techniques to deal with big-scale models in a more efficient way. There exist some techniques that improve scalability of formal verification techniques by partitioning the original model into submodels and verifying them independently. But they consider only static structure of the system. This research aims to verify both static structure and dynamic behavior of the system.