Accession Number : ADA313996

Title :   Cooperating Formal Methods Prototype Code.

Descriptive Note : Final rept. 18 Oct 95-12 Apr 96,

Corporate Author : ODYSSEY RESEARCH ASSOCIATES INC ITHACA NY

Personal Author(s) : Guaspari, David

PDF Url : ADA313996

Report Date : 12 APR 1996

Pagination or Media Count : 247

Abstract : The prototype formal methods interface (FMI) can easily be linked to a variety of formal tools. This is achieved by representing the underlying specification language (RSML) in an attribute grammar and predefining a rich set of attributes that capture RSML semantics. A developer wishing to model aspects of RSML within a formal tool can access these predefined attributes directly, and may also add an arbitrary collection of new attributes. Editable WEB-style templates simplify this task. This attachment demonstrates the usefulness of our techniques by showing how the EVES and PVS theorem provers and the SPIN model checker were rapidly linked to the FMI.

Descriptors :   *COMPUTER PROGRAMS, *PROGRAMMING LANGUAGES, *PROTOTYPES, GLOBAL, MODELS, SPECIFICATIONS, SEMANTICS, CODING, DATA ACQUISITION, COMPUTER FILES, PARSERS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE