Integrating Object-oriented Design and Deductive Verification of Software

Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt


Formal methods can only gain widespread use in industrial software
development if they are integrated into software development
techniques, tools, and languages that are used in practice.

The objective of this tutorial is to show how formal specification and
deductive verification of object-oriented programs can be done within
a software development platform that supports contemporary design and
implementation methodologies.  The KeY System (developed by the
tutorial presenters) is used for demonstration purposes, which
implements our approach and integrates formal methods into the
commercial CASE tool Borland Together Control Center 6.2 and,
alternatively, the open extensible IDE Eclipse.

The tutorial covers: (a) The design and formal specification of
object-oriented programs using the Unified Modeling Language (UML), in
particular UML class diagrams, and the Object Constraint Language
(OCL). (b) The deductive analysis of design and formal
specification. (c) The deductive verification of implementations
w.r.t. their specification, with Java as the target implementation
language. (d) Case studies and critical assessment.

Though we concentrate in this tutorial on particular languages
(UML/OCL, Java), the presented ideas, problems, and solutions apply to
other object-oriented design and implementation languages as well.

More information on the tutorial and the KeY project can be found at
https://www.key-project.org/SEFM06-tutorial.