کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
455006 | 695330 | 2009 | 10 صفحه PDF | دانلود رایگان |

Verification and conformance testing for protocol specification, the key part of the protocol development process, are complementary technologies employed to increase confidence that a system will function as stated in its specifications. In this paper, we verify the safety and liveness of the protocol specified for the Labeled Transition System (LTS) by using a model-checking method and implementing the testing tool, which experimentally demonstrates the presence of deadlock and reachability from the initial state to a random state. Implementing the testing tool can use modal mu-calculus to assess whether protocol model properties, presented by modal logic, meet protocol specifications. In addition, we propose a conformance testing tool to check correct implementation of sequences that have been derived by the UIO method from the specification of the protocol being verified. This generating tool uses the C++ language in the Microsoft Windows NT environment.
Journal: Computer Standards & Interfaces - Volume 31, Issue 2, February 2009, Pages 362–371