Formal Verification of Spacecraft Control Programs (Experience Report)

Mokhov, A; Lukyanov, G; Lechner, J

doi:10.1145/3331545.3342593

Formal Verification of Spacecraft Control Programs (Experience Report)

Lookup NU author(s): Dr Andrey Mokhov, Dr Georgy Lukyanov

Downloads

Published version [.pdf]

Licence

This is the final published version of a conference proceedings (inc. abstract) that has been published in its final definitive form by ACM, 2019.

For re-use rights please refer to the publisher's terms and conditions.

Abstract

Verification of correctness of control programs is an essentialtask in the development of space electronics; it is difficultand typically outweighs design and programming tasks interms of development hours. This experience report presentsa verification approach designed to help spacecraft engineersreduce the effort required for formal verification of low-levelcontrol programs executed on custom hardware.The verification approach is demonstrated on an industrialcase study. We present REDFIN, a processing core used inspace missions, and its formal semantics expressed using theproposed metalanguage for state transformers, followed byexamples of verification of simple control programs.