Language Specific Analysis of State Machine Models of Reactive Systems
software analysis , model checking , Model Driven Development , software engineering
Model Driven Development (MDD) is a paradigm introduced to overcome the complexities of modern software development. In MDD we use models as a primary artifact that is being developed, tested and refined, with code being a result of code generation. Analysis and verification of models is an important aspect of MDD paradigm, because they improve understanding of a developed system and enable discovery of faults early in the development. Even though many analysis methods exist (e.g., model checking, proof systems), they are not directly applicable in the context of industrial MDD tools such as IBM Rational Software Architect Real Time Edition (IBM RSA RTE). One of the main reasons for this inapplicability is the difference between modeling languages used in MDD tools (e.g. UML-RT language in IBM RSA RTE) and languages used in existing tools. These differences require an implementation of a transformation from a modeling language to an input language of a tool. UML-RT as well as other industrial MMD models, cannot be easily translated, if the target languages do not directly support key model features. To address this problem we follow a research direction that deviates from the standard approaches and instead of bringing MDD models to analysis tools, the approach brings analysis "closer" to MDD models. We introduce analysis of UML-RT models dedicated to this modeling language. To this end we use a formal internal representation of UML-RT models that preserves the important features of these models, such as hierarchical structures of components, asynchronous communication and action code. This provides us with formalized models using straightforward transformation. In addition, this approach enables the use of MDD-specific abstractions aiming to reduce the size of the state space necessary. To this end we introduce several MDD-specific types of abstractions for: data (using symbolic execution), structure and behavior. The work also includes model checking algorithms, which use the modular nature of UML-RT models. The proposed approach is implemented in a toolset that enables analysis directly of UML-RT models. We show the results of experiments with UML-RT models developed in-house and obtained from our industrial partner.