MODULAR VERIFICATION OF ASYNCHRONOUS SYSTEMS.

Title: MODULAR VERIFICATION OF ASYNCHRONOUS SYSTEMS.
Identifier: AAI8319787
identifier: 8319787
Creator: NEMES, RICHARD MICHAEL.
Contributor: E. A. Akkoyunlu | M. Anshel
Date: 1983
Language: English
Publisher: City University of New York.
Subject: Computer Science
Abstract: The semantics of communication are investigated from the viewpoint of modularity and hierarchical program development. Communicating Sequential Processes (CSP), Hoare's language for parallel programming, is modified and expanded to support process modularity and hierarchical structure using a Port construction. A formal axiomatic verification methodology is developed along the lines of Hoare's axiomatic proof system for sequential programs, extending his system to include CSP-like parallel programs without resort to global invariants. Hierarchical structure and modularity are fully supported within the proof system. Processes are verified against an abstract entity, the interface, thereby achieving a formal notion of process specification and plug-compatibility. Formal Port semantics are further broadened and extended to include a generalization of the simple Port, termed multi-Port, based on a universal assertion, Kirchoff's Law. As an application of the methodology, a modular proof of the generic single-entry, multiple-user CSP subroutine process is provided.
Type: dissertation
Source: PQT Legacy CUNY.xlsx
degree: Ph.D.
Program: Engineering