Model Checking for Formal Verification of Space Systems

TASTE is ESA’s model-based development environment for heterogenous, embedded, real-time systems, using AADL, ASN.1 and SDL models for high-level architecture, data and behaviour description. It provides the capabilities to design, implement, build, deploy and test embedded applications.  The use of high-level modelling constructs also provides opportunities for deploying model checking techniques.  Model checking is a family of methods for verifying that a finite-state model of a system satisfied a given specification. In simple terms, it can be thought of as generalized testing, in which all possible system behaviours are automatically explored and verified against the defined requirements, or system properties. These properties are usually categorized into two groups: safety (“nothing bad ever happens”) and liveness (“something good eventually happens”). 

Model Checking for Formal Verification of Space Systems, funded by European Space Agency, aims to develop a practical, user-friendly model checker which can be used in TASTE to perform formal verification of real systems, deployable onto embedded platforms from a single “source of truth”, in the spirit of “Check as You Fly, Fly as You Check” principle (derived from “Test as You Fly, Fly as you Test”, used in the traditional development of flight software). At its core, the solution uses Spin, Simple Promela INterpreter, which is a widely used, powerful, open-source model checking engine, capable of modelling and verifying concurrent distributed systems with shared memory. System properties to be verified can be expressed using: 

• Stop Conditions – Boolean expressions using an SDL-like syntax and enhanced with a small subset of Linear Temporal Logic, which can be used to define system invariants; 
• Observers – enhanced SDL state machines capable of observing and modifying entire system state, which can be used to verify the correctness of complex behaviour, as well as inject errors to verify software system’s resilience to unreliable hardware in a hostile space environment; 
• Verification Message Sequence Charts – Message Sequence Charts with constrained and formalized semantics, which can be used to verify the correctness of message exchange sequences. 

A simplified version of the assumed (user-tailorable) model-based workflow is: 

• define an iteration of the model structure, so that a framework (e.g., signals, states, data structures) is available for the formalization of requirements; 
• formalize the requirements by translating the informal ones into Stop Conditions, Observers and Verification Message Sequence Charts; 
• define an iteration of model behaviour using SDL; 
• define a model checking scenario by selecting the relevant subset of the model under verification and applicable requirements, as well as optionally refining input vector generation and preparing additional Observers transitioning the model into the desired initial state. 

The developed TASTE Model checker is to: 

• transform AADL, ASN.1 and SDL models into Promela, the modelling language understood by Spin; 
• execute the model using Spin, hidden from the user via a simple and friendly façade; 
• convert Spin traces (generated in case a property violation is found) into MSC, allowing to analyse, test and debug the found scenario using TASTE. 

All of the above actions are to be available from within the new TASTE Integrated Development Environment – SpaceCreator. Activity is primed by N7 Space, the design of the model transformation is supported by Liverpool John Moores University – School of Computing Science and Mathematics, and the developed model checker is to be verified using a set of representative cases developed by Thales Alenia Space UK: 

• Toy Model, for basic verification of the model checking engine using an existing known example, well-analysed and documented in the relevant literature; 
• Subsystem Model, based on ECSS-E-ST-50-15C CANopen protocol stack, for benchmarking the capabilities and performance of the model checker; 
• Application Model, based on an in-orbit fuel transfer use-case, for benchmarking the capabilities of the model checker and verifying its usefulness early in the system engineering life cycle. 

Resources: 

• TASTE – https://taste.tools/ 
• Spin – http://spinroot.com/ 
• SpaceCreator – https://gitrepos.estec.esa.int/taste/spacecreator/ 
• Thales Alenia Space UK – https://www.thalesgroup.com/en/countries/europe/united-kingdom/markets-we-operate/space 
• Liverpool John Moores University – https://www.ljmu.ac.uk/ 

Disclaimer: This work performed during this project was carried out under a programme of, and funded by, the European Space Agency. The views expressed here can in no way be taken to reflect the official opinion of the European Space Agency.