| Year | 2005 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Mihai Danes, Gabriel Ciobanu, Dorel Lucanu |
Links
Abstract
This paper presents a specication framework for coordinated objects. Coordination is described by a process. The integration of the concurrent objects and the coordinating process is given by a wrapper. Using an encoding into Maude, we extract a Kripke structure describing the behavior of the specied system, and verify its temporal properties.
We use the Alternating Bit Protocol to exemplify our specification framework, and SMV to verify its correctness.
BibTeX
@INPROCEEDINGS{synasc05,
author = {M. Danes and G. Ciobanu and D. Lucanu},
title = {Specification of Coordinated Objects and Verification of
Their Temporal Properties},
booktitle = {7th International Workshop on Symbolic and Numeric Algorithms for
Scientific Computing},
pages = {259-266},
year = {2005},
publisher = {IEEE Computer Society},
optnote = {A revised version appeared in IEEE Computer Press},
url_publisher = {http://doi.ieeecomputersociety.org/10.1109/SYNASC.2005.67},
url={http://synasc05.info.uvt.ro/[SYNASC]}
}