Vehicular control systems are characterized with numerous complex interactions with a steady rise of autonomous functions, which makes it more challenging for designers and safety engineers to identify unexpected failures. These systems tend to be highly integrated and exhibit features like concurrency for which traditional verification and validation techniques (i.e. testing and simulation) are insufficient to provide rigorous and complete assessment. Model Checking, a well-known formal verification technique, can be used to rigorously prove the correctness of such systems according to design Requirements. In particular, Model Checking is a method for formally verifying finite-state concurrent systems. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. Systems Modeling Language (SysML) has been widely used in architectural and functional modeling in automotive industries. However, it cannot directly be verified against safety requirements. In this work, SysML is used to establish a unified system model that can present an integrated autonomy software and hardware system of a vehicular control system. A generic model transformation strategy is developed to integrate SysML with one of the state-of-the-art Model Checking tools, NuSMV. Cameo Systems Modeler is an industry leading cross-platform collaborative Model-Based Systems Engineering environment for designing standard-compliant SysML models and diagrams. A native Cameo's plugin is constructed to transform SysML state machines to the input language of NuSMV model checker and also to replay the verification results back into the Cameo's environment. A case study of an executable state machine for a high-level autonomous driving system is built. The NuSMV model checker is used to model check the state machine of the autonomous driving system against design requirements expressed as temporal logic formulas. Upon violation of design requirements, our SysML-NuSMV integration allows to replay counterexamples in the Cameo modeling environment. Thus a bi-directional integration of system modeling language with the model checker is developed and the transformation rules are defined. The case study result shows how this method can help designers and safety engineers to automatically identify hidden design errors in a variety of possible design models.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Automatic Formal Verification of SysML State Machine Diagrams for Vehicular Control Systems


    Weitere Titelangaben:

    Sae Int. J. Adv. and Curr. Prac. in Mobility


    Beteiligte:
    Paredis, Chris (Autor:in) / Rizzo, Denise (Autor:in) / Mahani, Maziar (Autor:in) / Wang, Yue (Autor:in)

    Kongress:

    SAE WCX Digital Summit ; 2021



    Erscheinungsdatum :

    2021-04-06


    Format / Umfang :

    9 pages




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Verification and Validation of SysML Models

    Hecht, Myron / Chen, Jaron / Pugliese-Rosillo, Gloria | IEEE | 2021


    Modeling Systems-of-Systems Interfaces with SysML

    Shames, Peter / Sarrel, Marc / Friedenthal, Sandy | NTRS | 2016


    OWL2 and SysML

    Rouquette, Nicolas / Jenkins, Steven | NTRS | 2010


    SysML und Fahrzeugelektronik

    Stuecka, Renate | Tema Archiv | 2006


    SysML Submission Team State- based Behavior Concepts

    Friedenthal, Sanford / Sarrel, Marc | NTRS | 2018