A Design Phase Directed Formal Verification Process

Abstract

The presence of an effective verification process at an earlier phase of the system development lifecycle will have a greater impact on productivity and product quality than a verification process at a later phase. The usual verification process at the later coding phases involves some form of testing. As high-level design cannot be tested in the same way as code, an option at that phase is some kind of formal verification. A process of verification is presented for the high-level design phase of an operating system development, where both rigorous and formal verification are used, and the rigorous directs the formal. The methodology is based on temporal logic. Formal proofs are manageable on an in-house theorem prover.