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.