Runtime Verification with Multi-valued Formula Rewriting

Runtime verification is a promising method that tries to bridge the gap between formal methods and traditional testing. In this paper, we present an improved runtime verification method via multi-valued formula rewriting. A 3-valued executable semantics for finite trace LTL is formally defined, and an algorithm based on this new semantics is proposed and implemented in Maude, which is a high performance rewriting system. To improve the efficiency of our algorithm, we introduce a novel approximation technique, which reduces rewriting steps by sacrificing some abilities of detecting the satisfactions of LTL properties. Moreover, this technique provides a quick procedure for distinguishing non-monitor able properties from those can be monitored. Finally, experiments are conducted to show the strength and weakness of the presented method.