Domain Specific Analysis of Statemachine Models of Reactive Systems.
Karolina Zurowska · 2013
Abstract. Analysis of models is an important aspect of the Model Driven Development (MDD) paradigm. Even though many analysis methods exist (e.g., model checking), they are not easily applicable in the context of MDD tools such as IBM Rational Software Architect Real Time Edition (IBM RSA RTE) and MDD languages such as UML-RT. The major reason for this inapplicability is that they typically require MDD models to be translated to a formal notation, which does not directly support key model features. The research direction proposed in this paper deviates from the standard approaches – it brings analysis “close” to MDD models and introduces domain-specific analysis of UML-RT models. To this end we use a formal representation that preserves the important aspects of the models. This removes the translational effort and, in addition, enables the use of MDD-specific abstractions aiming to support better understanding of models and to improve the scalability of verification. We will define abstractions for data (using symbolic execution), for structure and for behavior. The approach will be implemented as a set of plugins to IBM RSA RTE and evaluated on a variety of UML-RT models. 1