Abstract:
This paper presents an algorithm for checking global predicates from traces of distributed embedded systems. For an individual agent, such as a mobile phone, tablet, or robot, a trace is a finite sequence of state observations and message histories. Each recording has a possibly inaccurate timestamp from the agent's local clock. The challenge is to symbolically overapproximate the reachable states of the entire system from the unsynchronized traces of the individual devices. The presented algorithm first approximates the time of occurrence of each event, based on the synchronization errors of the local clocks, and then overapproximates the reach sets of the continuous variables between consecutive observations. The algorithm is shown to be sound; it is also complete for a class of agents with restricted continuous dynamics and when the traces have precise information about timing synchronization inaccuracies. The algorithm is implemented in an SMT solver-based tool for analyzing traces of distributed Android Apps. Experimental results using the tool illustrate that interesting properties like safe separation, correct geocast delivery, and distributed deadlocks can be automatically checked and potential counterexamples can be found. Analyzing these properties on a 10 second long distributed trace for 20 agents completes within a minute and often in seconds, suggesting that the approach can scale.
Reference:
Parasara Sridhar Duggirala, Taylor T. Johnson, Adam Zimmerman, Sayan Mitra, "Static and Dynamic Analysis of Timed Distributed Traces", In Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS 2012), San Juan, Puerto Rico, pp. 173–182, 2012, dec.
Bibtex Entry:
@inproceedings{duggirala2012rtss,
author = {Parasara Sridhar Duggirala and Taylor T. Johnson and Adam Zimmerman and Sayan Mitra},
title = {Static and Dynamic Analysis of Timed Distributed Traces},
year = {2012},
booktitle = {Proceedings of the 33rd IEEE Real-Time Systems Symposium (<a href='http://www.rtss.org/'>RTSS 2012</a>)},
address = {San Juan, Puerto Rico},
month = dec,
pages = {173--182},
doi = {10.1109/RTSS.2012.69},
gsid = {7478096960006514961},
abstract = {This paper presents an algorithm for checking global predicates from traces of distributed embedded systems. For an individual agent, such as a mobile phone, tablet, or robot, a trace is a finite sequence of state observations and message histories. Each recording has a possibly inaccurate timestamp from the agent's local clock. The challenge is to symbolically overapproximate the reachable states of the entire system from the unsynchronized traces of the individual devices. The presented algorithm first approximates the time of occurrence of each event, based on the synchronization errors of the local clocks, and then overapproximates the reach sets of the continuous variables between consecutive observations. The algorithm is shown to be sound; it is also complete for a class of agents with restricted continuous dynamics and when the traces have precise information about timing synchronization inaccuracies. The algorithm is implemented in an SMT solver-based tool for analyzing traces of distributed Android Apps. Experimental results using the tool illustrate that interesting properties like safe separation, correct geocast delivery, and distributed deadlocks can be automatically checked and potential counterexamples can be found. Analyzing these properties on a 10 second long distributed trace for 20 agents completes within a minute and often in seconds, suggesting that the approach can scale.},
pdf = {http://www.taylortjohnson.com/research/duggirala2012rtss.pdf},
}