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.