31

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++?

willfredthebuel
  • 339
  • 2
  • 6
  • If you are writing safety-critical software, you probably have a certification standard to respect and a safety authority to answer to. These state explicitly what they expect from you. Is that C++ code? Usually, no, although it is always possible to explain why you think it is a better tool for the job. Formal methods? Usually, no again, although there is an appendix in the new DO-178C standard for aeronautics. What standard and authority apply in your case? – Pascal Cuoq Jul 23 '14 at 00:01
  • In our case we're looking at class 2 medical which isn't guided by any specific coding standard, but does have software process standards. In the class 2 and 3 device world Misra is a pretty safe bet to go with for coding standards but also doesn't require formal methods. This question has more to do with our future development and learning in general than a specific project. I've heard the DO178C standard has a part on formal methods and I ordered a book on it to see what's going on. This is kinda a follow up to see what others have been using with C++ – willfredthebuel Jul 23 '14 at 00:09
  • 3
    You might want to review the MISRA C++ coding guidelines. There are static analysis tools that support this standard. The tools also have other checkers to augment the MISRA standard checks. – Thomas Matthews Jul 23 '14 at 00:13
  • 1
    I am close to the Frama-C development team and I can say that a C++ front-end is in development. This is part of a EU project where VeriFast is also getting a C++ front-end, with some resources being shared. Some information is available at http://llvm.org/devmtg/2014-04/PDFs/Posters/FramaC.pdf – Pascal Cuoq Jul 23 '14 at 00:17
  • Yes. Thank you Pascal! This is exactly what I was hoping for. The website is a bit scarce on info. I can see from the papers and presentations they've probably completed WP1 and are somewhere in the middle of WP2. I'm not sure if you're allowed to say, but any gut feelings for when alpha-type stuff might end up being available? – willfredthebuel Jul 23 '14 at 02:33
  • @willfredthebuel The C++ front-end will be available through this company: http://trust-in-soft.com (which is also my current employer). I will let you find the contact address. – Pascal Cuoq Jul 23 '14 at 13:12
  • You could also try [QA.C++](http://www.programmingresearch.com/products/qacpp/) by Programming Research. I do not represent this company, but have come across their products in the past. – Evil Dog Pie Jan 20 '15 at 15:57
  • Pascal Cuoq - while I readily agree that you _should_ have a standard and an authority, commonly you don't. It's a serious problem. Some of the very worst C++ code I've ever seen is in safety critical code. – Mike Crawford May 19 '15 at 03:46

1 Answers1

3

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.

Alexis Wilke
  • 19,179
  • 10
  • 84
  • 156
  • 8
    [Formal methods](https://en.wikipedia.org/wiki/Formal_methods) has nothing to do with MISRA. MISRA is just a coding standard used to reduce the programming language into a safe subset. If you are looking at the more hardcore, application-specific safety standards, they will require that you both use formal methods and a safe subset of the programming language. – Lundin Sep 14 '15 at 06:45