Accession Number : ADA329940
Title : Towards a Formal Treatment of Implicit Invocation
Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Dingel, J. ; Garlan, D. ; Jha, S. ; Notkin, D.
PDF Url : ADA329940
Report Date : 29 JUL 1997
Pagination or Media Count : 24
Abstract : Implicit invocation SN92,GN91 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 Jon83,St(phi)91. 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.
Descriptors : *COMPUTER COMMUNICATIONS, *COMPUTER ARCHITECTURE, *CONCURRENT ENGINEERING, SOFTWARE ENGINEERING, COMPUTER AIDED DESIGN, DISTRIBUTED DATA PROCESSING, PARALLEL PROCESSING, OPERATING SYSTEMS(COMPUTERS), SYSTEMS ANALYSIS, DESIGN CRITERIA.
Subject Categories : Computer Systems
Distribution Statement : APPROVED FOR PUBLIC RELEASE