Menu
Looking at C, C has good support for formal methods that can be used in-code(frama-c, VCC, verifast). C++ doesn't seem to have any comparable as far as I can tell.
What formal methods are available for reasoning about safety-critical software written in C++?
256
In software development, formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety-critical or security-critical software and systems, such as avionics software.
Formal methods encompass a group of technologies that aim to manage these problems much more effectively by supplementing human resources with computational resources.
Formal methods are the use of mathematical modelling for the specification, development and verification of systems in both software and electronic hardware. The formal methods are used to ensure these systems are developed without error.
Safety-critical systems are those systems whose failure could result in loss of life, significant property damage, or damage to the environment. Aircraft, cars, weapons systems, medical devices, and nuclear power plants are the traditional examples of safety-critical software systems.
A medical company I work with uses Coverity and Klocwork to check the code for possible problems such as resource leaks and uninitialized pointer getting used.
However, these are tools and not standard for safety critical code.
What I have seen is that MISRA has been working on a standard for C++. They started with C way back, and start work on C++ about 5 years ago or so. One big problem is that the MISRA standard for C++, for example, says you should not use templates. That really limits what you can do in C++. However, you could use that document as a starting point. You may want to limit templates used in your software to what comes in the standard library and boost, for example.
Note that Klocwork has an extension for MISRA C++.
Yet, one of the best way to write good code is to test it with unit tests and integration tests. I have found with years that this is way more reliable that most other methods.
90
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
