Techniques for executing and reasoning about specification diagrams
By
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
BibTeX
@inproceedings{conf/amast/ThatiTA04,
author = "Thati, Prasanna and Talcott, Carolyn L. and Agha, Gul",
editor = "Rattray, Charles and Maharaj, Savi and Shankland,
Carron",
title = "Techniques for Executing and Reasoning about
Specification Diagrams",
booktitle = "AMAST",
crossref = "conf/amast/2004",
ee = "http://dx.doi.org/10.1007/978-3-540-27815-3_39",
keywords = "formal methods, software engineering",
pages = "521-536",
year = "2004",
}
@proceedings{conf/amast/2004,
editor = "Rattray, Charles and Maharaj, Savi and Shankland,
Carron",
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",
}