Specification and Verification of Secure Concurrent and Distributed Software Systems
Final technical rept. Jul 1988-Dec 1989
CALIFORNIA UNIV DAVIS DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
This report describes an investigation of techniques to support the specification and verification of concurrent and distributed software systems, with special emphasis on issues of security. The investigation has focused on two major areas. The primary focus is a survey of existing methodologies and systems that are relevant to the specification and verification of concurrency. The secondary focus is on the initial design of a short-term workbench that embodies capabilities of existing systems together with new features that extend the current state of the art in the specification and verification of concurrency. The introduction to the report summarizes survey results and presents overall conclusions about the current state of the art. Sections 2 and 3 of the report present the details of the methodology and system surveys respectively. The surveys include high level feature comparison tables accompanied by extended reviews. Section 4 describes a design for the short-term workbench that will support computer-aided specification and verification. Section 5 describes a set of extended examples that were developed to test the design ideas. Section 6 concludes with an overall summary and an overview of targets for future work.
- Computer Programming and Software
- Computer Systems Management and Standards