Formal Verification of Spacecraft Control Programs: An Experience Report
Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware.
The verification approach is demonstrated on an industrial case study. We present REDFIN, a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage for state transformers, followed by examples of verification of simple control programs.
Thu 22 Aug
|13:30 - 14:00|
|14:00 - 14:30|
|14:30 - 15:00|