Language Specific Analysis of State Machine Models of Reactive Systems
Loading...
Date
2014-06-25
Authors
Zurowska, Karolina
Keyword
software analysis , model checking , Model Driven Development , software engineering
Abstract
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.