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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Trust Your Model - Verifying Aerospace System Models with Java Pathfinder


    Contributors:


    Publication date :

    2008-03-01


    Size :

    1729382 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Verifying Aerospace Software

    W. Visser | NTIS | 2005


    Verifying Aerospace Software

    Visser, Willem | NTRS | 2005


    Pathfinder: Overview

    Hudson, Wayne R. / Mankins, John / Anderson, John L. | NTRS | 1988


    Verifying identity of vehicle entering trust zone

    MONDELLO ANTONINO / TROIA ALBERTO | European Patent Office | 2021

    Free access

    Mars pathfinder

    Kubota, T. | British Library Online Contents | 1997