Design and analysis of concurrent software systems (petri nets, protocols, verification)
E. Timothy Morgan · 1986
In this dissertation, the development of concurrent software systems is discussed. Mechanisms for representing concurrency in modern programming languages are reviewed, as well as formal models and techniques for analyzing and verifying concurrent systems. Two well-developed methodologies for designing concurrent systems are studied in detail. Some specific open problems are identified: obtaining feedback on concurrent systems under development, rapid prototyping of such systems, mechanisms for specifying desired behavior of these systems, and automation of the translation from the formal system specification language to a high-level, concurrent implementation language. A formal, executable specification language provides prototyping and early feedback. Therefore, a new language is proposed whose purpose is two-fold. First, it serves as the basis of a computer program for the analysis of system state spaces. This tool is capable of proving both general and system-specific properties through the use of complex, user-defined analysis algorithms. Second, the language is suitable for specification of the desired behavior of concurrent systems. The techniques for automatic instantiation of Petri nets as concurrent systems are reviewed. The details of a newly implemented translator are given, extending the previous work in several ways: timed Petri nets, concurrent transition firings, and predicates and actions are supported. In addition, a method of instantiating Contour/Transition-nets is proposed. As a demonstration of feasibility, the Transmission Control Protocol is modeled and analyzed using the proposed tools and techniques. The utility of state space analysis for both model debugging and discovery of specification errors is shown. Finally, the contributions made in this dissertation are summarized and areas for future research are listed.