The Community for Technology Leaders
2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2005)
Timisoara, Romania
Sept. 25, 2005 to Sept. 29, 2005
ISBN: 0-7695-2453-2
pp: 259-266
Dorel Lucanu , "A. I.Cuza" University
Gabriel Ciobanu , Romanian Academy
Mihai Daneş , "A. I.Cuza" University
ABSTRACT
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.
INDEX TERMS
null
CITATION
Dorel Lucanu, Gabriel Ciobanu, Mihai Daneş, "Specification of Coordinated Objects and Verification of Their Temporal Properties", 2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, vol. 00, no. , pp. 259-266, 2005, doi:10.1109/SYNASC.2005.67
78 ms
(Ver 3.3 (11022016))