Simulating Reactive Systems by Deduction
Yishai A. Feldman and Haim Schneider
Dept. of Computer Science
Tel Aviv University
69978 Tel Aviv, Israel
Appeared in: ACM Trans. Software Engineering and Methodology,
vol. 2, no. 2, April 1993
Debugging is one of the main uses of simulation. Localizing bugs or finding the reasons
for unclear behavior involves going backwards in time, whereas simulation goes forward in
time. Therefore, identifying causes with the aid of most existing simulation tools usually
requires repeating the simulation several times, each time with reduced holes in the
sieve. An alternative is simulation by deduction, a technique in which the steps in the
dynamic behavior of the simulated model are deduced by a reasoning system. A simulation
system that uses simulation by deduction can give direct answers to questions about the
reasons for the simulation results. By recording the support for its deductions, such a
system can answer "why" and "why not" questions about the scenario.
Another benefit of simulation by deduction is that it enables symbolic simulation, that
is, simulating a scenario given only a partial description of the environment and the
simulated model. This allows verifying properties of an evolving design at any stage of
the design process, and thus checking the consequences of the design decisions made so
far. In order to allow deducing as much as possible from partial information, the axiom
system has to be minimalistic, i.e., axioms have to require the minimum amount of
knowledge of simulation inputs.
These ideas were implemented in a system called SIP, which simulates the behavior of
reactive systems. SIP is capable of answering "why", "why not", and
"what if" questions. It also has a limited capability of dealing with partial
knowledge. SIP is based on a reasoning system that is responsible for deducing the effects
of the external inputs on the state of the simulated model, and recording the support for
its deductions. The logical basis for the deduction of a step in SIP is provided by a
minimalistic axiom system for statecharts.
Although SIP simulates reactive systems described as statecharts, the principle of
simulation by deduction is applicable to other types of systems and descriptions, provided
only that they have a well-defined formal semantics.