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.

Preview

Text 1405 - model checking for formal verification of space systems.pdf - Published Version Download (314kB) | Preview

Abstract

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