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", }