Trace Rewriting Systems

Mr. Yabo Wang

Dr. David Lorge Parnas

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1


Software modules, just as other engineering products, should have precise specifications, i.e., precise descriptions of their externally observable behaviour. To abstractly specify the requirements on each module's interface, we view modules as "black-boxes" and specify them by a finite state machine based module interface specification method - the trace assertion method.

To support this method, we plan to develop a simulation tool, trace simulator, that symbolically interprets trace assertions of trace specifications and simulates the externally observable behaviour of the modules specified.

In this report, we first describe the trace assertion method. We then present a theoretical model for the trace simulator - trace rewriting (a form of term rewriting), and study the properties of trace rewriting systems. We show that a proper trace rewriting system is both terminating and confluent and offer some comparisons between trace rewriting systems and general term rewriting systems.