ASE2 CARD CATALOG ENTRY
This report is a collection of several possible ways in which tools supporting formal methods might be made interoperable and/or integrated into the STARS SEE. The possibilities discussed are merely representative, and are limited only by the effort available for completing the report. In general, formal methods might be applied to any phase of system development, including requirements analysis, design, implementation of both hardware and software, testing, and so forth. However, this report is restricted for the most part to formal code verification of Ada. (The single exception to this restriction is the discussion of run-time checking in Anna.) Formal code verification is proof that an algorithm implemented by a piece of code meets a formally stated specification. ORA's Penelope and Ariel tools support code verification.
03 June 1992 Paramax Initial release to ASSET 20 December 1993 ASSET Initial release to the PAL
Approved for public release; distribution unlimited
This documentation is provided "AS IS" and without any expressed or implied warranties whatsoever. No warranties as to performance, merchantability, or fitness for a particular purpose exist. The user must assume the entire risk and liability of using this document. In no event shall any person or organization of people be held responsible for any direct, indirect, consequential or inconsequential damages or lost profits.
Powered by the Generic Web-Based Reuse Library (GWRL)