Specification and Verification Techniques for Parallel Programs Based on Message Passing Semantics.

摘要

This thesis presents formal specification and verification techniques for both serial and parallel programs written in SIMULA-like object oriented languages. These techniques are based on the notion of states of individual objects which are defined uniformly in serial and parallel computations. They can specify and verify the behavior of data and procedural objects in multi-process environments, thus overcoming some of the difficulties in dealing with parallelism which characterized previous work on formal specifications for abstract data types. Among others, the specifications and verifications of a bounded buffer and air line reservation systems are given. Using a model of a simple post office illustrates our specification and verification techniques for systems, such as operating systems and multi-user data base systems, which are characterized by complex internal concurrent activities. It is demonstrated that the specifications of the overall functions of the system which are called task specifications can be derived from specifications of the individual behavior and mutual interaction of the subsystems. A method of defining states of individual objects as mathematical functions is suggested.