Fair smg and linear time model checking

Abstract

SMG [GB88] is a system designed to generate a finite state model of a program from the program itself and an operational semantics for the programming language. Model-checking can then be used to verify that the program satisfies a set of desired temporal properties. In this paper we first show how we have incorporated notions of fairness into SMG; in particular, a user is now able to define semantics with “fair” constructs, for example, parallel composition, repetitive choice, etc. A program may contain several fair constructs, each with its own fairness type. Secondly we describe a practical approach to model checking of linear temporal formulae over the fair structures generated by the new SMGF. Our approach is a refinement and extension of the fair-satisfiability algorithms, presented earlier by Lichtenstein and Pnueli [LP85], together with techniques developed in our practical implementations of decision procedures for linear temporal logic [Gou84].