Is cFE been verified through formal verification?

I found some resources about verification of NASA flight software.

I am not sure whether NASA flight software is cFS or not.

In [1] Appendix D Sec. 7 Model-Based Engineering mentioning, “use directly in the formal verification of design models, for instance with strong model-checking tools”.

[1] NASA Study on Flight Software Complexity: https://www.google.com.tw/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwj7ypSUxerTAhUGnJQKHXxSAhMQFgglMAA&url=https%3A%2F%2Fwww.nasa.gov%2Fpdf%2F418878main_FSWC_Final_Report.pdf&usg=AFQjCNEm-lffuZYcOMBr_MqXX8HBACSNiQ&sig2=_mAtV4KDdvyvWl17chDR4w

[2] Using SPIN Model Checking for Flight Software Verification: https://www.google.com.tw/url?sa=t&rct=j&q=&esrc=s&source=web&cd=16&ved=0ahUKEwjX4Ny9vOrTAhUDmpQKHT1tB_E4ChAWCD8wBQ&url=http%3A%2F%2Fspinroot.com%2Fgerard%2Fpdf%2Fgluck_holz.pdf&usg=AFQjCNHV6-ORtjYw9N9o-9O9F6CzY7QzVg&sig2=ia1qS4VQVwqk3rF52N979A


  • You must to post comments

I do not believe cFE has been formally verified through a tool such as SPIN.

It has gone through some less formal verification processes, such as described in this paper: https://www.semanticscholar.org/paper/Verifying-architectural-design-rules-of-the-flight-Ganesan-Lindvall/7ea4fda511b3e29a3a61cb5cf71e40916521d129 (Verifying Architectural Design Rules of the Flight Software Product Line) and in this slide deck: https://trs.jpl.nasa.gov/bitstream/handle/2014/43345/12-5188_A1b.pdf (NASA’s Software Architecture Review Board’s (SARB) Findings from the Review of GSFC’s “core Flight Executive/Core Flight Software” (cFE/CFS)).

I think a formal verification of cFE would be really useful, but (albeit with limited knowledge about formal verification methods) I anticipate a few problems in applying it to cFE:
1) C code is difficult to verify (due to how permissive of a language it is, for example pointer manipulation), and may require additional restrictions beyond the C standard. cFE may not follow these additional restrictions as is.
2) cFE does not include the operating system, so any formal verification will have to assume that the OS is trusted. Unless you use a formaly verified OS, but I believe seL4 is the only one, and cFE has not been ported to it.
3) Formal verification requires a good amount of effort and expertise to perform.

That said, cFE is fairly modular, which may make it easier to verify.

Do you have an interest in formal verification / applying it to cFE?

  • You must to post comments
Showing 1 result
Your Answer

Please first to submit.