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
Identification Number:	10.1007/978-3-319-47846-3_28
Dates:	Date Event 2016 Published
Uncontrolled Keywords:	Co-simulation FMI CSP SysML Algebraic loops
Subjects:	CAH11 - computing > CAH11-01 - computing > CAH11-01-01 - computer science
Divisions:	Faculty of Computing, Engineering and the Built Environment Faculty of Computing, Engineering and the Built Environment > College of Computing
Depositing User:	Ian Mcdonald
Date Deposited:	14 Aug 2017 11:25
Last Modified:	22 Mar 2023 12:01
URI:	https://www.open-access.bcu.ac.uk/id/eprint/4990

Actions (login required)

View Item