The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel,
Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski,
Andreas Roth, Steffen Schlager, Peter H. Schmitt
KeY is a tool that provides facilities for formal specification and
verification of programs within a commercial platform for UML based
software development. Using the KeY Tool, formal methods and
object-oriented development techniques are applied in an integrated
manner. Formal specification is performed using the Object Constraint
Language (OCL), which is part of the UML standard. KeY provides
support for the authoring and formal analysis of OCL constraints. The
target language of KeY based development is Java Card, a proper
subset of Java for smart card applications and embedded systems.
KeY uses a dynamic logic for Java Card to express proof
obligations, and provides a state-of-the-art theorem prover for
interactive and automated verification. Apart from its integration
into UML based software development, a characteristic feature of KeY
is that formal specification and verification can be introduced
incrementally.