2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2005)
Sept. 25, 2005 to Sept. 29, 2005
Dorel Lucanu , "A. I.Cuza" University
Gabriel Ciobanu , Romanian Academy
Mihai Daneş , "A. I.Cuza" University
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.
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