Dines Bjørner's Course Web Page
Department of Information Technology
Computing Science Division
Uppsala University, Sweden

Host: Prof., Dr. Lars-Henrik Eriksson

E-Mail: Lars-Henrik.Eriksson@it.uu.se

E-Mail: bjorner@gmail.com, URL: www.imm.dtu.dk/~db
Course Dates: 8-19 November
Compiled: October 27, 2010

Dines Bjørner's Home Page


Contents

An Eye-Opener Course

Stop Press !

  1. Slight course rescheduling, new texts and slides: Monday October 1. 2010
  2. Creation of this Web page: Tuesday June 8, 2010

Course Data - Uppsala Format

The information [1-6] given in this section takes precedence over information given elsewhere in this document.

[1] Entry Requirements

60 ECTS credits at the advanced [Master's] level
Basic understanding of Functional Programming
Basic understanding of simple Mathematical Logic, Discrete Mathematics: sets, sequences, functions, Cartesian products.

[2] Grading System

Pass/Fail

[3] Learning Outcome

In order to pass, the student must be able to

[4] Contents

Phases of Software Engineering, including Domain Engineering and Requirements Engineering.

Precise natural language for specification.

Formal specification languages.

Methodological stages of Domain Engineering.

[5] Instruction

Lectures, lesson, seminars, project.

[6] Examination

Written examination (3 ECTS credits) and a project (4,5 ECTS credits).

[7] Reading List

Course notes by the instructor.

See "clickable" URLs in Section Lecture Timetable and Course Texts and Slides below.

Overview

This Web page, with its sub-Web pages, provides information about the course to be given at Eötvös Loránd University.

Lecture Timetable and Course Texts and Slides

Lect.No. Subject Day Text Slides
1 Summary + Introduction Mon.08.11.2010 Sects. 0-1 Lecture 1
2 A Specification Ontology Mo.08.11.2010 Sect. 2 Lecture 2
3 Domain Engineering, I Tue.09.11.2010 Sects. 3.1-3.4 Lecture 3
4 Domain Engineering, II Wed.10.11.2010 Sects. 3.5-3.7 Lecture 4
5 Requirements Engineering Thu.11.11.2010 Sects. 4.-4.2.3 Lecture 5
6 Requirements Engineering Fri.12.11.2010 Sects. 4.2.4-4.4.1 Lecture 6
7 RSL Types Mon.15.11.2010 App. 1.1 Lecture 7
8 RSL Values and Operations Tue.16.11.2010 App. 1.2 Lecture 8
9 RSL Logic, Fcts. and Appl.Spec. Wed.17.11.2010 Apps. 1.3-1.5 Lecture 9
10 RSL Imperativeness, Concurrency and Specifications Thu.18.11.2010 Apps. 1.6-1.7 Lecture 10.1
11 Conclusion Fri.19.11.2010 Sect. 5 Lecture 11

Course Prerequisites

Aims and Objectives

Aims

Objectives

Students may, instead of in RAISE/RSL [4,5,2], work out the formal aspects of their course report in Alloy [6], Event B [1], VDM-SL [3], Z [7], etc., or in good, simple and reliable Mathematics !

Exam

Course Project

Topics

Course Groups

Course Work

Course Report

Project Report and Exam Evaluation

References

Bibliography

1
J.-R. Abrial.
The B Book: Assigning Programs to Meanings and Modeling in Event-B: System and Software Engineering.
Cambridge University Press, Cambridge, England, 1996 and 2009.

2
D. Bjørner.
Software Engineering, Vol. 1: Abstraction and Modelling; Vol. 2: Specification of Systems and Languages; ol. 3: Domains, Requirements and Software Design.
Texts in Theoretical Computer Science, the EATCS Series. Springer, 2006.

3
J. Fitzgerald and P. G. Larsen.
Modelling Systems - Practical Tools and Techniques in Software Development.
Cambridge University Press, Cambridge, UK, Second edition, 2009.

4
C. W. George, P. Haff, K. Havelund, A. E. Haxthausen, R. Milne, C. B. Nielsen, S. Prehn, and K. R. Wagner.
The RAISE Specification Language.
The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead, England, 1992.

5
C. W. George, A. E. Haxthausen, S. Hughes, R. Milne, S. Prehn, and J. S. Pedersen.
The RAISE Development Method.
The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead, England, 1995.

6
D. Jackson.
Software Abstractions: Logic, Language, and Analysis.
The MIT Press, Cambridge, Mass., USA, April 2006.
ISBN 0-262-10114-9.

7
J. C. P. Woodcock and J. Davies.
Using Z: Specification, Proof and Refinement.
Prentice Hall International Series in Computer Science, 1996.

Some of My Books

Formalisation Approaches

URLs to Formal Methods Web Pages

As of August 26, 2010, the below URLs were OK.

Formal Method Links

A "Chatty" CV

For an unconventiomal CV click this.

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...

About this document ...

Dines Bjørner's Course Web Page
Department of Information Technology
Computing Science Division
Uppsala University, Sweden

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 -toc_depth 6 index

The translation was initiated by Dines Bjorner on 2010-10-27

Dines Bjorner 2010-10-27