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


Abstract

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.