After the course, the student - is able to write simple specifications using the approaches of the course, - can analyze the properties of the specified system using these specifications, - can animate and simulate a formal specification, and - understands some principles that can be used to implement the specified system.
Contents
The course gives introductory knowledge and basic skills in formal specification, using various different approaches: 1. Specification of concurrent systems using process algebras with the FSP language and LTSA tool. 2. Specification of collective, joint action behaviour of the system, using The DisCo language.
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.
Further information on prerequisites and recommendations
Recommended year of study: First or second year of M.Sc. studies.