Specification and Verification of Concurrency in OBJC

A software system can be very difficult to construct correctly, and when concurrency is introduced to increase performance or reliability, the task often becomes even more difficult. For a large system, many people with a variety of skills and responsibilities must be involved, and that can cause additional problems. A typical division of labor is: users develop requirements for the system, analysts build and refine specifications from the requirements, and programmers write an implementation from the refined specification. When specifications are executable, they provide a touchstone for all three parties. This dissertation presents a new concurrent specification language named OBJC. In addition to describing the language and its interpreter, a methodology for specifying concurrent software systems and verifying the correctness of those specifications is demonstrated.

There are many specification languages, and even several concurrent specification languages. Some are executable, but most offer no testing support. Some have formal semantics, but most offer no verification support. Some are based on computation models found in programming languages and thus allow a specification to be refined into a reasonably recognizable implementation, but most are mathematical notations. An OBJC specification is executable, verifiable, and implementable. Execution is by equational rewriting. Verification is by a combination of structural induction and monitor induction. Implementation is by message passing.

The most notable contribution of this dissertation is the definition, implementation, and demonstration of OBJC. OBJC embodies a new protocol for equational message passing, which is realized as a parameterized module that can be imported into an ordinary equational specification. An operational semantics based on an abstract message-passing rewrite-rule machine and an equational semantics based on a transformation to ordinary equational semantics is given. Several example specifications are also given, including a specification of SMTP, the Internet mail protocol. These examples utilize a new equational-specification model called the client/server model. Verification of OBJC specifications is also demonstrated, and several new techniques for using a rewrite-rule system as a verification tool are presented. These include message-induction, which is a combination of structural induction and monitor induction, and a kind of symbolic evaluation that is tailored for message passing.