Foundations of the Trace Assertion Method of Module Interface Specification

Dr. Ryszard Janicki

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


The trace assertion method is a formal state machine based method for specifying module interfaces ([3, 15, 25, 28, 32, 36]). 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. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The role of non-determinism, normal and exceptional behaviour, value functions and multi-object modules are discussed. The relationship with the Algebraic Specification ([9, 37]) is analyzed.