Research Projects

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.