Guidelines for Development of Operational Requirements for Model Checking Tools

Formal model checking techniques have been shown to be an effective means of verification for safety-critical software. However, several issues remain for their widespread use in industry. Among the most pressing of these issues is the qualification of tools implementing formal model checking techniques for use in certification activities. DO-178C is a contemporary aviation software safety standard that includes supplementary standards for both formal methods techniques (DO-333) and software tool qualification (DO-330). Little research has focused on the application of these standards to formal model checker qualification. This paper investigates the importance of the Tool Operational Requirement (TOR) definition, verification, and validation process. Further considerations for definition of TORs are investigated, with a proposed framework for TOR content presented. Finally, strategies for the TOR process itself and for appropriate TOR definition level are proposed for further investigation.