A Model-checking Algorithm for Formal-verification of Peer-to-peer Fault-tolerant Networks
2013-06-03 16:26:48 来源: 评论:0 点击:
Abstract— In this paper, the goal is to perform the verification of fault-tolerant properties of a peer-to-peer (P2P) network consisting of n nodes running n corresponding parallel processes. The specification of the processes is in the form of communicating finite state machines (CFSMs). The work to be reported in this paper follows the prequel work wherein, instead of the traditional approach to construct a single synchronous product machine by composing the given CFSMs, we simulate each of the CFSMs in the non-local environment of other CFSMs and generate a set of what are called Communicating Minimal Prefix Machines(CMPMs). In this paper, we take the CMPMs model and perform the reachability analysis of certain global state vectors without losing the locality of the CFSMs of the given specification. This method cuts down the state space explosion and also opens out the possibility of distributed exploration of the local CFSM states. Fault-tolerance consists of both safety and liveness properties and our approach provides a sound platform for performing state exploration/model-checking to verify these properties of the given set of application tasks that run in the P2P network.
Index Terms—CFSMs-to-CMPMs model, liveness, model-checking, P2P networks, safety, state-space explosion.
Cite: Sungeetha Dakshinamurthy and Vasumathi K. Narayanan , "A Model-checking Algorithm for Formal-verification of Peer-to-peer Fault-tolerant Networks," Lecture Notes on Information Theory, Vol.1, No.3, pp. 128-131, Sept. 2013. doi: 10.12720/lnit.1.3.128-131
Index Terms—CFSMs-to-CMPMs model, liveness, model-checking, P2P networks, safety, state-space explosion.
Cite: Sungeetha Dakshinamurthy and Vasumathi K. Narayanan , "A Model-checking Algorithm for Formal-verification of Peer-to-peer Fault-tolerant Networks," Lecture Notes on Information Theory, Vol.1, No.3, pp. 128-131, Sept. 2013. doi: 10.12720/lnit.1.3.128-131
Array
相关热词搜索:
上一篇:Efficient Voice Integrated Browser Using Naïve Approach
下一篇:Preventing Injection Attack by Whitelisting Inputs
分享到:
收藏
评论排行
频道总排行
频道本月排行
- 366Efficient Voice Integrated Browser Using Naïve Approach
- 2A Proactive Complex Event Proc...
- 14 Bit Comparator Design Based on Reversible Logic Gates
- 1Design Consideration for Config...
- 1A Comparative Analysis for WLM...
- 1A Hybrid Mutation-based Artific...
- 1A Device Management and Credit...
- 1Design and Development of a H...
- 1Information Security Requirement...
- 1A Model-checking Algorithm for...