A course by Christoph Lüth, Shi Hui, Markus Roggenbach, and Lutz Schröder at the Universität Bremen 2001/2002.
This is a basic course on practical approaches to correct software development.The emphasis is put on applicable techniques and effective use of tools.
Sequential as well as parallel systems will be discussed, using the algebraic specification language CASL and the process calculus CSP, respectively. On the tool side, the theorem prover Isabelle and the model checker FDR will play central roles. All methods, techniques and concepts introduced in the course will be thoroughly motivated and explained by examples and reinforced by practical exercises.
Building on methods discussed in the preceding introductory course, substantial example applications such as, e.g., the verification of a communication protocol will be the focus of interest in this course. Students will have the opportunity to gather experience in modelling both sequential and parallel systems. To this end, the course will offer exercises concerned with the development of formal models and the investigation of their properties using tool support. The required background will be discussed in further depth in the accompanying lectures.
Your solution of the final exercise should be in correct CASL (i.e. cats -input=empty,static "solution.casl" should run without error messages).