Distributed cyber-physical systems (DCPS) are pervasive in areas such as aeronautics, ground transportation, medical systems, etc. They are often hierarchical distributed control systems whose components operate with different rates, and that should behave in a virtually synchronous way. DCPS design and verification is quite challenging because of asynchronous communication, skews of the local clocks, and network delays. Furthermore, their model checking verification typically becomes unfeasible due to the huge state space explosion caused by the system’s concurrency. Together with colleagues at UIUC and Rockwell-Collins, we have proposed the Multirate PALS ("physically asynchronous, logically synchronous") methodology that reduces the problem of designing and verifying such virtually synchronous multirate systems to the much simpler tasks of designing and verifying their underlying synchronous design. To make the Multirate PALS methodology available within an industrial modeling environment, we define the modeling language Multirate Synchronous AADL, which can be used to specify multirate synchronous designs using AADL, an industrial modeling standard for avionics and automotive systems. We then define the formal semantics of Multirate Synchronous AADL in real-time rewriting logic, and integrate model checking processes into the existing OSATE tool environment for AADL. We illustrate such design and verification of Multirate Synchronous AADL models with two avionics case studies.

Kyungmin Bae is a PhD candidate in Computer Science at University of Illinois at Urbana-Champaign. His research interests are in formal methods and model checking; in particular, developing rewriting-based model checking techniques to verify a wide range of real-world applications, including real-time and cyber-physical systems. He received the Feng Chen Memorial Award from the Department of Computer Science at UIUC in 2013, and earned his bachelor's degrees in Computer Science and Mathematics from KAIST.