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 bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.
The KeY project is supported by the Deutsche Forschungsgemeinschaft (grant no. Ha 2617/2-1).
URL: http://i12www.ira.uka.de/~key/.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. The KeY approach: Integrating object oriented design and formal verification. In M. Ojeda-Aciego, I. P. de Guzmán, G. Brewka, and L. M. Pereira, editors, Proc. 8th European Workshop on Logics in AI (JELIA), Malaga,Spain, volume 1919 of LNCS, pages 21–36. Springer-Verlag, Oct. 2000.
T. Baar. Experiences with the UML/OCL-approach to precise software modeling: A report from practice. In Proc. Net. ObjectDays, Erfurt, Germany, 2000. http://i12www.ira.uka.de/~key/doc/2000/baar00.pdf.gz.
B. Beckert. A dynamic logic for the formal verification of Java Card programs. In I. Attali and T. Jensen, editors, Java on Smart Cards: Programming and Security. Revised Papers, Java Card 2000, International Workshop, Cannes, France, LNCS 2041, pages 6–24. Springer-Verlag, 2001.
B. Beckert, U. Keller, and P. H. Schmitt. Translating the object constraint language into first-order predicate logic. Submitted to FASE 2002, available from http://i12www.ira.uka.de/~projekt/publicat.htm.
D. L. Dill and J. Rushby. Acceptance of formal methods: Lessons from hardware design. IEEE Computer, 29(4):23–24, Apr. 1996.
R. Hähnle and A. Ranta. Connecting OCL with the rest of the world. In J. Whittle, editor, Workshop on Transformations in UML at ETAPS, Genova, Italy, Apr. 2001.
Object Modeling Group. Unified Modelling Language Specification, v1.4, Sept. 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ahrendt, W. et al. (2002). The Key System: Integrating Object-Oriented Design and Formal Methods. In: Kutsche, RD., Weber, H. (eds) Fundamental Approaches to Software Engineering. FASE 2002. Lecture Notes in Computer Science, vol 2306. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45923-5_23
Download citation
DOI: https://doi.org/10.1007/3-540-45923-5_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43353-8
Online ISBN: 978-3-540-45923-1
eBook Packages: Springer Book Archive