Lookup NU author(s): Dr Andrey Mokhov,
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.
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.
Author(s): Mokhov A, Lukyanov G, Lechner J
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Haskell Symposium 2019
Year of Conference: 2019
Online publication date: 08/08/2019
Acceptance date: 21/06/2019
Date deposited: 10/07/2019
Library holdings: Search Newcastle University Library for this item