Formal methods for object oriented programming
185.073
AK der Theoretischen Informatik 4
VU, 2.0 Std. (WS 2000/2001)

Last Change: January 19, 2001

The Postscript version of this document.

Vorbemerkung

Sprache

Diese Vorlesung habe ich für Studenten an der Chalmers University of Technology entwickelt und dort Im September 2000 gehalten. Alle Unterlagen, insbesondere die Folien, sind daher auf Englisch. Die Vorlesung selbst kann ich nach Wunsch auf Deutsch oder Englisch abhalten. Sie können natürlich auch alle Übungen auf Deutsch erledigen.

Voraussetzungen

Sie sollten Grundkenntnisse in einer objekt-orientierten Programmiersprache wie zum Beispiel C++ oder JAVA haben. Sie brauchen ebenfalls Grundkenntnisse in der formalen Logik.

Sie benötigen keine Spezialkenntnisse. Als Vorbereitung für die Vorlesung empfehle ich Ihnen die Lektüre des Übersichtsartikels [1].

Alle weiteren Informationen finden Sie weiter unten.

1. Introduction

In this course I would like to introduce you into a new and emerging research area, which can perhaps be paraphrased as Integrated Logic-Based Tools in Object-Oriented Software Design. There really is no established term to describe it, because software developers and logicians traditionally used to live on different planets.

So, what I am trying to do is, in a nutshell, to make the wealth of existing logic-based methods for formal software specification and verification accessible to designers and implementors of object-oriented programs who do not have much training in theory. In Section 2 below I give some more details and spell out reasons why I think this is a great idea.

Hence, the topics of my lectures span over a fairly broad range of topics: object-oriented modeling of software, specification languages, program verification and theorem proving. As a consequence, the course will be broad rather than deep.

At this point you may well wonder about a few things:

How can one guy pull off such an ambitious project single-handedly? Well, of course, he can't. I am doing this work in collaboration with colleagues in Germany and Sweden, the so-called KeY-project. It is described in Section 3.

Why should I spend one week learning about Reiner's hobbyhorse (if it were not for the credits)? I hope that you will learn, or at least hear about, a few interesting things that you find useful even if you don't buy into the rest. Among other things, I will talk about: CASE tools, the Unified Modeling Language (UML), Patterns for software design, JAVA and JAVA CARD. Then I will suggest ways how to link the software developer's world with tools and methods for logic-based verification. You will get a crash course on axiomatic semantics for programming languages (exemplified by JAVA) and automated proof search with tableau calculi.

What do I need to know to benefit from this course? I strive to make it self-contained, but, in particular if you have a math background, you might be unfamiliar with some things. First, I recommend you to read an overview article [1], which gives a good idea of the topics discussed in the course. If you understand everything in it, fine. Otherwise, I've put together a list of resources (many online) in Section 4.3 below. You can send me an email anytime, if you would like to discuss with me or if you have questions.

More questions? Links that don't work? Missing anything? Please let me know, right now!

2. The Need for Integrated Logic-Based Tools in
Object-Oriented Software Design

While formal methods are by now well established in hardware and system design (the majority of producers of integrated circuits are routinely using BDD-based model checking packages for design and validation), usage of formal methods in software development is currently confined essentially to academic research projects. There are industrial applications of formal software development [6], but they are still exceptional [8].

The limits of applicability of formal methods in software design are not defined by the potential range and power of existing approaches. Several case studies clearly demonstrate that computer-aided specification and verification of realistic software is feasible [17]. The real problem lies in the excessive demand imposed by current tools on the skills of prospective users:

Tools for formal software specification and verification are not integrated into industrial software engineering processes.
User interfaces of verification tools are not ergonomic: they are complex, idiosyncratic, and are often without graphical support.
Users of verification tools are expected to know syntax and semantics of one or more complex formal languages. Typically, at least a tactical programming language and a logical language are involved. And even worse, to make serious use of many tools, intimate knowledge of employed logic calculi and proof search strategies is necessary.

Successful specification and verification of larger projects, therefore, is done separately from software development by academic specialists with several years of training in formal methods, in many cases by the tool developers themselves.

While this is viable for projects with high safety and low secrecy demands, it is unlikely that formal software specification and verification will become a routine task in industry under these circumstances.

The future challenge for formal software specification and verification is to make the considerable potential of existing methods and tools feasible to use in an industrial environment. This leads to the requirements:

Tools for formal software specification and verification must be integrated into industrial software engineering procedures.
User interfaces of these tools must comply with state-of-the-art software engineering tools.
The necessary amount of training in formal methods must be minimized. Moreover, techniques involving formal software specification and verification must be teachable in a structured manner. They should be integrated in courses on software engineering topics.

To be sure, the thought that full formal software verification might be possible without any background in formal methods is utopian. An industrial verification tool should, however, allow for gradual verification so that software engineers at any (including low) experience level with formal methods may benefit. In addition, an integrated tool with well-defined interfaces facilitates ``outsourcing'' those parts of the modeling process that require special skills.

Another important motivation to integrate design, development, and verification of software is provided by modern software development methodologies which are iterative and incremental. Post mortem verification would enforce the antiquated waterfall model. Even worse, in a linear model the extra effort needed for verification cannot be parallelized and thus compensated by greater work force. Therefore, delivery time increases considerably and would make formally verified software decisively less competitive.

3. The KeY Project

Since November 1998 I work on a project addressing the goals outlined above. It is called the KeY project (read ``key'' and write ``KeY'', if you lack the special font). The project is carried out in close collaboration with University of Karlsruhe. Its aim is to integrate formal software specification and verification into the industrial software engineering processes.

In the principal use case of the KeY system there are actors who want to implement a software system that complies with given requirements and formally verify its correctness. The system is responsible for adding formal details to the analysis model, for creating conditions that ensure the correctness of refinement steps (called proof obligations), for finding proofs showing that these conditions are satisfied by the model, and for generating counter examples if they are not. Highlights of KeY are:

We concentrate on object-oriented analysis and design methods (OOAD), because of their key role in today's software development practice, and on JAVA as the target language. In particular, we use the Unified Modeling Language (UML) [23] for visual modeling of designs and specifications and the Object Constraint Language (OCL) for adding further restrictions. This choice is supported by the fact, that the UML (which contains OCL since version 1.2) is not only an OMG standard, but has been adopted by all major OOAD software vendors and is featured in recent OOAD textbooks [21].
We use a commercial CASE tool as starting point and enhance it by additional functionality for formal specification and verification. The current tool of our choice is TogetherSoft's TOGETHER 4.
Formal verification is based on an axiomatic semantics of the real programming language JAVA CARD [28] (soon to be replaced by Java 2 Micro Edition, J2ME).
As a case study to evaluate the usability of our approach we develop a scenario using smart cards with JAVA CARD as programming language [11,15]. JAVA smart cards make an extremely suitable target for a case study:
- As an object-oriented language, JAVA CARD is well suited for OOAD;
- JAVA CARD lacks some crucial complications of the full JAVA language (no threads, fewer data types, no graphical user interfaces);
- JAVA CARD applications are small (JAVA smart cards currently offer 16K memory for code);
- at the same time, JAVA CARD applications are embedded into larger program systems or business processes which should be modeled (though not necessarily formally verified) as well;
- JAVA CARD applications are often security-critical, thus giving incentive to apply formal methods;
- the high number (usually millions) of deployed smart cards constitutes a new motivation for formal verification, because, in contrast to software run on standard computers, arbitrary updates are not feasible;
Through direct contacts with software companies we check the soundness of our approach for real world applications (some of the experiences from these contacts are reported in [2]).

The KeY system consists of three main components:

$\includegraphics [width=.9\textwidth]{key-tool.eps}$

The modeling component: this component is based on the CASE tool and is responsible for all user interactions (except interactive deduction). It is used to generate and refine models, and to store and process them. The extensions for precise modeling contains, e.g., editor and parser for the OCL. Additional functionality for the verification process is provided, e.g., for writing proof obligations.
The verification manager: the link between the modeling component and the deduction component. It generates proof obligations expressed in formal logic from the refinement relations in the model. It stores and processes partial and completed proofs; and it is responsible for correctness management (to make sure, e.g., that there are no cyclic dependencies in proofs).
The deduction component. It is used to actually construct proofs--or counter examples--for proof obligations generated by the verification manager. It is based on an interactive verification system combined with powerful automated deduction techniques that increase the degree of automation; it also contains a part for automatically generating counter examples from failed proof attempts. The interactive and automated techniques and those for finding counter examples are fully integrated and operate on the same data structures.

Although consisting of different components, the KeY system is going to be fully integrated with a uniform user interface.

A first KeY system prototype has been implemented, integrating the CASE tool TOGETHER and the system IBIJa [12] as (interactive) deduction component (it has limited capabilities and lacks the verification manager). Work on the full KeY system is in progress.

4. The Lectures

1. Schedule

The lectures will take place at:

Institut für Computersprachen 185.2
Favoritenstraße 9/Stiege 1/3. Stock (gelber Bereich)
Seminarraum der Abteilung

The first lecture is on Monday, 22 January 2001, 11:00. The course will be finished by Friday, 26 January 2001, 16:00. We can shift the times around a little, if there is a problem for you. This is perhaps best discussed at the first lecture.

Mon Tue Wed Thu Fri

9-11 -- -- -- -- --

11-13 Lecture 1 Lecture 2 Lecture 3 Lecture 4 Lecture 5

14-15 -- -- -- -- --

15-16 -- Exercise Exercise -- Exercise

16-18 -- -- -- -- --

2. Description and Slides for each Lecture

Overview -- Motivation -- Introduction to object-oriented modeling with UML
gzipped Postscript, ditto, 4 pages on 1
Introduction to OCL and Design Patterns
gzipped Postscript, ditto, 4 pages on 1
Automatic Generation of OCL Constraints driven by Design Patterns
Relating OCL, natural language, and logic
gzipped Postscript, ditto, 4 pages on 1
gzipped Postscript, ditto, 4 pages on 1
Automated Proof Search with Tableau Systems
gzipped Postscript, ditto, 4 pages on 1
A Dynamic Logic for JAVA CARD
gzipped Postscript, ditto, 4 pages on 1
gzipped Postscript, ditto, 4 pages on 1
gzipped Postscript, ditto, 4 pages on 1

3. Resources

1. OOAD/OOM

A good introduction to object-oriented analysis & software design (OOAD) and object-oriented modeling (OOM) is [21]. A brief and useful account is also in [9]. Another, very useful and comprehensive reference is [22].

2. UML

A comprehensive collection of UML resources.

The final specification of the UML, version 1.3, is freely available from the OMG [23]. Don't print out the whole set -- it has close to 1,000 pages and is not useful of learning the UML!

Standard books on the UML are [5,25,18]; they are reviewed at Dr. Dobb's Electronic Review of Computer Books and Software Development Online's UML page. I ordered these books for our library and they are available from me.

An excellent introduction to the UML and my personal recommendation is [9]. The library has it and you can borrow my own copy.

A bibliography on the UML is maintained at University of Bremen.

3. OCL

The latest specification of the Object Constraint Language (OCL) [30], the language developed to express non-graphical constraints about an object model, is in [23, Chapter 7]. For your convenience, I put a gzipped Postscript file containing this chapter here.

OCL can be used, for example, to specify invariants on classes and types in the class model or to describe pre- and post conditions on operations and methods.

The standard book on OCL is [29], briefly reviewed at Dr. Dobb's Electronic Review of Computer Books.

A critical discussion of the OCL is in the paper [14]. A more partisan view is expressed in [19].

Free OCL parsers from IBM and University of Technology Dresden as well as a collection of OCL resources are available.

It is not too difficult to give a formal semantics to OCL (and I give several examples in the lecture). In the literature one can find a denotational [24] as well as model theoretic semantics [27].

4. Design Patterns

The best and most important book on Design Patterns is [10]. It is available in the Hauptbibliothek as well as in the library of Abt.Progr.spr.u.Übers E185.

A brief and good introduction is [7]. Also very nice is the article at www.enteract.com/~bradapp/docs/patterns-intro.html.

Here and here are comprehensive collections of electronic resources on design patterns.

The application of design patterns to the generation of OCL constraints discussed in the lecture is described in the paper [3] (in German).

5. Dynamic Logic

Dynamic logic goes back to Pratt and the mid seventies, but don't try to read the original papers. There is a lengthy (and mostly very technical) overview article [16]. More recent and digestable is [20]. A brief description of the Java version of DL we are using in KeY is [4].

6. Automated Deduction

I wrote a lengthy overview article that covers what I discuss in the lecture (and probably more than you ever want to know) [13]. A preprint is available here.

4. Passing the Course

I will give you an assignment on Monday, Tuesday, and Thursday. You may work in pairs to solve it (if you prefer). The assignment can be found on the last one or two slides of the respective day's lecture.

The idea is that you hand in your solution on the following day in the afternoon, and then we discuss the solutions together. The nature of this course implies that there is usually no unique solution, and one can argue about advantages and disadvantages. Every participant should briefly present and defend one solution during the course. In addition, I will check your hand-ins.

In general, you are welcome to slightly modify my assignments, if you have something that interests you more, but please ask me beforehand.

The grade is based on the quality of your solutions and your actiuve contribution in the exercises. There is no separate written exam.

Bibliography

1: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. Schmitt.
The KeY approach: Integrating object oriented design and formal verification.
In Manuel Ojeda-Aciego, Inma P. de Guzmán, Gerhard Brewka, and Luís Moniz Pereira, editors, Proc. 8th European Workshop on Logics in AI (JELIA), volume 1919 of LNCS, pages 21-36. Springer-Verlag, October 2000.
URL: ftp://ftp.cs.chalmers.se/pub/users/reiner/jelia.ps.gz.
2: Thomas Baar.
Experiences with the UML/OCL-approach to precise software modeling: A report from practice.
In Proc. Net.ObjectDays, Erfurt, Germany, 2000.
URL: http://i12www.ira.uka.de/~key/doc/2000/baar00.pdf.gz.
3: Thomas Baar, Reiner Hähnle, Theo Sattler, and Peter H. Schmitt.
Entwurfsmustergesteuerte Erzeugung von OCL-Constraints.
In Gregor Snelting, editor, Softwaretechnik-Trends, Informatik Aktuell. Springer-Verlag, 2000.
URL: http://i12www.ira.uka.de/~key/doc/2000/baarsattlerea00.pdf.gz.
4: Bernhard Beckert.
A dynamic logic for java card.
In Proc. 2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France, 2000.
URL: http://i12www.ira.uka.de/~key/doc/2000/beckert00.pdf.gz.
5: Grady Booch, James Rumbaugh, and Ivar Jacobson.
The Unified Modeling Language User Guide.
Object Technology Series. Addison-Wesley, Reading/MA, 1999.
6: Edmund Clarke and Jeanette M. Wing.
Formal methods: State of the art and future directions.
ACM Computing Surveys, 28(4):626-643, 1996.
7: James O. Coplien.
Software Patterns.
SIGS Management Briefings. SIGS, New York, 1996.
8: David L. Dill and John Rushby.
Acceptance of formal methods: Lessons from hardware design.
IEEE Computer, 29(4):23-24, April 1996.
Part of [26].
9: Martin Fowler and Kendall Scott.
UML Distilled: Applying the Standard Modeling Object Language.
Object Technology Series. Addison-Wesley, second edition, 2000.
10: Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides.
Design Patterns: Elements of Reusable Object-Oriented Software.
Addison-Wesley, Reading/MA, 1995.
11: Scott B. Guthery.
Java Card: Internet computing on a smart card.
IEEE Internet Computing, 1(1):57-59, 1997.
12: Elmar Habermalz.
Interactive theorem proving with schematic theory specific rules.
Technical Report 19/00, Fakultät für Informatik, Universität Karlsruhe, 2000.
URL: http://i12www.ira.uka.de/~key/doc/2000/stsr.ps.gz.
13: Reiner Hähnle.
Tableaux and related methods.
In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, to appear, 2001.
14: Ali Hamie, Franco Civello, John Howse, Stuart J. H. Kent, and Richard Mitchell.
Reflections on the object constraint language.
In Pierre-Alain Muller and Jean Bézivin, editors, Proc. International Conference on the Unified Modelling Language (UML) 1998, Mulhouse, France, number 1618 in LNCS. Springer-Verlag, 1999.
15: U. Hansmann, M. S. Nicklous, T. Schäck, and F. Seliger.
Smart Card Application Development Using Java.
Springer-Verlag, 2000.
16: David Harel.
Dynamic logic.
In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, chapter 10, pages 497-604. Reidel, Dordrecht, 1984.
17: Michael G. Hinchey and Jonathan P. Bowen, editors.
Applications of Formal Methods.
Prentice Hall, 1995.
18: Ivar Jacobson, James Rumbaugh, and Grady Booch.
The Unified Software Development Process.
Object Technology Series. Addison-Wesley, Reading/MA, 1999.
19: Anneke Kleppe, Jos Warmer, and Steve Cook.
Informal formality? the object constraint language and its application in the UML metamodel.
In Pierre-Alain Muller and Jean Bézivin, editors, Proc. International Conference on the Unified Modelling Language (UML) 1998, Mulhouse, France, volume 1618 of LNCS. Springer-Verlag, 1999.
20: Dexter Kozen and Jerzy Tiuryn.
Logics of programs.
In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 14, pages 789-840. The MIT Press, 1990.
21: James Martin and James J. Odell.
Object-Oriented Methods: A Foundation, UML Edition.
Prentice-Hall, 1997.
22: Bertrand Meyer.
Object-Oriented Software Construction.
Prentice-Hall, Englewood Cliffs, second edition, 1997.
23: Object Modeling Group.
Unified Modelling Language Specification, version 1.3, March 2000.
OMG document formal/00-03-01. URL: http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz.
24: Mark Richters and Martin Gogolla.
On formalizing the UML object constraint language OCL.
In Tok-Wang Ling, Sudha Ram, and Mong Li Lee, editors, Proc. 17th International Conference on Conceptual Modeling (ER), volume 1507 of LNCS, pages 449-464. Springer-Verlag, 1998.
25: James Rumbaugh, Ivar Jacobson, and Grady Booch.
The Unified Modeling Language Reference Manual.
Object Technology Series. Addison-Wesley, Reading/MA, 1999.
26: Hossein Saiedian.
An invitation to formal methods.
IEEE Computer, 29(4):16-30, April 1996.
A ``roundtable'' of short articles by several authors.
27: Peter H. Schmitt.
A model-theoretic semantics for OCL.
In ??, Department of Computer Science, University of Karlsruhe, September 2000.
http://www.cs.chalmers.se/~reiner/Lehre/Wien-2001/ocl.ps.gz.
28: Sun Microsystems, Inc., Palo Alto/CA, USA.
Java Card 2.1.1 Platform API Specification, May 2000.
29: Jos Warmer and Anneke Kleppe.
The Object Constraint Language: Precise Modelling with UML.
Object Technology Series. Addison-Wesley, Reading/MA, 1999.
30: Jos Warmer and Anneke Kleppe.
OCL: The constraint language of the UML.
Journal of Object-Oriented Programming, 12(1):10-13,28, March 1999.

Footnotes

... feasible;: While JAVA CARD applets on smart cards can be updated in principle, for security reasons this does not extend to those applets that verify and load updates.
...http://www.ercb.com.: The book is based on OCL 1.2 and does not address the more recent additions.

Reiner Hähnle
2001-01-19

	Mon	Tue	Wed	Thu	Fri
9-11	--	--	--	--	--
11-13	Lecture 1	Lecture 2	Lecture 3	Lecture 4	Lecture 5
14-15	--	--	--	--	--
15-16	--	Exercise	Exercise	--	Exercise
16-18	--	--	--	--	--

Formal methods for object oriented programming 185.073 AK der Theoretischen Informatik 4 VU, 2.0 Std. (WS 2000/2001)