Accession Number : ADA313995

Title :   Cooperating Formal Methods Final Report.

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 : ADA313995

Report Date : 12 APR 1996

Pagination or Media Count : 49

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.

Descriptors :   *SOFTWARE ENGINEERING, *MATHEMATICAL PROGRAMMING, MATHEMATICAL MODELS, AUTOMATION, TECHNOLOGY TRANSFER, TOOLS, REPORTS, COMPUTER GRAPHICS, MACHINES.

Subject Categories : Numerical Mathematics
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE