Cooperating Formal Methods Prototype Code.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 12, 1996
Accession Number
ADA313996

Entities

People

  • David Guaspari

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Attachment
  • Coding
  • Computer Programming
  • Grammars
  • Hash Tables
  • Hierarchies
  • Language
  • Models
  • Numbers
  • Prototypes
  • Semantics
  • Separators
  • Side Effects
  • Specifications
  • Standards
  • Template Patterns
  • Translations

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.
  • Organizational Process Management (OPM).