| 170 |
@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}
}
|
|
