A Design Phase Directed Formal Verification Process

John A. Keane, Walter Hussak

    Research output: Contribution to journalArticlepeer-review

    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.
    Original languageEnglish
    Pages (from-to)255-269
    Number of pages14
    JournalSoftware Quality Journal
    Volume8
    Issue number4
    Publication statusPublished - 1999

    Keywords

    • High-level design
    • Operating systems
    • Temporal logic
    • Verification

    Fingerprint

    Dive into the research topics of 'A Design Phase Directed Formal Verification Process'. Together they form a unique fingerprint.

    Cite this