Static and dynamic analysis of timed distributed traces

Parasara Sridhar Duggirala, Taylor T. Johnson, Adam Zimmerman, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper presents an algorithm for checking global predicates from distributed traces of cyber-physical systems. For an individual agent, such as a mobile phone or a robot, a trace is a finite sequence of state observations and message histories. Each observation has a possibly inaccurate timestamp from the agent's local clock. The challenge is to symbolically over approximate the reachable states of the entire system from the unsynchronized traces of the individual agents. The presented algorithm first approximates the time of occurrence of each event, based on the synchronization errors of the local clocks, and then over approximates 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 distributed Android apps. Experimental results illustrate that interesting properties like safe separation, correct geocast delivery, and distributed deadlocks can be checked for up-to twenty agents in minutes.

Original languageEnglish (US)
Title of host publicationProceedings of the 2012 IEEE 33rd Real-Time Systems Symposium, RTSS 2012
Pages173-182
Number of pages10
DOIs
StatePublished - Dec 1 2012
Event2012 IEEE 33rd Real-Time Systems Symposium, RTSS 2012 - San Juan, Puerto Rico
Duration: Dec 5 2012Dec 7 2012

Publication series

NameProceedings - Real-Time Systems Symposium
ISSN (Print)1052-8725

Other

Other2012 IEEE 33rd Real-Time Systems Symposium, RTSS 2012
Country/TerritoryPuerto Rico
CitySan Juan
Period12/5/1212/7/12

Keywords

  • distributed cyber-physical systems
  • distributed systems
  • event ordering
  • hybrid systems
  • verification

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Static and dynamic analysis of timed distributed traces'. Together they form a unique fingerprint.

Cite this