This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Theory of Interfaces and Modules - I: Composition Theorem
January 1994 (vol. 20 no. 1)
pp. 55-71

We model a system as a directed acyclic graph where nodes represent modules and arcs represent interfaces. At the heart of our theory is a definition of what it means for a module to satisfy a set of interfaces as a service provider for some and as a service consumer for others. Our definition of interface satisfaction is designed to be separable; i.e., interfaces encode adequate information such that each module in a system can be designed and verified separately, and composable; i.e., we have proved a composition theorem for the system model in general.

[1] M. Abadi and L. Lamport, "Composing specifications," inProc. REX Workshop on Stepwise Refinement of Distributed Systems, Lect. Notes in Comput. Sci., J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds., vol. 430, 1990, pp. 1-41. Springer-Verlag.
[2] T. Bolognesi and E. Brinksma, "Introduction to the ISO Specification language LOTOS,"Computer Networks ISDN Syst., vol. 14, pp. 25- 59, 1987.
[3] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe, "A theory of communicating sequential processes,"J. ACM, vol. 31, no. 3, pp. 560-599, July 1984.
[4] E. W. Dijkstra, "Hierarchical ordering of sequential processes,"Acta Informatica, vol. 1, pp. 115-138, 1971.
[5] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[6] A. Kay and J. N. Reed, "A rely and guarantee method for timed CSP: A specification and design of a telephone exchange,"IEEE Trans. Software Eng., vol. 19, no. 6, pp. 625-639, June 1993.
[7] S. S. Lam and A. U. Shankar, "Protocol verification via projections,"IEEE Trans. Software Eng., vol. SE-10, no. 10, pp. 325-342, July 1984.
[8] S. S. Lam and A. U. Shankar, "Specifying modules to satisfy interfaces: A state transition system approach,"Distributed Comput., vol. 6, pp. 39-63, 1992.
[9] S. S. Lam and A. U. Shankar, "A relational notation for state transition systems,"IEEE Trans. Software Eng., vol. 16, pp. 755-775, July 1990.
[10] S. S. Lam and A. U. Shankar, "A composition theorem for layered systems,"Proceedings 11th Int. Symp. on Protocol Specification, Testing and Verification, Stockholm, June 1991.
[11] S. S. Lam and A. U. Shankar, "Understanding interfaces," inProc. Fourth Int. Conf. Formal Description Techniques, Sydney, Australia, 1991.
[12] S. S. Lam and A. U. Shankar, "A theory of interfaces and modules II--Methodology," Tech. Rep., Department of Computer Sciences, University of Texas at Austin, in preparation.
[13] S.S. Lam, A.U. Shankar, and T.Y.C. Woo, "Applying a Theory of Modules and Interfaces to Security Verifications,"Proc. IEEE Symp. Research in Security and Privacy, IEEE CS Press, Los Alamitos, Calif., Order No. 2168, 1991, pp. 136-154.
[14] L. Lamport, "A simple approach to specifying concurrent systems,"Commun. ACM, vol. 32, pp. 32-45, 1989.
[15] N. Lynch and M. R. Tuttle, "Hierarchical correctness proofs for distributed algorithms," inProc. Sixth Annu. ACM Symp. Principles of Distrib. Comput., 1987, pp. 137-151.
[16] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[17] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7, no. 4, pp. 417-426, July 1981.
[18] A. Pnueli, "In transition from global to modular temporal reasoning about programs," NATO ASI Series, vol. F13,Logics and Models of Concurrent Systems, K. R. Apt, Ed. Berlin: Springer-Verlag, 1984.
[19] A.U. Shankar and S.S. Lam, "A Stepwise Refinement Heuristic for Protocol Construction,ACM Trans. Programming Languages and Systems, Vol. 14, No. 3, July 1992, pp. 417-461.

Index Terms:
directed graphs; systems analysis; user interfaces; formal specification; interface theory; modules; composition theorem; system modelling; directed acyclic graph; nodes; arcs; interface satisfaction; service provider; service consumer; module design; module verification; system model; system design; specification
Citation:
S.S. Lam, A.U. Shankar, "A Theory of Interfaces and Modules - I: Composition Theorem," IEEE Transactions on Software Engineering, vol. 20, no. 1, pp. 55-71, Jan. 1994, doi:10.1109/32.263755
Usage of this product signifies your acceptance of the Terms of Use.