Using Formal Reasoning to Augment Commercial Reactive System Design Tools

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.