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
Study load (hours):168
Contract restrictions: No contract restriction
Language of instruction:English
Exam period:exam in the 1st semester
Lecturer(s)Dirk Janssens

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.