Qualification of Proof Assistants, Checkers, and Generators: Where Are We and What Next?

TL;DR

This paper assesses the current state and future directions of qualifying proof assistants, checkers, and generators for high-integrity cyber-physical systems, emphasizing standards compliance and practical application readiness.

Contribution

It provides a comprehensive SWOT analysis of tool qualification in proof assistants, checkers, and generators, and offers recommendations for improving qualification processes.

Findings

Tools are partially qualified for safety-critical use

SWOT analysis reveals key strengths and weaknesses

Recommendations for enhancing qualification standards

Abstract

Cyber-physical systems, such as learning robots and other autonomous systems, employ high-integrity software in their safety-critical control. This software is developed using a range of tools some of which need to be qualified for this purpose according to international standards. In this article, we first evaluate the state of the art of tool qualification for proof assistants, checkers (e.g., model checkers), and generators (e.g., code generators, compilers) by means of a SWOT (Strengths, Weaknesses, Opportunities, Threats) analysis. Our focus is on the qualification of tools in the three mentioned categories. Our objective is to assess under which conditions these tools are already fit or could be made fit for use in the practical engineering and assurance of high-integrity control software. In a second step, we derive a viewpoint and a corresponding range of suggestions for improved tool qualification from the results of our SWOT analysis.