Open Systems Laboratory at Illinois

Techniques for executing and reasoning about specification diagrams

By Prasanna Thati, Carolyn L. Talcott, and Gul Agha. In AMAST, volume 3116 of Lecture Notes in Computer Science, 521–536. Springer, 2004.

Full Text:
Download PDF
Publisher Link:


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).

Keywords  Graphical specification languages - π-calculus - may testing - trace equivalence - rewriting logic


    author = "Thati, Prasanna and Talcott, Carolyn L. and Agha, Gul",
    editor = "Rattray, Charles and Maharaj, Savi and Shankland,
    title = "Techniques for Executing and Reasoning about
             Specification Diagrams",
    booktitle = "AMAST",
    crossref = "conf/amast/2004",
    ee = "",
    keywords = "formal methods, software engineering",
    pages = "521-536",
    year = "2004",

    editor = "Rattray, Charles and Maharaj, Savi and Shankland,
    title = "Algebraic Methodology and Software Technology, 10th
             International Conference, AMAST 2004, Stirling, Scotland, UK, July
             12-16, 2004, Proceedings",
    isbn = "3-540-22381-9",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "3116",
    year = "2004",