Facial reconstruction

Search LJMU Research Online

Browse Repository | Browse E-Theses

Model Checking for Formal Verification of Space Systems

Kurowski, M, Babski, R, Duncan, S, Perrotin, M and Webster, M (2021) Model Checking for Formal Verification of Space Systems. In: Model Based Space Systems and Software Engineering (MBSE2021), 29 September 2021 - 30 September 2021, Virtual.

1405 - model checking for formal verification of space systems.pdf - Published Version

Download (314kB) | Preview


The goal of the presented activity is to integrate an existing model checking engine – SPIN1 – with the TASTE2 MBSE environment. For this purpose, the modelling languages used in TASTE – ASN.1, AADL and SDL need to be translated into PROMELA, a language for modelling and verification of concurrent systems. This paper describes the current achievements of the activity – proposal of a TASTE model checking workflow, formalization of requirement specification and established PROMELA translation patterns. Finally, the development of SDL models for validation of the tools and exploration of their utility in the design of space systems is discussed.

Item Type: Conference or Workshop Item (Paper)
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Q Science > QA Mathematics > QA76 Computer software
Divisions: Computer Science & Mathematics
Date Deposited: 11 Oct 2021 12:47
Last Modified: 13 Apr 2022 15:18
URI: https://researchonline.ljmu.ac.uk/id/eprint/15619
View Item View Item