Formale Spezifikation von Softwaresystemen /

Formal Specification of Software Systems


Prof. Heinrich Hußmann

Technische Universität Dresden

Vorlesung mit Übung (2+2 SWS, 6 ECTS Credits)

Wintersemester 2001/2002


Zeit und Ort:

 Vorlesung: Dienstag,  5. DS (14:50 Uhr), Hörsaal GRU 350
  Übung: Freitag, 3. DS (11:10 Uhr), Hörsaal GRU 350 (und gelegentlich GRU 108, siehe untenstehende Übersicht)

Time and Location:

Lecture: Tuesday, 14:50, Room GRU 350
Exercises: Friday, 11:10, Room GRU 350 (and sometimes GRU 108, see timetable below)

Please note: Deadline for projects is March 30. Earlier delivery is welcome.


Hinweis für Informatik-Studenten:

Diese Lehrveranstaltung wird sowohl für die Vertiefungsrichtung Softwaretechnologie als auch für den internationalen Studiengang Computational Logic angeboten. Aus diesem Grund wird die Lehrveranstaltung in englischer Sprache durchgeführt und sind alle Lehrmaterialien in englischer Sprache verfaßt. Die Auseinandersetzung mit Fachthemen in englischer Sprache ist in sich ein durchaus wichtiger Gegenstand des Studiums. Bei Bedarf wird deutschsprachigen Studenten eine gewisse Hilfestellung bei Sprachproblemen gegeben.

Die Übungen schließen auch praktische Arbeit am Rechner ein. Ein Teil der Übungszeit wird deshalb als praktische Gruppenübung in einem Rechnerlabor abgehalten werden.
 

Notice for students of Computational Logic:

This lecture is held jointly for the International Master Programme in Computational Logic and for German-speaking students of the main Computer Science programme with a specialisation in Software Engineering. The lecture will be held in English language, and all accompanying material is in English.

Examination type:

The examination will be based on practical work in the exercises. Every participant is expected to carry out some small practical projects using special software systems supporting formal specification methods. Opportunity for this project work, including access to an appropriate computer lab, will be given during the exercises hours.


Summary:


Construction of large software systems requires notations and techniques for abstract modelling of software structures. Current development practice mainly relies on diagrammatic, informal notations, but there is a clear long-term trend towards higher formalisation in software specification. This lecture builds a bridge between practically used specification notations from software engineering (like the Unified Modeling Language UML) and pure formal specification approaches based on mathematical logic.
This lecture is located right in the middle between the two areas of formal methods and traditional software engineering methods. The lecture deliberately takes a different approach to most textbooks on formal specification. Traditionally, formal methods are presented like a sub-discipline of mathematical logic, with strong emphasis on the mathematical foundations. In this lecture, a pragmatic, application-driven approach to formal concepts is taken. Mathematical definitions and concepts are used only where there is a clear advantage from their usage.
Technically, the lecture puts particular emphasis to an algebraic approach for formal system specification, but briefly covers also several other specification formalisms. For the software engineering side, an object-oriented approach based on the UML notation is assumed.

The main topics are:

Prerequisites: Elementary knowledge in mathematical logic and in software engineering


Literature:

Further reading:



Outline of Lecture and Lecture Materials:

Notice: For accessing the lecture notes, identification by a user name and password is required. This information will be given in the lecture.

1.  Formal Specification of Software: Why and When?

Lecture of 9 October
Slides
Lecture notes: Preliminaries Chapter 1
1.1 Purpose of Specifications
1.2 Specification Examples
1.3 Formality
1.4 Overview of Formal Specification Languages
1.5 Reminder on Mathematical Notation
2. Software Models in Software Engineering
Lecture of 16 October:
(Note: This lecture can be omitted by students who have attended the lecture "Softwaretechnologie". It is targeted to CL students mainly.)
Slides
Lecture notes: Chapter 2 (Sorry this chapter is very short.)
2.1 Large Software Projects
2.2 Models and Modeling from the Software Engineering Point of View
2.3 Object-Oriented Modeling
3.  Algebraic Specification (Abstract Data Types)
Lecture of 23 October:
Slides (Please note slide format has changed to to requests from students.)
Lecture notes: Chapter 3 (sections 3.1, 3.2)
Lecture of 30 October:
Slides
Lecture notes: Chapter 3 (section 3.3)
Lecture of 6 November:
Slides   Additional slide (for section 3.3)
Lecture notes: Chapter 3 (section 3.4)
Lecture of 13 November:
Slides
Lecture notes: Chapter 3 (section 3.5)
Lecture of 20 November (Part 1):
Slides
Lecture notes: Chapter 3 (section 3.6)
3.1 Syntax of Data Types: Signatures
3.2 Algebraic Semantics: Heterogeneous Algebras
3.3 Axiomatic Specification
3.4 Deduction and Evaluation: Tools
3.5 Specification Styles
3.6 Concluding Remarks on Practical Usage
4. UML Class Diagrams as a Formal Specification Language
Lecture of 20 November (Part 2):
(Note: This part of the lecture can be omitted by students who have attended the lecture "Softwaretechnologie". It is targeted to CL students mainly.)
Slides
Lecture notes: Chapter 4 (section 4.1)
Lecture of 27 November:
Slides
Lecture notes: Chapter 4 (sections 4.1 contd. and 4.2 first part)
Note: No lecture on 4 December !

Lecture of 11 December:

Slides
Lecture notes: Chapter 4 (sections 4.2 contd. and 4.3)
4.1 Object-oriented Specification with the Unified Modeling Language (UML)
4.2 UML Class Diagrams: Formal Syntax and Semantics
4.3 Object-Oriented Specification and Object-Oriented Programs
5. The Object Constraint Language (OCL) for UML
Lecture of 18 December:
Slides
Lecture notes: Chapter 5 (section 5.1)


Lecture of 8 January:

Slides
Lecture notes: Chapter 5 (section 5.2)


Lecture of 15 January:

Slides
Lecture notes: Chapter 5 (section 5.3 and 5.4)


5.1 Object Constraints in OCL: Principles and Syntax
5.2 Formal Semantics of OCL
5.3 Collection Types
5.4 Methodical Use of of OCL

6. Dynamic Models in UML as a Formal Specification Language
Lecture of 22 January:
Slides
Lecture notes: Chapter 6

6.1 Statecharts in UML: Sketch of Formal Semantics
6.2 State Models and OCL
6.3 Sequence Diagrams in UML: Sketch of Formal Semantics

7.  Outlook
Lecture of 30 January Please note the date change! Lecture shifted by two days.
Slides Chapter 7   Slides Chapter 8
Lecture notes: Chapter 7  Chapter 8 (Please note: lecture notes cover more material than lecture.)
Additional material on Dresden OCL Toolset example (high-resolution screenshots, full Java files)

7.1 Overview of the Formal Specification Language Z
7.2 IT Security and Formal Specification
7.3 Practical Usability of Formal Methods


Exercises:

Details to be announced in the first meeting, since some organizational decisions are dependent on the number of participants.

Projects: Participants are expected to carry out a small practical project in formal specification using either the  formal specification language CafeOBJ or the Object Constraint Language OCL (which is part of UML). Specific software tools have to be used to validate the produced specifications.


Schedule of locations and topics (more details will be added in due time):
 
Date
Location
Topic
Type of exercise
Additional information
12.10.
--
(no class this day)
--
--
19.10.
GRU 350
Mathematical specification
paper and pencil exercises
problem set 1
26.10.
GRU 350
Algebraic specification with OBJ
paper and pencil exercises
problem set 2
02.11.
Laboratory GRU 108
CafeOBJ Part 1
supervised lab work
 instructions to access CafeOBJ
problem set 3
09.11.
Laboratory GRU 108
CafeOBJ Part 2
supervised lab work
 problem set 4
VECTOR spec in CafeOBJ
16.11.
Laboratory GRU 108
CafeOBJ Part 3
supervised lab work;
introduction to projects
 problem set 5
CafeOBJ projects
23.11
Laboratory GRU 108
Work on OBJ projects
lab work
 --
30.11.
Laboratory GRU 108
Work on OBJ projects
lab work
 --
07.12.
Laboratory GRU 108
UML/OCL Tools Part 1
supervised lab work;
introduction to further projects
 instructions for using USE
UML/OCL projects
problem set 6
14.12.
Laboratory GRU 108
UML/OCL Tools Part 2
supervised lab work
 problem set 7
21.12.
--
(no class this day)
--
 --
11.01.
Laboratory GRU 108
UML/OCL Tools Part 3
supervised lab work
 problem set 8
18.01.
Laboratory GRU 108
Work on OCL projects
lab work
 --
25.01.
Laboratory GRU 108
Work on OCL projects
lab work
 --

 


Further Resources:

WWW-Adm. H. Hußmann, 13 February 2002