A formal approach to property testing in causally consistent distributed traces |
| |
Authors: | H H Hallal S Boroday A Petrenko A Ulrich |
| |
Affiliation: | (1) CRIM, 550 Sherbrooke West, Suite 100, Montreal, H3A 1B9, Canada;(2) Corporate Technology CT SE1, Siemens AG, Otto-Hahn-Ring 6, 81730 Munich, Germany |
| |
Abstract: | A formal framework for the analysis of execution traces collected from distributed systems at run-time is presented. We introduce
the notions of event and message traces to capture the consistency of causal dependencies between the elements of a trace.
We formulate an approach to property testing where a partially ordered execution trace is modeled by a collection of communicating
automata. We prove that the model exactly characterizes the causality relation between the events/messages in the observed
trace and discuss the implementation of this approach in SDL, where ObjectGEODE is used to verify properties using model-checking
techniques. Finally, we illustrate the approach with industrial case studies.
Received May 2004, Revised February 2005, Accepted April 2005 by J. Derrick, M. Harman and R. M. Herons |
| |
Keywords: | Distributed systems System validation Passive testing Trace analysis SDL Monitoring |
本文献已被 SpringerLink 等数据库收录! |
|