Decomposing, Transforming and Composing Diagrams: The Joys of Modular Verification

Abstract

The paper proposes a modular framework for the verification of temporal logic properties of systems based on the deductive transformation and composition of diagrams The diagrams represent abstractions of the modules composing the system, together with information about the environment of the modules The proof of a temporal specification is constructed with the help of diagram transformation and composition rules, which enable the gradual decomposition of the system into manageable modules, the study of the modules, and the final combination of the diagrams into a proof of the specification. We illustrate our methodology with the modular verification of a database demarcation protocol.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1998
Accession Number
ADA461279

Entities

People

  • Henny Sipma
  • Luca De Alfaro
  • Zohar Manna

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Availability
  • Classification
  • Computer Science
  • Computers
  • Contracts
  • Databases
  • Decomposition
  • Environment
  • Information Operations
  • Instructions
  • Monitoring
  • Specifications
  • Standards
  • Verification

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Software Engineering.