On the Adoption of Model Checking in Safety-Related Software Industry

On the Adoption of Model Checking in Safety-Related Software Industry
Alessandro Fantechi, Stefania Gnesi

Computer Safety, Reliability, and Security
Lecture Notes in Computer Science Volume 6894, 2011, pp 383-396

3.3 Tool Qualification
When using a model checker for the certification of a safety-related software, one of the issues that is often raised is: Is the model checker itself bug-free? That is, can I trust the model checker tool when it says that a system is safe? DO178B addresses this issue by Tool Qualification, classifying software tools as:
– Software development tools: Tools whose output is part of the developed
software and thus can introduce errors (this type includes compilers)
– Software verification tools: Tools that cannot introduce errors, but may fail to detect them: this type may include model checkers.

According to DO178B the qualification criteria for software verification tools should be achieved by demonstration “that the tool complies with its Tool Operational Requirements under normal operational conditions”; this demonstration requires comprehensive testing and the establishment of a controlled development process. To our knowledge, no model checker up to now has been qualified.

An alternative to qualification can be found in the proven in use concept from EN50128: a tool that has a long record of usage within similar projects with no known failure. Since we are at the beginning of industrial application of model checking to software code correctness, this is a hardly justifiable alternative.

Another alternative is to adopt diverse redundancy: duplicating the validation effort by repeating the verification session over two different independent model checkers, and then compare the result for equality.