Simulating reactive systems by deduction

Abstract
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.

This publication has 11 references indexed in Scilit: