Preface

This text is a companion to the lecture Formal Specification and Verification (FSV) as part of the master program High Integrity Systems (HIS). It is intended for students with basic knowledge in computer science and/ or engineering and it is formatted for a 1-semester course. This text will and cannot replace the texts mentioned below. Rather it is a 'guide' to use these books for a course with limited scope.

As primary textbooks we will use in this course Baier et al. (2008)[28], Berard et al (2001)[34], Clarke et al. (1999)[61], as well as Schneider (2004)[250]. Other very helpful books are those from McMillan (1993)[196], Manna and Pnueli (1992)[191] and (1995)[192] as well as Girault and Valk (2003). [116].

One has to keep in mind that a complete and deep unerstanding of the subject is only possible if one reads also the original papers cited in the books. The books can only give first ideas and represent selections of some perspectives.

Here is a short historical overview of the development of some of the topics which are important for the field (cf. figure 1.1):

Figure 1.1: A simple overview about the topic formal specification and verification
\includegraphics[width=4.5in]{fsv_general_scenario.eps}

Gerd Doeben-Henisch 2010-03-03