FASE System Description
The
System:
Integrating Object-Oriented Design and
Formal Methods?
Wolfgang Ahrendt2, Thomas Baar1, Bernhard Beckert1, Martin Giese1,
Reiner Hähnle2, Wolfram Menzel1, Wojciech Mostowski2, and
Peter H. Schmitt1
1 Universität Karlsruhe
Inst. f. Logik, Komplexität und Dedukt.-Syst.
D-76128 Karlsruhe, Germany
2 Chalmers University of Technology
Department of Computing Science
S-41296 Gothenburg, Sweden
Abstract. This paper gives a brief description of the KeY system, a tool
written as part of the ongoing KeY project1, which is aimed at bridg-
ing the gap between (a) OO software engineering methods and tools
and (b) deductive verification. The KeY system consists of a commer-
cial CASE tool enhanced with functionality for formal specification and
deductive verification.
1 Introduction
The goal of the ongoing KeY project is to make the application of formal methods
possible and effective in a real-world software development setting. The incen-
tive for this project is the fact that formal methods for software development –
i.e. formal software specification and verification – are hardly used in practical,
industrial software development [5]. As the analysis in [1] shows, the reason is
not a lack of maturity or capacity of existing methods. Our work in the KeY
project is based on the assumption that the primary reasons are as follows:
– The application of formal methods is not integrated into the iterative and
incremental software development processes employed in real-world projects.
– The tools for formal software specification and verification are not integrated
into the CASE tools used to support these processes. Indeed, the target
language of verification tools, in which the programs to be verified have to
be written, is hardly ever a ‘real’ programming language used in industrial
software development.
? The KeY project is supported by the Deutsche Forschungsgemeinschaft (grant
no. Ha 2617/2-1).
1 URL: http://i12www.ira.uka.de/~key/
– Users of verification tools are expected to know synta