Checking SysML Models Against Safety and Security Properties
- 1 December 2021
- journal article
- research article
- Published by American Institute of Aeronautics and Astronautics (AIAA) in Journal of Aerospace Information Systems
- Vol. 18 (12), 906-918
- https://doi.org/10.2514/1.i010950
Abstract
Systems engineering, or engineering in general, has long been relying on document-centric approaches. Switching to model-based systems engineering, or MBSE for short, has extensively been discussed over the past three decades. Since about two decades, MBSE has been commonly associated with the modeling language SysML (Systems Modeling Language), which offers a standardized notation, not a methodology of using it. SysML needs therefore to be associated with a methodology supported by tools. In this paper, a methodology supported by the free and open-source software TTool is associated with SysML. This paper focuses discussion on methodological issues, leading the authors to share their experience in real-time systems modeling. Modeling with SysML is more than just drawing the different diagrams. Associated tools offer possibilities to analyze SysML models for specific properties. In this paper, verification addresses both safety and security properties. The TTool model checker inputs the SysML model enriched with safety properties to be verified and outputs an yes/no answer for each property. Security verification checks SysML models against confidentiality, integrity, and authenticity properties. As an illustration of the proposed approach, an aircraft cockpit door control system is modeled in SysML and verified against safety and security properties.Keywords
This publication has 17 references indexed in Scilit:
- SysML Model Transformation for Safety and Security AnalysisPublished by Springer Science and Business Media LLC ,2019
- Integrating Model Checking With SysML in Complex System Safety AnalysisIEEE Access, 2019
- Formal verification of SysML diagram using case studies of real-time systemInnovations in Systems and Software Engineering, 2018
- An Extended UML Method for the Verification of Security ProtocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2014
- A formal verification framework for SysML activity diagramsExpert Systems with Applications, 2014
- Foundations of Attack–Defense TreesLecture Notes in Computer Science, 2011
- Analyzing security protocols with secrecy types and logic programsJournal of the ACM, 2005
- TURTLE: A Real-Time UML Profile Supported by a Formal Validation ToolkitIEEE Transactions on Software Engineering, 2004
- Model Checking UML State Machines and CollaborationsElectronic Notes in Theoretical Computer Science, 2001
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983