<p>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 a 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.</p> <p>In this thesis, our primary concern is the problem of establishing that systems, 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. We represent essential characteristics of the system (or its requirements) as predicates in a formal logic. The problem of establishing required correctness properties for the system is then reduced to the problem of establishing that a set of logical formulae hold. This is known as the verification problem. Our verification method, TOP, is mainly applicable to systems with complex control structures and simple data structures, and is tailored to systems that are designed not to terminate, and which often exhibit nondeterministic behaviour i.e., different runs of the system may produce different results, for the same inputs. Examples of such systems are operating systems, computer hardware, communications protocols, telecommunications systems, and control systems.</p> <p>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). This is desirable, because automated methods are applicable only to a limited class of systems. They are severely limited by the size of the state space generated by the abstract program denoting the system description - current limits are in the region of 108 states - roughly the number of states that could be generated by a program with a single 32-bit integer variable. Theorem proving approaches, while more general, are tedious and require specialised knowledge (the ability to provide proofs) on the part of verifiers. When carried out manually, proofs also tend to be error-prone. Theorem proving is particularly valuable in cases where the effort invested in carrying out a verification may be amortised over several projects (good examples are communications protocol specifications and distributed algorithms). Theorem proving can benefit tremendously from appropriate mechanical support, which can automate the tedious parts, in addition to playing the part of a relentless skeptic who demands the utmost precision and rigour in proofs. By presenting verifiers with a unified framework, therefore, we hope to extend the range of verification to systems that cannot be verified by either method alone.</p> <p>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. We also describe the details of system SNAP which has been built with this interface. SNAP has been designed for the purpose of checking proofs, in addition to providing partial automation of proofs. SNAP additionally allows users to carry out proofs at the desired level of abstraction. To support this, SNAP includes proof libraries and simplification algorithms based on conditional term rewriting.</p> <p>Our method, TOP, has been used to verify problems derived from practice. We present two case studies that involved the use of TOP. In the first study, we provide a formal semantics for a tabular notation for requirements documents in terms of MELA. We then use model checking and theorem proving to establish certain "safety assertions" for the requirements specification of a system that mediates access to data shared by two processes. In the second study, we analyse liveness violations in a communications protocol standard, and verify that suggested changes to the standard have indeed fixed the problem. Finally, we conclude by describing ongoing work and suggestions for future research.</p> / Doctor of Philosophy (PhD)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/6965 |
| Date | January 1996 |
| Creators | Bharadwaj, Ramesh |
| Contributors | Parnas, David L., Electrical Engineering |
| Source Sets | McMaster University |
| Detected Language | English |
| Type | thesis |
Page generated in 0.0039 seconds