Home   Research Publications Members Related Software
IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
Publication no #172   Download bibtex file Type :   Html | Bib | Both
Add to my selection
Reasoning about Implicit Invocation

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

In Proceedings of the Sixth International Symposium on the Foundations of Software Engineering (FSE-6), Lake Buena Vista, Florida, November 1998.

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 specication and verication formalisms for such systems. Based on standard notions from process algebra and trace semantics, we dene a formal computational model for implicit invocation. A verication 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 eect 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.

Keywords: Formal Methods, Implicit Invocation, Model Checking, Software Architecture.  
    Created: 2006-08-22 14:42:08
Feedback: ABLE Webmaster
Last modified: Tue June 20 2017 16:43:41