User-Interface for Rule-Based Formal-Methods

This project aims towards an initial "Formal Methods Inter-face,, frame- work which will provide interface in three senses: * between the engineer and formal methods tools; * to support interworking of diverse tools which implement a ide range of formal approaches; * between the formal tools and conventional computer-aided software engineering (CASE) environments. In order to keep the scope of the project within the scale of an SBIR development, we concentrate on a particular class of applications, those real- izable by rule-basedstate/input/output transition schemes, to yield a tool "Proof and Refinement in State Machines" WiSM). Nevertheless, future exten- sibility to further domains will be a major influence on the architectural de- sign. Phase I has four main goals: to survey candidate systems from which to capture data, so as to identify the types of system description and properties that the framework should manage; to establish the theoretical and practical foundations for combining the use of existing model-checking and theorem- proving tools and CASE environments; to formulate a high-level design of PRiSM in terms of the abstract objects it manipulates, and the operations it applies to those objects; and to prepare a demonstration and argument of the projects feasibility, via story-boarding.