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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Trust Your Model - Verifying Aerospace System Models with Java Pathfinder


    Beteiligte:

    Erschienen in:

    Erscheinungsdatum :

    01.03.2008


    Format / Umfang :

    1729382 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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 | Europäisches Patentamt | 2021

    Freier Zugriff