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: 

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

The developed TASTE Model checker is to: 

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: 

Resources: 

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.