Abstract Many important properties of cyber-physical systems (CPS) are defined upon the relationship between multiple executions simultaneously in continuous time. Examples include probabilistic fairness and sensitivity to modeling errors (i.e., parameters changes) for real-valued signals. These requirements can only be specified by hyperproperties. In this talk, I will first introduce new hyper probabilistic temporal logics that formally capture these hyperproperties. Then, I will introduce new statistical model checking (SMC) techniques for verifying hyper logic formulas. Finally, I will demonstrate the efficiency of the SMC algorithms on CPS benchmarks with varying levels of complexity.
Biography Yu Wang is currently a postdoctoral associate of Electrical and Computer Engineering at Duke University. He received his PhD degree in Mechanical Engineering from the University of Illinois at Urbana-Champaign. His research focuses on the security and privacy in cyber-physical systems. His recent paper was selected one of the best paper finalists of EMSOFT ‘19. His Ph.D. dissertation “Statistical Verification and Differential Privacy in Cyber-Physical Systems” was for nominated for the CSL PhD Thesis Award of the Coordinated Science Laboratory of UIUC.