Next: General Idea Up: Verification as Model Checking Previous: Verification as Model Checking Contents
Verification represents the general case where a given formal specification S of some properties will be verified against some formal structure M. Today is this handled with the aid of socalled Kripke Structures which serve as models for the interpreted meaning of sets of formal expressions.
Historically is the story leading from first distinctions of syntax and semantics in modern logic to more and more elaborated theories very rich (cf. Dieudonné (1985)[79]:Pp.858ff, Berka and Kreiser (1973)[35]:chapter 12, Kneale and Kneale (1986/1962)[156]:Chapt.X, and Schneider (2004)[250]:Pp.16ff). As important 'milestones' one can see at least Bolzano (1781 - 1848), Frege (1828-1925) with his first distinction of syntax and semantics, then Skolem (1920, 1928) (skolemization of logic formulas, herbrand universe), Herbrand (1930), Tarski(1930, 1932, 1935)(Truth concept for formal languages), Gödel (1930, 1931)(Incompleteness or Undecidability property of first order theories), Carnap (1935, 1942, 1943, 1947)(who switched from purely syntactical conceptions of logic to more semantical versions), Schröter (1941), Henkin (1950) , Kripke (1959, 1962, 1963, 1965, 1975)(Modal Logic and Semantics), Kreisel and Krivine (1967)(Model theory).
Although there is also a rich tradition of deductive approaches to verification (cf. Schneider 2004 [250]:Pp.20ff, Siekmann and Wrightson (1983)[256], [257]), we will concentrate here on the semantic approaches, especially on so called model checking.