# Specification and verification

Course Code : | 2001WETFSP |

Study domain: | Computer Science |

Bi-anuall course: | Taught in academic years starting in an odd year |

Academic year: | 2015-2016 |

Semester: | 1st semester |

Contact hours: | 45 |

Credits: | 6 |

Study load (hours): | 168 |

Contract restrictions: | No contract restriction |

Language of instruction: | English |

Exam period: | exam in the 1st semester |

Lecturer(s) | Dirk Janssens |

### 1. Prerequisites *

an active knowledge of

- English

You have successfully completed a number of more complex programming projects and you have a basic knowledge of logic and software engineering.

### 2. Learning outcomes *

- You have to be able to write a specification in each of the formalisms considered (Hoare logica and SPIN/PROMELA), starting from an informal specification in natural language. This specification should use the features offered by the languages in a sensible way: abstraction, refinement, modularity.
- You are also expected to be able to comment on a given specification, or to correct and improve a given one.
- You have to be able to explain in your own words the main characteristics of the various specification languages, their motivation, their intended application area, etc.
- You should be able to explain the constructions, motivations and proofs concerning the reachability algorithm discussed in the course, and to apply them to simple examples.

### 3. Course contents *

An important issue in the development of large software systems is the specification of its desired structural and dynamic properties. To avoid the impreciseness and ambiguities of specifications in natural language, a number of specialized formal languages, based on mathematics, have been developed: Hoare logic, Petri Nets, Process calculi, etc. Moreover, these languages are supported by tools allowing various types of analysis and verification. The SPIN system is a prominent example of that.

The course starts with an introduction into Hoare logic, an approach that has had a major impact on the development of the area.

Then a few sessions are devoted to the study of a verification problem (reachability) and it is demonstrated how a mathematical analysis of this problem leads to a flexible verification algorithm. In the last part of the course the SPIN/PROMELA verification system and its mathematical background are discussed.

### 4. Teaching method and planned learning activities

Personal work

### 5. Assessment method and criteria

Project

### 6. Study material *

#### 6.1 Required reading

For each of the specification languages discussed a number of papers and/or books will be made available.

**6.2 Optional reading**

The following study material can be studied voluntarily :For the part on program logic: an extensive treatment can be found in:

Krysztof R. Apt and Ernst-Rüdiger Olderog, Verification of Sequential and Concurrent Programs, Springer, ISBN 0-387-94896-1

### 7. Contact information *

lecturer: Dirk.Janssens@ua.ac.be