Deduction in the verification support environment (VSE)

Abstract

The reliability of complex software systems is becoming increasingly important for the technical systems they are embedded in. In order to assure the highest levels of trustworthiness of software formal methods for the development of software are required. The VSE-tool was developed by a consortium of German universities and industry to make a tool available which supports this formal development process. VSE is based on a particular method for programming in the large. This method is embodied in an administration system to edit and maintain formal developments. A deduction component is integrated into this administration system in order to provide proof support for the formed concepts. In parallel to the development of the system itself, two large case studies were conducted in close collaboration with an industrial partner. In both cases components of systems previously developed by the industry were re-developed from scratch, starting with a formal specification derived from the original documents. This paper focuses on the deduction component and its integration. We use a part of one of the industrial case studies in order to illustrate the important aspects of the deduction component: We argue that a close integration which makes the structure of developments visible for the theorem prover is necessary for an efficient treatment of changes and an indispensable structuring of the deduction process itself. Also we commend an architecture for interactive strategic theorem proving which has turned out to be adequate for applications in the context of formal program development. The last one of the three main sections addresses the important point of detecting bugs in implementations and specifications.