ESA ITI AO6067 - Verifying Satellite Operational Procedures

Details
Category: Projects
Last Updated on Friday, 11 January 2013 09:34

Project Title: Model Checker Validator for Satellite Operational Procedure

Project Acronym: ESA-ITI-AO6067

Funding Scheme: European Space Agency (ESA) Innovation Triangle Initiative (ITI). ITI Type B (150K Eur)

Starting Date: May 2010

Project Duration in Months: 12

UNIROMA1 Unit Activity: our research activity focuses on formal verification of satellite operational procedures via model checking driven simulation.

Project Consortium: 1) Telespazio - Napoli (Developer, Prime Contractor), 2) Telespazio - Fucino (Customer), 3) Sapienza University of Rome (Inventor)

Abstract
We develop a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a formal model for a complex system such as a satellite is a prohibitively expensive task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we carry out case stuudies on a meaningful scenario.