% % GENERATED FROM http://acme.able.cs.cmu.edu % by : anonymous % IP : ec2-3-142-249-192.us-east-2.compute.amazonaws.com % at : Thu, 03 Apr 2025 01:59:27 -0400 GMT % % Selection : Publication #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} }