Checking SysML Models for Co-simulation

Amalio, Nuno and Payne, Richard and Cavalcanti, Ana and Woodcock, Jim (2016) Checking SysML Models for Co-simulation. In: Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science, 10009 . Springer. ISBN 978-3-319-47845-6

Full text not available from this repository. (Request a copy)

Abstract

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.

Item Type: Book Section
Uncontrolled Keywords: Co-simulation FMI CSP SysML Algebraic loops
Subjects: G400 Computer Science
Divisions: Faculty of Computing, Engineering and the Built Environment
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology > Cyber Security
UoA Collections > UoA11: Computer Science and Informatics
Depositing User: $ Ian McDonald
Date Deposited: 14 Aug 2017 11:25
Last Modified: 14 Aug 2017 11:25
URI: http://www.open-access.bcu.ac.uk/id/eprint/4990

Actions (login required)

View Item View Item

Research

In this section...