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