Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Sep 17, 2019
Many cyber-physical systems (e.g. Industrial Automation systems, Medical Devices, and Autonomous Vehicles) are designed with the presumption of a reliable shared clock. This is a very risky approach. Shared clocks can drift or even fail, leading to catastrophic results. I will present an approach to modeling shared-clock systems with TLA+ that can expose clock-based failure modes and drift envelopes, allowing the system designer to better understand the system’s failure boundaries. I will also share strategies to constrain the search space, and general experiences from the use of TLA+ for this class of problem.