Model Driven Development (MDD) is rapidly becoming a mainstream practice for the development of complex aerospace systems. UML has emerged as the de facto standard for modeling languages, supporting a wide range of modeling aspects and refinement levels. As a consequence, models can easily become too complex for manual verification and simple static analysis. This paper describes an approach to using the Java¿ Pathfinder (JPF) software model checker to systematically verify UML state charts. While state machines in general are amenable to model checking, embedded actions and guards in UML state charts are not, since they require execution and analysis of a full programming language to cover the whole model behavior. Many UML development systems can produce code from diagrams, but this code is usually aimed at production systems, and is not suitable for software model checkers. Our approach is based on a specific translation scheme from UML state charts into Java code that (a) is highly readable, (b) shows close correspondence between diagram and program, (c) provides a 1:1 mapping between model and program states, and (d) imposes no restrictions about aspects and actions that can be modeled. We have demonstrated scalability and efficiency of this approach on hierarchical state charts with up to 1000 states, including verification of incomplete models by means of guided model checking. This paper provides an overview of the method based on an exemplary spacecraft model.
Trust Your Model - Verifying Aerospace System Models with Java Pathfinder
2008-03-01
1729382 byte
Conference paper
Electronic Resource
English
NTIS | 2005
|NTRS | 2005
|NTRS | 1988
|British Library Online Contents | 1997
|