Talk "PALS: Virtual Synchrony for Cyber-Physical Systems"

by Peter Ölveczky

Mon, 04 September 2017 at 09:40 am in Berlin, Germany

Abstract: Many cyber-physical systems (CPSs)--including avionics systems, automotive systems, power plant controllers, etc.--are virtually synchronous: logically they operate in rounds, but must be realized in a distributed real-time environment with hard real-time bounds. Such systems are hard to design because of asynchronous communication, network delays, and clocks skews. In addition, their model checking typically becomes unfeasible due to the large state spaces caused by the interleavings. For virtual synchronous CPSs where the underlying infrastructure provides a bound on the network delays and clocks skews, we have developed, formalized, and formally verified the PALS (physically asynchronous, logically synchronous) architectural pattern. PALS significantly reduces the design and verification of virtually synchronous CPSs by allowing us to design and verify the underlying synchronous design; PALS then generates a correct-by-construction distributed design. For example, PALS reduces the state space encountered in an integrated modular avionics design developed at Rockwell Collins from 3 million---in the over-simplified case with no message delays and no clock skew--to a mere 185 states. To make the PALS design and verification methodology available to domain experts, we have defined the Synchronous AADL modeling language. Synchronous AADL allows engineers to define their synchronous PALS designs in the industrial modeling standard AADL. We have also integrated Real-Time Maude model checking of such Synchronous AADL models into the OSATE modeling environment for AADL, so that engineers can model check their designs directly in OSATE. Since some CPSs are multi-rate systems, we have extended both PALS and Synchronous AADL to the multi-rate setting, and have applied our methodology to analyze a textbook algorithm for turning an airplane; our analysis indicated that the algorithm did not provide a safe turn, so we also designed and model checked a modified turning algorithm. If time allows, I will also briefly discuss our recent extension of the PALS methodology to the hybrid setting, where the verification of synchronous Hybrid PALS models can be reduced to SMT solving over nonlinear theories of the real numbers. This talk is based on joint work with: - Kyungmin Bae (now at POSTECH Korea), José Meseguer, Lui Sha, and others at UIUC - Darren Cofer and Steve Miller at Rockwell Collins - colleagues at CMU