Checking sysML models for co-simulation

N. Amálio, R. Payne, A. Cavalcanti, J. Woodcock, Ogata K. (Editor), Lawford M. (Editor), Liu S. (Editor)

    Research output: Book/ReportBookpeer-review


    Cyber-physical systems (CPSs) are often treated modularly to tackle both complexity and heterogeneity; and their validation may be done modularly by co-simulation: the coupling of the individual subsystem simulations. This modular approach underlies the FMI standard. This paper presents an approach to verify both healthiness and well-formedness of an architectural design, expressed using a profile of SysML, as a prelude to FMI co-simulation. This checks the conformity of component connectors and the absence of algebraic loops, necessary for co-simulation convergence. Verification of these properties involves theorem proving and model-checking using: Fragmenta, a formal theory for representing typed visual models, with its mechanisation in the Isabelle/HOL proof assistant, and the CSP process algebra and its FDR3 model-checker. The paper’s contributions lie in: a SysML profile for architectural modelling supporting multi-modelling and co-simulation; our approach to check the adequacy of a SysML model for co-simulation using theorem proving and model-checking; our verification and transformation workbench for typed visual models based on Fragmenta and Isabelle; an approach to detect algebraic loops using CSP and FDR3; and a comparison of approaches to the detection of algebraic loops. © Springer International Publishing AG 2016.
    Original languageEnglish
    PublisherSpringer Verlag
    Number of pages16
    Volume10009 LNCS
    ISBN (Print)03029743 (ISSN); 9783319478456 (ISBN)
    Publication statusPublished (VoR) - 2016


    • Algebraic loops
    • Co-simulation
    • CSP
    • FMI
    • SysML
    • Algebra
    • Embedded systems
    • Formal methods
    • Machinery
    • Software engineering
    • Theorem proving
    • Component connectors
    • Cosimulation
    • CSP process algebra
    • Cyber physical systems (CPSs)
    • Modular approach
    • Multi-modelling
    • Model checking


    Dive into the research topics of 'Checking sysML models for co-simulation'. Together they form a unique fingerprint.

    Cite this