The KeY tool |
| |
| Authors: | Wolfgang Ahrendt Thomas Baar Bernhard Beckert Richard Bubel Martin Giese Reiner Hähnle Wolfram Menzel Wojciech Mostowski Andreas Roth Steffen Schlager Peter H Schmitt |
| |
| Affiliation: | (1) Department of Computing Science, Chalmers University of Technology, 41296 Gothenburg, Sweden;(2) Software Engineering Laboratory, Swiss Federal Institute of Technology in Lausanne, 1015 Lausanne EPFL, Switzerland;(3) Institute for Computer Science, University of Koblenz-Landau, 56072 Koblenz, Germany;(4) Department of Computer Science, University of Karlsruhe, 76128 Karlsruhe, Germany |
| |
| 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 formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL 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. |
| |
| Keywords: | Object-oriented design Formal specification Formal verification UML OCL Design patterns Java" target="_blank">Java |
| 本文献已被 SpringerLink 等数据库收录！ |
|
