Accession Number : ADA310056

Title :   Formal Methods for Dependable Distributed Software.

Descriptive Note : Final rept. 1 Oct 92-30 May 96,

Corporate Author : MISSOURI UNIV-ROLLA

Personal Author(s) : McMillin, Bruce

PDF Url : ADA310056

Report Date : MAY 1996

Pagination or Media Count : 13

Abstract : This work has developed a powerful concept in evaluating formal specifications concurrently with distributed program execution for the purposes of error detection, fault tolerance, and security. This concept is realized in the CCSP evaluation system for axiomatic proofs, for interval temporal formulae, and for a security calculus. We have validated this concept through nontrivial examples of distributed programs including a dynamic group membership protocol, a distributed database scheduler, of a responsive system modeling railroad trains on intersecting tracks, and of a secure warehouse management system. Temporal subsumption has been developed as a way of making these programs efficient. Moreover, the spinoff technologies from this work, in of themselves have become useful. CCSP can also be used as a debugging tool for distributed programs. Temporal Subsumption functions as a quick and powerful proof checker for Hoare triples. Both of these achievements may help to bring more use of formal methods into the mainstream.

Descriptors :   *SOFTWARE ENGINEERING, *METHODOLOGY, *DEBUGGING(COMPUTERS), *COMPUTER PROGRAM RELIABILITY, COMPUTER PROGRAMS, RAILROADS, MANAGEMENT PLANNING AND CONTROL, DETECTION, DISTRIBUTED DATA PROCESSING, MODELS, SPECIFICATIONS, DYNAMICS, SECURITY, ERRORS, CALCULUS, FAULT TOLERANCE, WAREHOUSES.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE