Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05) (2005)
Sept. 25, 2005 to Sept. 29, 2005
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.
D. Lucanu, G. Ciobanu and M. Daneş, "Specification of Coordinated Objects and Verification of Their Temporal Properties," Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05)(SYNASC), Timisoara, Romania, 2005, pp. 259-266.