Abstract

A cyber-physical system often consists of distributed multi-rate periodic processes that communicate using message passing; each process owns a local clock not synchronized with others. We call such systems quasi-periodic distributed systems. Traditionally, one would model them using timed automata, thereby having to deal with high-complexity verification problems. Recently, several researchers proposed discrete-time abstractions based on the calendar model to make the verification more tractable. However, even the calendar model contains a notion of time in the form of a global clock. We propose a novel, timeless computation model for quasi-periodic distributed systems to facilitate their verification. The main idea behind our model is to judiciously replace synchronization using a global clock and calendar with synchronization over lengths of message buffers. We introduce a simple domain-specific language for programming of such systems and use it to formalize the semantics of both the calendar and timeless model. Then, we prove that our timeless model is an overapproximation of the calendar model. Finally, we evaluate our timeless model using several benchmarks.

Citation

BibTeX

@inproceedings{2019_memocode_dr,
  title = {A Timeless Model for The Verification of Quasi-Periodic Distributed Systems},
  author = {Maryam Dabaghchian and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 17th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)},
  publisher = {ACM},
  pages = {4:1--4:11},
  doi = {10.1145/3359986.3361201},
  year = {2019}
}

Acknowledgements

This work was supported in part by the National Science Foundation (NSF) awards CCF 1552975 and CCF 1837051. We thank Ankush Desai for introducing us to the problem of the verification of quasi-periodic distributed systems. We also thank Natarajan Shankar for insightful discussions that helped us to improve this paper.