Tue 6 Nov 2018 10:30 - 11:15 at Charles River - II Chair(s): Philipp Haller

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 - 12:00: DocSymposium - II at Charles River
Chair(s): Philipp HallerKTH, Sweden
splash-2018-Doctoral-Symposium10:30 - 11:15
Maryam DabaghchianUniversity of Utah
splash-2018-Doctoral-Symposium11:15 - 12:00
Wilson MizutaniUniversity of São Paulo