Reasoning about implicit invocation

ABSTRACT

Implicit invocation [SN92, GN91] has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of specification and verification formalisms for such systems. Based on standard notions from process algebra and trace semantics, we define a formal computational model for implicit invocation. A verification methodology is presented that supports linear time temporal logic and compositional reasoning. First, the entire system is partioned into groups of components (methods) that behave independently. Then, local properties are proved for each of the groups. A precise description of the cause and the effect of an event supports this step. Using local correctness, independence of groups, and properties of the delivery of events, we infer the desired property of the overall system. Two detailed examples illustrate the use of our framework.

REFERENCES

• AAG95: Gregory D. Abowd , Robert Allen , David Garlan, Formalizing style to understand descriptions of software architecture, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.4, p.319-364, Oct. 1995 [doi>10.1145/226241.226244]
• BCTW96: Daniel J. Barrett , Lori A. Clarke , Peri L. Tarr , Alexander E. Wise, A framework for event-based software integration, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.378-421, Oct. 1996 [doi>10.1145/235321.235324]
• BG99: A. Berry and D. Garlan. Making architectural analysis reasonable. In Proceedings of First Ii'o&ing IFIP Conference on Software Architeture (WICSAl), February 1999. To appear.
• BJ89: K. P. Birman , T. A. Joseph, Exploiting replication in distributed systems, Distributed systems, ACM Press, New York, NY, 1990 [doi>10.1145/90417.90751]
• BN84: Andrew D. Birrell , Bruce Jay Nelson, Implementing remote procedure calls, ACM Transactions on Computer Systems (TOCS), v.2 n.1, p.39-59, February 1984 [doi>10.1145/2080.357392]
• CM88: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• Cor91: The Common Object Request Broker: Architecture and specification. OMG Document Number 91.12.1, December 1991. Revision 1.1 (Draft 10).
• DGJN98: J. Dingel, D. Garlan, S. Jha, and D. Notkin. Towards a formal treatment of implicit invocation using rely/guarantee reasoning. Formal Aspects of Computing, 199s. To appear.
• Dij76: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• Din97: Jürgen Dingel, Approximating UNITY, Proceedings of the Second International Conference on Coordination Languages and Models, p.320-337, September 01-03, 1997
• dR85: W.P. de Roever. The quest for compositionality - a survey of assertion-based proof systems for concurrent programs. Part I: Concurrency based on shared variables. In E. J. Neuhold and G. C&oust, editors, Formal Methods in Programming. IFIP, Elsevier Science Publishers, 1955.
• Ger89: C. Gerety. HP Softbench: A new generation of software development tools. Technical Report SESD-89-25, Hewlett-Packard Software Engineering Systems Division, Fort Collins, Colorado, November 1989.
• GHJV95: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• GKN92: David Garlan , Gail E. Kaiser , David Notkin, Using Tool Abstraction to Compose Systems, Computer, v.25 n.6, p.30-38, June 1992 [doi>10.1109/2.153255]
• GN91: David Garlan , David Notkin, Formalizing Design Spaces: Implicit Invocation Mechanisms, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.31-44, October 21-25, 1991
• Gol84: Adele Goldberg, SMALLTALK-80: the interactive programming environment, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1984
• GZ97: David Gelernter , Lenore D. Zuck, On What Linda Is: Formal Description of Linda as a Reactive System, Proceedings of the Second International Conference on Coordination Languages and Models, p.187-204, September 01-03, 1997
• Hoa69: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• Hoa85: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• ISO87: ISO. Information processing systems - open systems interconnection - LOTOS - a formal description technique based on the temporal ordering of observational behaviour. Technical Report ISO/TC 97/SC 21, International Standards Organization, 1987.
• Jon83: C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983 [doi>10.1145/69575.69577]
• Jub98: Henri Jubin, JavaBeans by example, Prentice-Hall, Inc., Upper Saddle River, NJ, 1998
• KP88: Glenn E. Krasner , Stephen T. Pope, A cookbook for using the model-view controller user interface paradigm in Smalltalk-80, Journal of Object-Oriented Programming, v.1 n.3, p.26-49, Aug./Sept. 1988
• Mil80: R. Mimer. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980.
• OG76: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• Rei90: Steven P. Reiss, Connecting Tools Using Message Passing in the Field Environment, IEEE Software, v.7 n.4, p.57-66, July 1990 [doi>10.1109/52.56450]
• San90: B.A. Sanders. Stepwise refinement of mixed specifications of concurrent programs. In M. Broy and C.B. Jones, editors, Proceedings of IFIP Working Conference on Programming and Methods, pages l-25. EIsevier Science Publishers (North Holland), May 1990.
• SN92: Kevin J. Sullivan , David Notkin, Reconciling environment integration and software evolution, ACM Transactions on Software Engineering and Methodology (TOSEM), v.1 n.3, p.229-268, July 1992 [doi>10.1145/131736.131744]
• Sun93: SunSoft. Tooltalk 1.1.1 Users's Guide, November 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.1 Project and People Management
          Subjects: Systems analysis and design

General Terms:
Design, Languages, Performance, Theory, Verification