Cyber-physical systems are increasingly employed in diverse areas, such as healthcare, transportation, avionics, and home appliances. Ensuring the safety of such systems is of great importance to avoid catastrophe. These systems usually consist of distributed multi-rate periodic processes, each of which owns a local clock, and they interact through message passing with a bounded transmission delay. Discrete time abstractions of such real-time systems are adopted to make their verification feasible. However, time notion complicates the verification of such systems. In this paper, we propose a timeless computation model for distributed multirate periodic processes to facilitates their verification. Our approach provides a safe programming model that eases building of those systems.We formalize the semantics of distributed multi-rate periodic processes as transition systems. To ensure the properties of such systems, we automate the computation of the minimum number of messages required by a process before its activation and the size of their local buffers as an optimization problem. In addition, we prove our timeless abstraction is sound.
Tue 6 Nov
|10:30 - 11:15|
Maryam DabaghchianUniversity of Utah
|11:15 - 12:00|
Wilson MizutaniUniversity of São Paulo