Sciweavers

Share
RSP
2007
IEEE

Verifying Distributed Protocols using MSC-Assertions, Run-time Monitoring, and Automatic Test Generation

10 years 5 months ago
Verifying Distributed Protocols using MSC-Assertions, Run-time Monitoring, and Automatic Test Generation
This paper addresses the need for formal specification and runtime verification of system-level requirements of distributed reactive systems. It describes a formalism for specifying global system behaviors in terms of Message Sequence Chart assertions and a technique for the evaluation of the likelihood of success of a distributed protocol under non-trivial communication conditions via discrete event simulation and runtime execution monitoring. We constructed a proof-of-concept prototype for the leader-election algorithm within a 4-node ring network. The prototype consists of the following components: (i) an OMNeT++ model of the network using non-trivial communication conditions, (ii) C++ code for the network agents, (iii) a system-level assertion stipulating the formal requirement for a correct, timebound, leader election, (iv) simulation of the formal assertion, (v) automatic scenario generation, and (vi) run-time monitoring of the formal assertion and stochastic-based estimation of...
Doron Drusinsky, Man-tak Shing
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where RSP
Authors Doron Drusinsky, Man-tak Shing
Comments (0)
books