 |
This article or section needs sources or references that appear in reliable, third-party publications. Primary sources and sources affiliated with the subject of the article are generally not sufficient for a Wikipedia article. Please include more appropriate citations from reliable sources, or discuss the issue on the talk page. (July 2008) |
 |
The introduction to this article provides insufficient context for those unfamiliar with the subject. Please help improve the article with a good introductory style. |
KeY is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software. It supports programs written in Java (more precisely: in a superset of Java Card) and specifications written in JML or OCL. At the core of the system is a deductive theorem prover. It employs a free variable sequent calculus for first-order dynamic logic for Java Card.
The development of KeY has been started in autumn 1998 and is an ongoing effort. KeY is jointly developed by the University of Karlsruhe, Chalmers University of Technology in Gothenburg, and the University of Koblenz. It is licensed under the GPL.
Contents |
Java Card DL
The theoretical foundation of KeY is a formal logic called Java Card DL. It is a version of dynamic logic tailored to Java Card programs. As such, it for example allows statements (formulas) like p → [j]q, which intuitively says that q must hold in all program states reachable by executing the Java Card program j in any state that satisfies p. Proofs of the validity of such formulas can then be performed by means of a sequent calculus and symbolic execution.
Other Supported Logics
Besides the core tool based on Java Card DL, there are several variants of KeY which support reasoning for other kinds of logics:
- Dynamic Logic for MISRA C [1] (KeY-C) (*)
- Differential dynamic logic (dL) [2] (KeYmaera [3], external) (*)
- Logic for Abstract state machines [4] (ASMKeY, external)
- A logic for JCSP programs [5]
(*) under active development/maintained
Variants of the KeY System
KeY for C
KeY for C is an adaption of the KeY System to MISRA C, a subset of the C programming language.
Symbolic Execution Debugger
The Symbolic Execution Debugger visualizes the control flow of a program as a symbolic execution tree that contains all feasible execution paths through the program up to a certain point.
The Symbolic Execution Debugger is provided as a plugin to the Eclipse development platform.
KeY-Hoare
KeY-Hoare is built on top of KeY and features a Hoare calculus with state updates. State updates are a means of describing state transitions in a Kripke structure.
KeYmaera
KeYmaera [6] (previously called HyKeY) is a deductive verification tool for hybrid systems based on a calculus for the differential dynamic logic dL [7]. It extends the KeY tool with Mathematica and corresponding algorithms and proof strategies such that it can be used for practical verification of hybrid systems.
KeYmaera has been developed at the University of Oldenburg.
KeY Test Case Generator
KeY is usable as a model-based testing tool that can generate unit tests for Java programs. The model from which test data and the test case are derived consists of a formal specification (provided in JML or OCL) and a symbolic execution tree of the implementation under test which is computed by the KeY system.
Sources
- Verification of Object-Oriented Software: The KeY Approach. Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.). Springer, 2007. ISBN 978-3-540-68977-5.
- The KeY Tool. Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. Software and Systems Modeling, Springer, 2005.
- Programming With Proofs: Language Based Approaches To Totally Correct Software. Aaron Stump. Verified Software: Theories, Tools, and Experiments, 2005.
- Beispielanwendung KeY VESK. German only.
See also
External links
No comments have been added.
