Towards a Formal Treatment of Implicit Invocation

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 29, 1997
Accession Number
ADA329940

Entities

People

  • D. Garlan
  • D. Notkin
  • J. Dingel
  • Shalini Jha

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Computer Programming
  • Computer Science
  • Computers
  • Debugging
  • Engineering
  • Homosexuality
  • Information Processing
  • Information Systems
  • Judgment
  • Language
  • Operating Systems
  • Programming Languages
  • Software Design
  • Software Development
  • Software Development Tools
  • Standards
  • Systems Engineering

Fields of Study

  • Computer science

Readers

  • Software Engineering.
  • Theoretical Analysis.
  • Traumatic Brain Injury (TBI) and Cognitive Aging in the Guam and Border Populations Affected by Alzheimer's Disease and Tau-Associated Dementias.