Tools to Support a Formal Verification Method for Systems with Concurrency and Nondeterminism

Mr. Ramesh Bharadwaj

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1


Abstract

With the availability of inexpensive computer hardware, software intensive systems are becoming sophisticated and pervasive, creating a need for software design methods that deliver robust and efficient systems. Unfortunately, most systems today are designed by trial and error, with designers having little insight into their correctness before they are implemented. The hallmark of an engineering method is the use of system models (prototypes) to verify designs by provably establishing essential characteristics of products before they are constructed. This thesis attempts to bring the craft of software construction closer to an engineering discipline, by transforming theoretical ideas in program verification and concurrency theory into concrete method for the analysis of software requirements and system specifications. In our opinion, such methods will find wider acceptance if they are adequately supported by a set of tools. This thesis also describes tools that are being developed to support our verification method.

In this thesis, our primary concern is the problem of establishing systems, that when constructed in accordance with a design, will meet their required correctness properties. We describe a verification method, TOP, in which the description of a system (i.e., its design) is expressed as an abstract program in a programming language-like notation called MeLa. Our method offers a unified framework in which correctness properties may be verified using a combination of model checking (a fully automatic method), and theorem proving (a partially automated approach). One of the common complaints about theorem proving systems is that they are bewildering to beginners and hard to use. In this thesis we present an improved user interface for theorem provers. Our method, TOP, has been used to verify problems derived from practice.