KeY
From Wikipedia, the free encyclopedia
| This article may not meet the general notability guideline or one of the following specific guidelines for inclusion on Wikipedia: Biographies, Books, Companies, Fiction, Music, Neologisms, Numbers, Web content, or several proposals for new guidelines. If you are familiar with the subject matter, please expand or rewrite the article to establish its notability. The best way to address this concern is to reference published, third-party sources about the subject. If notability cannot be established, the article is more likely to be considered for redirection, merge or ultimately deletion, per Wikipedia:Guide to deletion. This article has been tagged since July 2007. |
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 |
[edit] 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.
[edit] 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
[edit] Variants of the KeY System
[edit] KeY for C
KeY for C is an adaption of the KeY System to MISRA C, a subset of the C programming language.
[edit] 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.
[edit] 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.
[edit] 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.
[edit] 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.
[edit] 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.
