In this thesis, we develop a formal and abstract method for 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 in order to

improve their readability. A rigid structure is introduced into trace specifications to ensure

that a user can find relevant information quickly, i.e., without searching through the whole


     Also developed in this thesis 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.