Prof. Heinrich Hußmann
Technische Universität Dresden
Vorlesung mit Übung (2+2 SWS, 6 ECTS Credits)
Wintersemester 2001/2002
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)
Lecture: Tuesday, 14:50, Room GRU 350
Exercises: Friday, 11:10, Room GRU 350 (and sometimes GRU 108, see timetable below)
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.
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
longterm 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 subdiscipline of mathematical
logic, with strong emphasis on the mathematical foundations. In this lecture,
a pragmatic, applicationdriven 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 objectoriented
approach based on the UML notation is assumed.
The main topics are:
1. Formal Specification of Software: Why and When?
Lecture of 9 OctoberSlides
Lecture notes: Preliminaries Chapter 1
1.1 Purpose of Specifications2. Software Models in Software Engineering
1.2 Specification Examples
1.3 Formality
1.4 Overview of Formal Specification Languages
1.5 Reminder on Mathematical Notation
Lecture of 16 October:3. Algebraic Specification (Abstract Data Types)
(Note: This lecture can be omitted by students who have attended the lecture "Softwaretechnologie". It is targeted to CL students mainly.)Slides2.1 Large Software Projects
Lecture notes: Chapter 2 (Sorry this chapter is very short.)
2.2 Models and Modeling from the Software Engineering Point of View
2.3 ObjectOriented Modeling
Lecture of 23 October:Slides (Please note slide format has changed to to requests from students.)Lecture of 30 October:
Lecture notes: Chapter 3 (sections 3.1, 3.2)SlidesLecture of 6 November:
Lecture notes: Chapter 3 (section 3.3)Slides Additional slide (for section 3.3)Lecture of 13 November:
Lecture notes: Chapter 3 (section 3.4)Slides
Lecture notes: Chapter 3 (section 3.5)
Lecture of 20 November (Part 1):4. UML Class Diagrams as a Formal Specification LanguageSlides3.1 Syntax of Data Types: Signatures
Lecture notes: Chapter 3 (section 3.6)
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
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.)SlidesLecture of 27 November:
Lecture notes: Chapter 4 (section 4.1)SlidesNote: No lecture on 4 December !
Lecture notes: Chapter 4 (sections 4.1 contd. and 4.2 first part)Lecture of 11 December:
Slides
Lecture notes: Chapter 4 (sections 4.2 contd. and 4.3)
4.1 Objectoriented Specification with the Unified Modeling Language (UML)5. The Object Constraint Language (OCL) for UML
4.2 UML Class Diagrams: Formal Syntax and Semantics
4.3 ObjectOriented Specification and ObjectOriented Programs
Lecture of 18 December:6. Dynamic Models in UML as a Formal Specification LanguageSlides
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
Lecture of 22 January:7. Outlook
Slides
Lecture notes: Chapter 66.1 Statecharts in UML: Sketch of Formal Semantics
6.2 State Models and OCL
6.3 Sequence Diagrams in UML: Sketch of Formal Semantics
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 (highresolution 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
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):
























problem set 3 




VECTOR spec in CafeOBJ 



introduction to projects 
CafeOBJ projects 













introduction to further projects 
UML/OCL projects problem set 6 
























