The Lunar Atmosphere Dust Environment Explorer (LADEE) mission orbited the moon in order to measure the density, composition, and time variability of the lunar dust environment. The successful mission launched September 7, 2013 and was de-orbited and impacted the moon’s surface on April 17, 2014. The ground-side and onboard flight software for the mission was developed using a Model-Based Software Engineering (MBSE) methodology combined with strong reuse of Government and Commercial Off-The-Shelf (G/COTS) components. Models of the spacecraft and flight software were developed in a graphical dynamics modeling package. Flight software requirements were prototyped and refined using the simulated models. After the model was shown to work as desired in the simulation framework, C-code software was automatically generated from the models. The auto-generated software was then tested in real-time Processor-in-the-Loop and Hardware-in-the-Loop test beds. Traveling Road Show test beds were used for early integration tests with payloads and other subsystems. Traditional techniques for verifying computational sciences models were used to characterize the spacecraft simulation. A lightweight set of formal methods analysis, static analysis, formal inspection, and code coverage analyses was utilized to further reduce defects in the onboard flight software artifacts. These techniques were applied early and often in the development process, iteratively increasing the capabilities of software and fidelity of vehicle models and test beds.
MBSE Validation and Verification
Case Study for LADEE
Handbook of Model-Based Systems Engineering ; Chapter : 58 ; 955-986
2023-07-08
32 pages
Article/Chapter (Book)
Electronic Resource
English
Model-based systems engineering , Validation and verification , LADEE , Software engineering , Automated testing , Auto-code Engineering , Control and Systems Theory , Simulation and Modeling , Models and Principles , Operations Management , Quality Control, Reliability, Safety and Risk , Cyber-physical systems, IoT
MBSE Validation and Verification: Case Study for LADEE
NTRS | 2021
|The FoReVer Methodology: A MBSE Framework for Formal Verification
British Library Conference Proceedings | 2013
|