You are here

Using Formal Reasoning to Augment Commercial Reactive System Design Tools

Award Information
Agency: Department of Defense
Branch: Navy
Contract: N/A
Agency Tracking Number: 28524
Amount: $59,776.00
Phase: Phase I
Program: SBIR
Solicitation Topic Code: N/A
Solicitation Number: N/A
Solicitation Year: N/A
Award Year: 1995
Award Start Date (Proposal Award Date): N/A
Award End Date (Contract End Date): N/A
Small Business Information
1717 W. Sixth St., Suite 290
Austin, TX 78703
United States
HUBZone Owned: No
Woman Owned: No
Socially and Economically Disadvantaged: No
Principal Investigator
 Michael K. Smith
 (512) 322-9951
Business Contact
Phone: () -
Research Institution

Commercial tools have been developed that support the graphical construction of behavioral models of reactive systems and implement various forms of analysis of such user-developed models. These methods rely primarily on simulation, that is, the execution of a model on sample data. We propose to take advantage of the extensive effort that has gone into making the graphical user interfaces of these commerical systems appealing to software engineers. We will use formal reasoning techniques to augment simulation in the analysis of system models obtained via these interfaces. Formal reasoning can be used to answer questions that are difficult or impossible to answer via simulation. Some of these questions can be formulated so that they can be answered with a minimum of user involvement, e.g. using ordered binary decision diagrams (BDDs) and derivative techniques, notably model checking. More general theorem proving techniques can prove properties that cannot be proved using BDDs and, in addition, support the evolution of a series of increasingly advanced tools.

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government