Specifying and Simulating the Externally Observable Behaviour of Modules

Dr. Yabo Wang

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


We develop a formal and abstract method of specifying module interfaces, the Trace Assertion Method. We present the underlying theory of this method and illustrate how it can be applied to specify various types of software modules and device interface modules. We define a tabular notation for writing trace specifications to ensure that a user can find relevant information quickly, i.e., without searching through the whole document.

Also developed in this report is a theory of Trace Rewriting Systems, an extension to the theory of the traditional term rewriting systems. We show that, for the purpose of simulating module interfaces, the trace rewriting provides an adequate operational semantics for trace specifications.

Based on the trace rewriting system theory, we design a software tool called Trace Simulator. The tool can be used to simulate the externally observable behaviour of modules by interpreting their trace specifications. Various techniques, such as, reusing the values of evaluated predicates, converting costly string comparisons to integer operations, adopting Knuth-Morris-Pratt string pattern matching algorithm, etc., are integrated into the design to ensure that the Trace Simulator is a practical tool.