Techniques for executing and reasoning about specification diagrams

Prasanna Thati, Carolyn Talcott, Gul Agha

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Specification Diagrams (SD) [19] are a graphical notation for specifying the message passing behavior of open distributed object systems. SDs facilitate specification of system behaviors at various levels of abstraction, ranging from high-level specifications to concrete diagrams with low-level implementation details. We investigate the theory of may testing equivalence [15] on SDs, which is a notion of process equivalence that is useful for relating diagrams at different levels of abstraction. We present a semantic characterization of the may equivalence on SDs which provides a powerful technique to relate abstract specifications and refined implementations. We also describe our prototypical implementation of SDs and of a procedure that exploits the characterization of may testing to establish equivalences between finitary diagrams (without recursion).

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsCharles Rattray, Savitri Maharaj, Carron Shankland
PublisherSpringer
Pages521-536
Number of pages16
ISBN (Print)3540223819, 9783540223818
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3116
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Graphical specification languages
  • May testing
  • Rewriting logic
  • TT-calculus
  • Trace equivalence

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Techniques for executing and reasoning about specification diagrams'. Together they form a unique fingerprint.

Cite this