Accession Number : ADA307890

Title :   An Architectural Description of the Simplex Architecture.

Descriptive Note : Final rept.,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST

Personal Author(s) : Rivera, Jose G. ; Danylyszyn, Alejandro A. ; Weinstock, Charles B. ; Sha, Lui R. ; Gagliardi, Michael J.

PDF Url : ADA307890

Report Date : MAR 1996

Pagination or Media Count : 76

Abstract : Simplex is a software architecture for dependable and evolvable process-control systems developed by the Software Engineering Institute. Our project consisted of creating a formal specification of this architecture, and analyzing its safety and liveness properties. We developed a Communicating Sequential Processes (CSP) model to describe the overall dynamic behavior of the Simplex architecture, which we verified using the Failure-Divergence-Refinement (FDR) model checker. As a result, we discovered interesting things about the use of FDR that revealed subtle points in the Simplex architecture. We also developed a WRIGHT specification of this architecture to characterize precisely the connections between its components at the architectural level, The specification was based on the latest version of the CSP model.

Descriptors :   *SOFTWARE ENGINEERING, *COMPUTER ARCHITECTURE, SPECIFICATIONS, DYNAMIC RESPONSE, SEQUENCES.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE