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...

• Type: Conference
• Year: 2007
• Where: RSP
• Authors: Doron Drusinsky, Man-tak Shing
• Keywords: Formal Assertion, Non-trivial Communication Conditions, Rapid System Prototyping, RSP 2007, System-level Assertion