ASE2 CARD CATALOG ENTRY

Instructions:

• Scroll forward and backward through this Card Catalog Entry to view it.
• Strike the PRINT button on your browser to print this Card Catalog Entry.
• Go to the FILE SPECS section of this Card Catalog Entry to find out where the associated directories and files are. If they are on this Website, you can transfer to them by clicking on the indicated hyperlinks. Note: the FILE SPECS hyperlink in this bullet will take you directly to the FILE SPECS section.
• Use the FIND command of your browser to search this Card Catalog Entry.
• Click here to go to the Card Catalog Taxonomy.
• Click here to go to the Card Catalog Index. Warning: the index file is large, so this may take a while on slower systems.
• Click here to go to the Title Page.

---

ASSET OVERVIEW

UNIT NAME

SEEMETH

VERSION

N/A

ORIGIN

ASSET

REVIEW CODE

OK

INET ADDRESS

librarian@source.asset.com

AUTHOR

Paramax

RIGHTS

Approved for public release; distribution unlimited

COPYRIGHT

1992 Paramax

LOCATION

ASSET
PAL

---

CLASSIFICATION

KEYWORDS

Software Development Process
Process, Software Development
SW Engineering Environment
Environment, SW Engineering
SEE
Formal Methods
Methods, Formal

INDEX

Paramax

DEPENDENCIES

None

SEE ALSO

SHORT DESCRIPTION

Ways in which tools supporting formal methods may merge with the STARS SEE

TAXONOMY

Documents

Ada Formal Methods in the STARS SEE

---

FILE LISTING

FILE SPECS

Click here to enter Asset Directory/transfer Asset File(s): ../../ase02_01/docs/see/seemeth

DIRECTORY DISPLAY

Follow path to see directory

---

ABSTRACT

Ada Formal Methods in the STARS Environment

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.

---

REVISION HISTORY

03 June 1992      Paramax    Initial release to ASSET
20 December 1993  ASSET      Initial release to the PAL

---

RELEASE NOTICE

Approved for public release; distribution unlimited

---

DISCLAIMER

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.

---

ASE CARD CATALOG ENTRY NAVIGATION

• Go to Title Page
• Go to Taxonomy
• Go to Index (warning: the index file is large, so this may take a while on slower systems)
• Go to Top of this Page

Powered by the Generic Web-Based Reuse Library (GWRL)