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.

Contents

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
Lectures
Tutorials

Weekly lectures 4 h, weekly exercises 2h.

Teaching language

English

Evaluation

Numeric 1-5.

Recommended year of study

First or second year of M.Sc. studies.

Study materials

Lecture notes.

Belongs to following study modules