@Article{DGJN97,
      AUTHOR = {Dingel, Jurgen and Garlan, David and Jha, Somesh and Notkin, David},
      TITLE = {Towards a formal treatment of implicit invocation using rely/guarantee reasoning},
      YEAR = {1998},
      JOURNAL = {Formal Aspects of Computing},
      VOLUME = {1-},
      PAGES = {193-213},
      PDF = {http://www.cs.cmu.edu/afs/cs/project/able/ftp/implinvoc-fac98/implinvoc-fac98.pdf},
      PS = {http://www.cs.cmu.edu/afs/cs/project/able/ftp/implinvoc-fac98/implinvoc-fac98.ps},
      ABSTRACT = {Implicit invocation 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. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed. },
      NOTE = {Supersedes CMU-CS-97-153.},
      KEYWORDS = {Implicit Invocation, Formal Methods, Software Architecture}
}