Model Checking for Formal Verification of Space Systems

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.