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.

REFERENCES

• 1: Hiralal Agrawal , Joseph R. Horgan, Dynamic program slicing, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.246-256, June 1990, White Plains, New York, United States
• 2: ~BALZER, R.M. EXDAMS--EXtendable Debugging and Monitoring System. In Proceedzngs ~of the AFIPS 1969 Sprint Joint Computer Conference (Boston, Mass., May 1969) vol. 34, ~AFIPS Press, pp. 567-580, 1969.
• 3: ~CARVER, R., AND TAi, K. Reproducible testing of concurrent programs based on shared ~variables. In Proceedings of the Szxth International Conference on Distributed Computer ~Systems (Cambridge, Mass., 1986), pp. 428-433.
• 4: Jong-Deok Choi , Barton P. Miller , Robert H. B. Netzer, Techniques for debugging parallel programs with flowback analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.491-530, Oct. 1991 [doi>10.1145/115372.115324]
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: ~FELDMAN, Y. A. Knowledge-based editing of reactive systems: A scenario. Tech. Rep. ~CS90-15, Dept. of Applied Mathematics and Computer Science, The Weizmann Institute of ~Science. 1990.
• 7: ~FELDMAN, Y. A., AND R~CU, C. Principles of knowledge representation and reasoning in the ~FRAPPE system. In Proceedings of the 6th Israeh Symposium on Artificial Intelligence (Tel ~Aviv, Israel, Dec. 1989), pp. 133-148.
• 8: Yishai A. Feldman , Charles Rich, Pattern-directed invocation with changing equations, Journal of Automated Reasoning, v.7 n.3, p.403-433, Sept. 1991 [doi>10.1007/BF00249022]
• 9: ~FELDMAN, Y. A., AND SCHNEIDER, H. Simulating the behaviour of reactive systems by a ~deduction system. Tech. Rep. 201/91, Tel Aviv Univ,, March 1991.
• 10: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9 ]
• 11: David Harel , Amir Pnueli , Hagi Lachover , Amnon Naamad , Michal Politi , Rivi Sherman , Aharon Shtull-Trauring , Mark Trakhtenbrot, STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.403-414, April 1990 [doi>10.1109/32.54292 ]
• 12: D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 13: ~HAREL, D., PNUELI, A., SCHMIDT, J. P., AND SHERMAN, R. On the formal semantics of ~statecharts. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science ~(1987), pp. 54-64.
• 14: ~HUIZING, C., GERTH, R., AND DE ROEVER, W.P. A compositional semantics for statecharts. ~Technical report, Eindhoven Univ. of Technology, 1987.
• 15: Ron I. Kuper, Dependency-Directed Localization of Software Bugs, Massachusetts Institute of Technology, Cambridge, MA, 1989
• 16: T. J. LeBlanc , J. M. Mellor-Crummey, Debugging parallel programs with instant replay, IEEE Transactions on Computers, v.36 n.4, p.471-482, April 1987 [doi>10.1109/TC.1987.1676929]
• 17: ~i-Logix. The semantics of statecharts. Tech. Rep. i-Logix, Inc., Burlington, MA, 1989.
• 18: Charles E. McDowell , David P. Helmbold, Debugging concurrent programs, ACM Computing Surveys (CSUR), v.21 n.4, p.593-622, Dec. 1989 [doi>10.1145/76894.76897]
• 19: ~MILLER, B., AND LEBLANC, T. J., Eds. Proceedings of the ACM SIGPLAN/SIGOPS Work- ~shop on Parallel and Dzstributed Debugging (Madison, Wise., May 1988). SIGPLAN Notices ~24, I (1989).
• 20: ~PNUELI, A., AND SHALEV, M. What is in a step? In J. W. De Bakker, 25 Jaar Semantlek. ~CWI, 1989, 373-399.
• 21: ~RIcI4, C. Knowledge representation languages and predicate calculus: How to have your ~cake and eat i~ too. In Proceedings of the 2nd National Conference on Artiflctal lntelhgence ~(Pittsburgh, PA, Aug. 1982), pp. 193-196.
• 22: Charles Rich , Yishai A. Feldman, Seven Layers of Knowledge Representation and Reasoning in Support of Software Development, IEEE Transactions on Software Engineering, v.18 n.6, p.451-469, June 1992 [doi>10.1109/32.142869 ]
• 23: Charles Rich , Richard C. Waters, The programmer's apprentice, ACM Press, New York, NY, 1990
• 24: Richard C. Waters, The programmer's apprentice: a session with KBEmacs, IEEE Transactions on Software Engineering, v.11 n.11, p.1296-1320, Nov. 1985 [doi>10.1109/TSE.1985.231880]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based)

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.7 Simulation Support Systems
          Subjects: Environments

  J. Computer Applications

General Terms:
Design, Theory