MINERVA

MINERVA (Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms) is a practical, but rigorous, approach to the development of safety-critical software components of systems that interact with the environment. In MINERVA, functional and operational requirements are first specified using a formal specification language. Core algorithms that implement those requirements are also specified and formally proved correct with respect to their specifications. These algorithms are then numerically evaluated on a generated set of test cases. Finally, the output values are compared to outputs computed by an implementation of these algorithms in a programming language with the purpose of showing similar behavior between the algorithm specifications and their corresponding implementations in code.

Publications

• Anthony Narkawicz, César Muñoz, and Aaron Dutle, The MINERVA Software Development Process, Automated Formal Methods, Menlo Park, California, 2017. BibTeX Reference.
• Aaron Dutle, César Muñoz, Anthony Narkawicz, and Ricky Butler, Software Validation via Model Animation, Proceedings of the Proceedings of the 9th International Conference on Tests and Proofs (TAP 2015), Lecture Notes in Computer Science, Vol. 9154, pp. 92-108, 2015. BibTeX Reference.

The tag identifies links that are outside the NASA domain