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