Software Tools for Formal Specification and Verification of Distributed Real-Time Systems.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 30, 1997
- Accession Number
- ADA330059