A framework for computer-aided validation

Abstract

This paper presents a framework to incorporate computer-based validation techniques to the independent validation and verification (IV&V) of software systems. The framework allows the IV&V team to capture its own understanding of the problem and the expected behavior of any proposed system for solving the problem via an executable system reference model, which uses formal assertions to specify mission- and safety-critical behaviors. The framework uses execution-based model checking to validate the correctness of the assertions and to verify the correctness and adequacy of the system under test.