This Article 
 Bibliographic References 
 Add to: 
Foundations of the Trace Assertion Method of Module Interface Specification
July 2001 (vol. 27 no. 7)
pp. 577-598

Abstract—The trace assertion method is a formal state machine based method for specifying module interfaces. 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 module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of nondeterminism, normal and exceptional behavior, value functions, and multiobject modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted.

[1] J.-R. Abrial, "Assigning Programs to Meanings," Mathematical Logic and Programming Languages, Philosophical Trans. Royal Society, series A, vol. 312, 1984.
[2] A. Arnold, Finite Transition Systems. Prentice Hall, 1994.
[3] W. Bartoussek and D. L. Parnas, “Using Assertions about Traces to Write Abstract Specifications for Software Modules,” Proc. Second Conf. European Cooperation in Informatics and Information Systems Methodology, pp. 211-236, 1978.
[4] P.M. Cohen, Universal Algebra. D. Reidel, ed., 1981.
[5] F. Courtois and D.L. Parnas, “Formally Specifying a Communication Protocol Using the Trace Assertion Method,” Technical Report CRL Report No. 269, McMaster Univ., Hamilton, Ontario, Canada, 1993.
[6] The Book of Traces. V. Diekert and G. Rozenberg, eds., World Scientific Publishing, 1995.
[7] M. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1. Berlin: Springer-Verlag, 1985.
[8] S. Eilenberg, Automata, Languages, and Machines, vol. A.Academic Press, 1974.
[9] R. Fraisse, Theory of Relations. North Holland, 1986.
[10] J. He, C.A.R. Hoare, and J.W. Sanders, "Data Refinement Refined," Lecture Notes in Computer Science 213, B. Robinet and R. Wilhelm, eds., pp. 187-196, Springer-Verlag.
[11] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, "Automated Consistency Checking of Requirements Specifications," ACM Trans. Software Eng. and Methodology, pp. 231-261, vol. 5, July 1996.
[12] D.M. Hoffman, “The Trace Specification of Communication Protocols,” IEEE Trans. Computers, vol. 34, no. 12, pp. 1102–1113, Dec. 1985.
[13] J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Apr. 1979.
[14] M. Iglewski, M. Kubica, and J. Madey, “Trace Specification of Nondeterministic Multiobject Modules,” Technical Report 95-05(205), Inst. of Informatics, Warsaw Univ., Warsaw, Poland, 1995.
[15] M. Iglewski, J. Madey, and K. Stencel, “On Fundamentals of the Trace Assertion Method,” Technical Report RR 94/09-6, Univ. du QuébecàHull, Hull, Canada, 1994.
[16] M. Iglewski, J. Mincer-Daszkiewicz, and J. Stencel, “Some Experiences with Specification of Nondeterministic Modules,” Technical Report RR 94/09-7, Univ. du QuébecàHull, Hull, Canada, 1994.
[17] R. Janicki, "Towards a Formal Semantics of Parnas Tables," Proc. 17th Int'l Conf. Software Eng., ICSE, pp. 231-240, Apr. 1995.
[18] R. Janicki and M. Koutny, “Structure of Concurrency,” Theoretical Computer Science, vol. 112, no. 1, pp. 5–52, 1993.
[19] R. Janicki, D.L. Parnas, and J. Zucker, "Tabular Representations in Relational Documents," Brink et al. [6], ch. 12, pp. 184-196.
[20] N. Lynch and M. Tuttle, “An Introduction to Input/Output Automata,” CWI Quarterly, vol. 2, no. 3, pp. 219–246, 1989.
[21] N. Lynch and F. Vaandrager, “Forward and Backward Simulations: I. Untimed Systems,” Information and Computation, vol. 121, no. 2, pp. 214–233, 1995.
[22] J. McLean, “A Formal Foundations for the Abstract Specification of Software,” J. ACM, vol. 31, no. 3, pp. 600–627, 1984.
[23] H.D. Mills, “Stepwise Refinement and Verification in Box-Structured Systems,” Computer, vol. 21, no. 6, pp. 23-26, June 1988.
[24] T. Norvell, “On Trace Specifications,” CRL Report 305, McMaster Univ., Hamilton, Canada 1995.
[25] D. L. Parnas, "A Technique for Software Module Specification with Examples," Comm. ACM, vol. 15, p. 330, May 1972.
[26] D.L. Parnas, J. Madey, and M. Iglewski, "Precise Documentation of Well-Structured Programs," IEEE Trans. Software Eng., vol. 20, no. 12, pp. 948-976, Dec. 1994.
[27] D. Parnas and Y. Wang, “The Trace Assertion Method of Module Interface Specification,” Technical Report 89–261, CIS, Queen's Univ., 1989.
[28] S.J. Prowell, “Sequence-Based Software Specification,” PhD Thesis, Univ. of Tennessee, 1996.
[29] G. Rozenberg and R. Varraedt, “Subset Languages of Petri Nets,” Theoretical Computer Science, vol. 26, pp. 301–323, 1983.
[30] G. Schmidt and T. Ströhlein, Relations and Graphs, Monographs on Theoretical Computer Science. Berlin: Springer-Verlag, 1993.
[31] A.J. van Schouwen, “The A-7 Requirements Model: Re-Examination for Real Time Systems and an Application to Monitoring Systems,” Technical Report 90–276, Queen's Univ., 1990.
[32] A.J. van Schouwen, “On the Road to Practical Module Interface Specification,” Proc. Workshop Tools for Tabular Notations, 1996.
[33] Y. Wang, "Specifying and Simulating the Externally Observable Behavior of Modules," PhD thesis, Dept. of Computing and Information Science, Queen's Univ., Kingston, Ontario, Canada, 1994.
[34] M. Wirsing, “Algebraic Specification,” Handbook of Theoretical Computer Science, vol. B, pp. 675-788, Amsterdam: North Holland, 1990.

Index Terms:
Module interface specifications, trace assertion method, state machines, Mealy machines, step-sequences, relational model, nondeterminism, module refinement, tabular notation.
Ryszard Janicki, Emil Sekerinski, "Foundations of the Trace Assertion Method of Module Interface Specification," IEEE Transactions on Software Engineering, vol. 27, no. 7, pp. 577-598, July 2001, doi:10.1109/32.935852
Usage of this product signifies your acceptance of the Terms of Use.