x !
Archived Curricula Guide 2011–2012
Curricula Guide is archieved. Please refer to current Curricula Guides
TKOPS148 Introduction to Formal Specification 5–8 ECTS
Organised by
Computer Science
Person in charge
Professor Jyrki Nummenmaa.

Learning outcomes

After the course, the student should be able to write simple specifications using the above approaches, and to perform the following tasks using at least one of the specification approaches of the course:
- formulate and prove simple formal properties of the specification,
- animate and simulate a formal specification, and
- implement a formally specified system.


The course gives introductory knowledge and basic skills in formal specification, using various different approaches:
1. Exact specification of computer programs using The Z language.
2. Specification of collective, joint action behaviour of the system, using The DisCo language.
3. Specification of concurrent systems, using some variant of CSP or CCS.

The course covers introductory level material on the following themes:specification and proving formal properties of systems, simulation and animation of the specified systems, and implementing the specified systems.

Teaching methods

Teaching method Contact Online

Weekly lectures 4 h, weekly exercises 2h.

Teaching language


Modes of study

Lectures, weekly exercises, coursework, exam


Numeric 1-5.

Recommended year of study

First or second year of M.Sc. studies.

Study materials

Lecture notes.

Belongs to following study modules

School of Information Sciences
School of Information Sciences
Archived Teaching Schedule. Please refer to current Teaching Shedule.
School of Information Sciences