Design and verification of multi-rate distributed systems

Multi-rate systems arise naturally in distributed settings where computing units execute periodically according to their local clocks and communicate among themselves via message passing. We present a systematic way of designing and verifying such systems with the assumption of bounded drift for local clocks and bounded communication latency. First, we capture the system model through an architecture definition language (called RADL) that has a precise model of computation and communication. The RADL paradigm is simple, compositional, and resilient against denial-of-service attacks. Our radler build tool takes the architecture definition and individual local functions as inputs and generate executables for the overall system as output. In addition, we present a modular encoding of multi-rate systems using calendar automata and describe how to verify real-time properties of these systems using SMT-based infinite-state bounded model checking. Lastly, we discuss our experiences in applying this methodology to building high-assurance cyber-physical systems.