The Trace Assertion Method of Module Interface Specification with Concurrency
Ms. Yan Liu
The trace assertion method is a formal state machine based method for
specifying module interfaces [2, 10, 23, 27, 31, 35]. A module interface
specification treats the module as a black-box, identifying all module's
access programs (i.e., programs that can be invoked from outside of the
module), and describing their externally visible effects. In the method,
both the system states and the behaviours observed are fully described by
traces built from access program invocations and their visible effects. So
far the method has only been applied to the sequential accesses to modules,
i.e. there is an assumption that no two events can occur simultaneously.
This paper improves the existing method and presents the trace assertion
method of module interface specification with concurrent events. The
foundations and specification formats of Concurrent Trace Assertion Method
is developed for deterministic, non-deterministic, output dependent and
output independent modules.