From Verified Scala to STIX File System Embedded Code using Stainless

paper ps   
We present an approach for using formal methods in embedded systems and its evaluation on a case study. In our approach, the developers describe the system in a restricted subset of the high-level programming language Scala. We then use 1) a verification system to formally prove properties of such Scala program, and 2) a source-to-source translator to map Scala to C code. We have adapted the Stainless verification system to support constructs for describing embedded software (more machine integer types and early returns) and to support verification patterns needed for embedded systems code (array swap operation, pre-allocated and initialized memory, constant-length arrays). The implemented C code translator generates code that can be compiled with compilers such as GCC and integrated into larger C applications. We evaluate our approach on a case study of a file system of an instrument on the Solar Orbiter satellite. We have ported around a thousand lines of C code to Scala. We wrote specification and proof hints to make the code verify. Stainless verified the absence of run-time errors, as well as function preconditions, postconditions, and data structure invariants. The generated C code was integrated into the existing code base and exhibits very similar code size, memory use, and performance. In this process we identified multiple bugs in the well-tested code base, which were fixed in-orbit.

Citation

Jad Hamza, Simon Felix, Viktor Kunčak, Ivo Nussbaumer, and Filip Schramka. From verified Scala to STIX file system embedded code using Stainless. In NASA Formal Methods (NFM), page 18, 2022.

BibTex Entry

@inproceedings{HamzaETAL22NFM,
  title = {From Verified {S}cala to {STIX} File System Embedded Code using {S}tainless},
  author = {Jad Hamza and Simon Felix and Viktor Kun\v{c}ak and Ivo Nussbaumer and Filip Schramka},
  pages = {18},
  year = {2022},
  abstract = {We present an approach for using formal methods in  embedded systems and its evaluation on a case study. In our  approach, the developers describe the system in a  restricted subset of the high-level programming language  Scala. We then use 1) a verification system to formally  prove properties of such Scala program, and 2) a  source-to-source translator to map Scala to C code. We have  adapted the Stainless verification system to support  constructs for describing embedded software (more machine  integer types and early returns) and to support  verification patterns needed for embedded systems code  (array swap operation, pre-allocated and initialized  memory, constant-length arrays). The implemented C code  translator generates code that can be compiled with  compilers such as GCC and integrated into larger C  applications. We evaluate our approach on a case study of a  file system of an instrument on the Solar Orbiter  satellite. We have ported around a thousand lines of C code  to Scala. We wrote specification and proof hints to make  the code verify. Stainless verified the absence of run-time  errors, as well as function preconditions, postconditions,  and data structure invariants. The generated C code was  integrated into the existing code base and exhibits very  similar code size, memory use, and performance. In this  process we identified multiple bugs in the well-tested code  base, which were fixed in-orbit.},
  booktitle = {NASA Formal Methods (NFM)},
  url = {http://infoscience.epfl.ch/record/292424}
}