Formal Verification of Spacecraft Control Programs Using a Metalanguage for State Transformers

Andrey Mokhov, Georgy Lukyanov, Jakob Lechner

Verification of functional correctness of control programs is an essential task for the development of space electronics; it is difficult and time-consuming and typically outweighs…