Accession Number : ADA330059

Title :   Software Tools for Formal Specification and Verification of Distributed Real-Time Systems.

Descriptive Note : Final rept.

Corporate Author : COMPUTER COMMAND AND CONTROL CO PHILADELPHIA PA

PDF Url : ADA330059

Report Date : 30 SEP 1997

Pagination or Media Count : 25

Abstract : This is the final report prepared under SBIR Phase II Contract N00014-95-C-0131 from the Office of Naval Research. It reports on the development of a set of software tools for specification and verification of distributed real time systems using formal methods. The task of this SBIR Phase II effort was to create a commercial-strength CASE toolset suitable for handling real-life verification problems. A preceding Phase I contract was concerned with development of the approach to the problem and design of a prototype environment 14. Forthcoming Phase III work will demonstrate the utility of the toolset to potential customers and establish it as a commercial off- the-shelf (COTS) specification and verification product. It is important to note that commercialization work, which is the task of Phase III efforts, has already begun during the current Phase II period (see Section IV). The toolset has been given the name PARAGON, which stands for 'Process-Algebraic Real-time Analysis with Graphics-Oriented Notation'. The toolset is indented to be used by designers of real-time systems for early detection of errors. The mathematical complexity of formal specification and verification has been hidden from the end users as much as possible. To achieve this, the specification language uses notions used by designers in their work as primitives. This provides for concise specifications, readable even by a non-specialist.

Descriptors :   *COMPUTER PROGRAMS, *SOFTWARE ENGINEERING, *TOOLS, MATHEMATICAL MODELS, VERIFICATION, REAL TIME, SPECIFICATIONS, COMPUTER PROGRAM VERIFICATION.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE