PAL CARD CATALOG ENTRY

SHORT DESCRIPTION

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


MOVEMENT WITHIN THE PAL CARD CATALOG
Move to top-level taxonomy
Move to keyword list

ASSET PROFILE

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

FILE LISTING

Directory Display


languages/ada/docs/seemeth:
  File Name                 Size
  ---------                 ----
  README                     914
  seemeth.zip            189,640


Totals
  ==============  ==============
    2 Files              190,554

ABSTRACT

ASSET_A_256:  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.