Verifying requirements through mathematical modelling and animation

Abstract

Achieving confidence in the correctness, completeness and consistency of requirements specifications can be problematic and the consequences of incorrect requirements can be costly. In this paper we argue that specification and animation can provide reasonably high levels of assurance in the requirements without the overheads of using general purpose theorem proving tools. We propose a framework based on mode analysis and the operational semantics of logic programs for animating specifications. The framework allows us to combine prototyping and limited forms of automated deduction to increase our levels of confidence in specifications. Finally, we show how such a framework can be used to inc..