Model-Driven Software Verification

Abstract. In the classic approach to logic model checking, software verification requires a manually constructed artifact (the model) to be written in the language that is accepted by the model checker. The construction of such a model typically requires good knowledge of both the application being verified and of the capabilities of the model checker that is used for the verification. Inadequate knowledge of the model checker can limit the scope of verification that can be performed; inadequate knowledge of the application can undermine the validity of the verification experiment itself. In this paper we explore a different approach to software verification. With this approach, a software application can be included, without substantial change, into a verification test-harness and then verified directly, while preserving the to apply data abstraction techniques. Only the test-harness is written in the language of the model checker. The test-harness is used to drive the application thr...

• Type: Conference
• Year: 2004
• Where: SPIN
• Authors: Gerard J. Holzmann, Rajeev Joshi
• Keywords: Inadequate Knowledge, Model Checker, Software Verification, SPIN 2004, Theoretical Computer Science