Skip to main content Skip to main navigation

Publication

The VSE development method - a way to engineer high-assurance software systems

Frank Koop; Markus Ullmann; Stefan Wittmann; Dieter Hutter; Bruno Langenstein; Claus Sengler; Werner Stephan; Andreas Wolpers; Wolfgang Reif
In: R. Gotzhein; J. Bredereke (Hrsg.). Tagungsband des 5. GI/ITG-Fachgesprächs "Formale Beschreibungstechniken für verteilte Systeme". GI/ITG-Fachgespräch (FBT), June 22-23, Kaiserlautern, Germany, 1995.

Abstract

The only way to build high-assurance software systems in a verifiably correct manner is to use formal methods. Formal methods can be characterized at several levels of use, and they provide different levels of assurance for the software developed by such methods [BoSt93]. At the basic level, they may simply be used for specification of the system to be designed. The next level of use is to apply formal methods to the development process, using a set of rules or a design calculus that allows stepwise refinement of the specification into an executable program. At the most rigorous level, the entire proof process is carried out. This paper describes the recently completed formal specification and verification tool Verification Support Environment (VSE). An advantage of the design of the VSE tool is the possibility of using formal and semiformal development methods combined in a unique working environment. The VSE development method is fully adaptable to the above-described operational classification of formal methods. Beginning with a formal top level design in a formal specification language (VSE-SL), this specification can be transferred into executable programs through stepwise refinement. The proof obligations are automatically generated by the VSE system. The corresponding proofs can even be carried out semi-automatically with VSE support. This process guarantees the correctness of refinements. However, the success of any formal approach to correct software strongly depends on two parameters: The first is the performance of the deduction subsystem used to verify the proof obligations arising during the development. The second is the structure of the design process itself. The main purpose of this paper is to present the formal design process with the formal specification language VSE-SL.