Paper Info
Title
Formal Verification of Spacecraft Control Programs
Abstract
AbstractVerification 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 article 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 a REDuced instruction set for Fixed-point and INteger arithmetic (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.
Year
DOI
Venue
2020
10.1145/3391900
ACM Transactions on Embedded Computing Systems
Keywords
DocType
Volume
Formal verification, instruction set architecture, functional programming, domain-specific languages
Journal
19
Issue
ISSN
Citations 
5
1539-9087
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
G Lukyanov100.34
Andrey Mokhov213626.57
J Lechner300.34