Cooperating Formal Methods Final Report.

Abstract

Formal methods research has developed a variety of mathematical tools and techniques applicable to the development of software systems, but they are greatly underused. The reasons include the limited mathematical backgrounds of many end-users and developers; idiosyncratic support tools; lack of attention to technology transfer. We have developed a prototype formal methods interface (PMI) that permits different kinds of users, with different degrees of expertise, to cooperate in applying formal methods to define, explore, and analyze system designs and specifications. Systems are specified in RSML, a mixed graphical and textual notation for defining state machines. The FMI allows a user to perform automated analysis of certain semantic questions about an RSML specification -- e.g., the question of whether the specified state machine can respond to every input. It does so by generating a representation of each question within the formalism of various formal analysis tools. The FMI can easily be linked to a variety of formal tools, as we have shown by rapidly incorporating the EVES and PVS theorem provers, and the SPIN model checker.

Open PDF

Document Details

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

Entities

People

  • David Guaspari

Tags

Communities of Interest

  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Models
  • Notation
  • Prototypes
  • Specifications
  • Technology Transfer

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.