Many cyber-physical systems (CPSs), including avionics, automotive, robotics, etc., are virtually synchronous distributed control systems with interconnected physical environments. Such CPSs are notoriously hard to verify, due to their combination of nontrivial continuous dynamics, network delays, imprecise local clocks, asynchronous communication, etc. This talk presents effective approaches to design and verify virtually synchronous CPSs, based on automatic formal analysis and model-based software engineering methods. First, the Hybrid PALS pattern reduces the complexity of designing and verifying virtually synchronous CPSs. Second, Synchronous AADL allows engineers to easily design and verify synchronous models within the industrial modeling standard AADL. Third, model checking and SMT-based methods automatically analyze synchronous models based on their formal semantics.
Kyungmin Bae is an assistant professor in the Department of Computer Science and Engineering at POSTECH. He received his Ph.D. in Computer Science at University of Illinois at Urbana-Champaign, and earned his bachelor’s degrees in Computer Science and Mathematics from KAIST. His research interests are in software engineering and formal methods to develop safe, secure, and reliable computer systems, based on automatic analysis techniques, including model checking and SMT.