This Article 
 Bibliographic References 
 Add to: 
Simulating the Behavior of Software Modules by Trace Rewriting
October 1994 (vol. 20 no. 10)
pp. 750-759

The trace assertion method is a module interface specification method based on the finite state machine model. To support this method, we plan to develop a specification simulation tool, a trace simulator, that symbolically interprets trace assertions of trace specifications and simulates the externally observable behavior of the modules specified. We first present the trace assertion method. Then we formally define trace rewriting systems and show how trace rewriting, a technique similar to term rewriting, can be applied to implement trace simulation.

[1] A. Avenhaus and K. Madlener, "Term rewriting and equational reason," in R. B. Banerji, Ed.,Formal Techniques in Artificial Intelligence, Amsterdam, Netherlands: Elsevier (North-Holland), 1990, pp. 1-43.
[2] W. Bartussek and D. L. Parnas, "Using traces to write abstract specifications for software modules,"Inform. Syst. Methodology, inLecture Notes in Computer Science 65, pp. 211-236, 1978.
[3] R. V. Book, "True systems as rewriting systems,"J. Symbolic Computation, vol. 3, pp. 39-68, 1987.
[4] N. Dershowitz, "Termination of rewriting,"J. Symbolic Computation, vol. 3, pp. 69-116, 1987.
[5] N. Dershowitz and J.-P. Jouannaud, "Rewriting systems," in J. van Leeuwen, Ed.,Handhook of Theoretical Computer Science, Amsterdam, Netherlands: Elsevier, 1990, pp. 243-320.
[6] E. W. Dijkstra, "Notes on structured programming," in O.-J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, Eds.,Structured Programming, New York: Academic, 1972.
[7] K. Futatsugi, J. Goguen, J.-P. Jouannaud, and J. Meseguer, "Principles of OB J2," inProc. Twelfth Symp. Principles of Programming Languages, ACM, 1985, pp. 52-66.
[8] S. J. Garland and J. V. Guttag, "An overview of LP, the Larch Prover," inProc. Third Int. Conf. Rewriting Techniques and Applications(Lecture Notes in Computer Science, vol. 355), Chapel Hill, NC. New York: Springer-Verlag, 1989, pp. 137-151.
[9] J. A. Goguen, J. W. Thatcher, and E. Wagner, "An initial algebra approach to the specification and implementation of abstract data types," in R. T. Yeh, Ed.,Current Trends in Programming Methodology, vol. IV, Englewood Cliffs, NJ: Prentice-Hall, 1978, pp. 80-184.
[10] J. Guttag and J. J. Horning, "The algebraic specification of abstract data types,"Acta Informaticavol. 10, pp. 27-52, 1978.
[11] D. Hoffman, "The specification of communication protocols,"IEEE Trans. Comput., vol. C-34, no. 12, pp. 1102-1113, Dec. 1985.
[12] G. Hue and D. C. Oppen, "Equations and rewrite rules: A survey," in R. Book, Ed.,Formal Language Theory: Perspectives and Open Problems, New York: Academic Press, 1980, pp. 349-405.
[13] J. W. Klop, "Term rewriting systems," in S. Abramsky, D. Gabby, and T. Maibaum, Eds.,Handbook of Logic in Computer Science, ch. 6. New York: Oxford University Press, 1992.
[14] D. R. Musser, "Abstract data type specification in the AFFIRM system,"IEEE Trans. Software Eng., vol. SE-6, no. 1, pp. 24-32, Jan. 1980.
[15] D. L. Parnas, "Information distributions aspects of design methodology,"Prof. IFIP Congress 1971, 1972, pp. 26-30.
[16] D. L. Parnas and Y. Wang, "The trace assertion method of module interface specification," Tech. Rep. 89-261, Telecommun. Res. Inst. of Ont. (TRIO), Queen's University,--city--, ON, Canada, 1989.
[17] L. Robinson and O. Roubine, "SPECIAL: A specification and assertion language," Tech. Rep. CSL-46, Comput. Sci. Lab., Stanford Res. Inst., Stanford, CA, USA, 1977.
[18] Y. Toyama, "Confluent term rewriting systems with membership conditions," inConditional Terms Rewriting Systems, inLecture Notes on Computer Science 308, pp. 229-241, 1987.
[19] I. van Horebeek, J. Lewi, and E. Bevers, "An exception handling method for constructive algebraic specifications,"Software Practice and Experience, vol. 18, pp. 443-438, May 1988.
[20] Y. Wang and D.L. Parnas, "Trace rewriting systems," inConditional Term Rewriting Systems, in M. Rusinowitch and J. L. Remy, Eds.,Lecture Notes in Computer Science 656, pp. 343-356, 1993.

Index Terms:
finite state machines; rewriting systems; formal specification; simulation; digital simulation; software module behavior simulation; trace rewriting; trace assertion method; module interface specification method; finite state machine model; specification simulation tool; trace simulator; trace specifications; trace rewriting systems; term rewriting; trace simulation
Yabo Wang, D.L. Parnas, "Simulating the Behavior of Software Modules by Trace Rewriting," IEEE Transactions on Software Engineering, vol. 20, no. 10, pp. 750-759, Oct. 1994, doi:10.1109/32.328996
Usage of this product signifies your acceptance of the Terms of Use.