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: | https://doi.org/10.1007/978-3-319-47846-3_28 | ||||
| Dates: |
|
||||
| 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 > School of Computing and Digital Technology |
||||
| 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 |
Tools
Tools