Home   Research Publications Members Related Software
IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
      Login
Publication no #170   Download bibtex file Type :   Html | Bib | Both
Add to my selection
Towards a formal treatment of implicit invocation using rely/guarantee reasoning

Jurgen Dingel, David Garlan, Somesh Jha and David Notkin.


In Formal Aspects of Computing, Vol. 1-:193-213, 1998. Supersedes CMU-CS-97-153.

Online links: PDF 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.

Keywords: Implicit Invocation, Formal Methods, Software Architecture.  
@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}
}
    Created: 2006-08-22 14:38:10     Modified: 2006-08-22 14:40:07
Feedback: ABLE Webmaster
Last modified: Sat October 12 2019 16:15:32
        BibAdmin