Home   Research Publications Members Related Software
IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
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   Bibtex entry   Plain Text

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.  
    Created: 2006-08-22 14:38:10     Modified: 2006-08-22 14:40:07
Feedback: ABLE Webmaster
Last modified: Mon February 12 2018 11:21:51