loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05)
Specification of Coordinated Objects and Verification of Their Temporal Properties
Timisoara, Romania
September 25-September 29
ISBN: 0-7695-2453-2
ASCII Text
x 
 
Mihai Daneş, Dorel Lucanu, Gabriel Ciobanu, "Specification of Coordinated Objects and Verification of Their Temporal Properties," Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on, pp. 259-266, Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/SYNASC.2005.67,
author = {Mihai Daneş and Dorel Lucanu and Gabriel Ciobanu},
title = {Specification of Coordinated Objects and Verification of Their Temporal Properties},
journal ={Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on},
volume = {0},
year = {2005},
isbn = {0-7695-2453-2},
pages = {259-266},
doi = {http://doi.ieeecomputersociety.org/10.1109/SYNASC.2005.67},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on
TI - Specification of Coordinated Objects and Verification of Their Temporal Properties
SN - 0-7695-2453-2
SP259
EP266
A1 - Mihai Daneş,
A1 - Dorel Lucanu,
A1 - Gabriel Ciobanu,
PY - 2005
KW - null
VL - 0
JA - Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on
ER -
 
Mihai Daneş, "A. I.Cuza" University
Dorel Lucanu, "A. I.Cuza" University
Gabriel Ciobanu, Romanian Academy
This paper presents a specification 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 specified system, and verify its temporal properties. We use the Alternating Bit Protocol to exemplify our specification framework, and SMV to verify its correctness.
Citation:
Mihai Daneş, Dorel Lucanu, Gabriel Ciobanu, "Specification of Coordinated Objects and Verification of Their Temporal Properties," synasc, pp.259-266, Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.