Astronomy & Space Sciences
Title : | Verification and validation of satellite onboard software (AOCE, TCP, BDH, SSR, SPS) using model checking |
Area of research : | Astronomy & Space Sciences |
Focus area : | Software Engineering, Embedded Systems, Software Quality Assurance |
Contact info : | daffini@isac.gov.in |
Details
Executive Summary : | Model Checking is a particular formal method which takes in "a finite model of the system" and "a formally written property" and verifies whether the system satisfies the property by making an exhaustive search for counter-examples. Models addresses the system behaviour and the properties prescribe what the system should do / should not do. For the verification and validation of Satellite Onboard software, the code written in ADA language needs to be converted into abstract model and the system/software specifications to be converted to properties understandable by the model checker. Once the system is modeled, the model checker explores the systems state space in order to determine satisfaction or violation of property. |
Co-PI: | Ms.Manoja J, U R Rao Satellite Centre (URSC), Bengaluru |
Organizations involved