| Software and Systems Modeling manuscript No. (will be inserted by the editor) Regular Paper The KeY Tool ⋆ Integrating Object Oriented Design and Formal Verification (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract 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 ⋆ The research reported here has been partially supported by STINT, Veten-skapsr˚adet, Vinnova, and DFG. 2 Wolfgang Ahrendt et al. 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. Key words object-oriented design—formal specification—formal verification—UML—OCL—design patterns—JAVA 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||