Projects

University of Michigan

STARnet Program TerraSwarm Project

• I focused on security and privacy issues in discrete event systems, with an emphasize on opacity. I proposed a novel obfuscation method called insertion/edit functions to enforce opacity by providing plausible deniability and leveraged results from game theory for reactive synthesis to solve the problem.

Expeditions in Computer Aided Program Engineering

• I further extended the method of insertion/edit functions for opacity enforcement, by considering the inference capabilities of the outside malicious intruders. I investigated both strong and weak intrusion scenarios, then developed opacity-enforcing tools correspondingly. The proposed method outperforms our previous ones. I was also responsible for implementing the algorithms and developing software tools.

NSF SaTC project TWC: Small: Intrusion Detection and Resilience Against Attacks in Cyber and Cyber-Physical Control Systems

• I investigated intrusion detection and mitigation in the framework of discrete event systems. Specifically, I studied the attack-defense dynamics by two-player game structure and developed strategies for the attacker and the defender in either qualitative or quantitive setting.

NSF project CPS: Small: Energy-Aware Formal Methods Synthesis for Supervisory Control and Information Acquisition in Cyber-Physical Systems.

• I investigated joint synthesis of supervisory control and information acquisition modals in cyber-physical systems, especially for secrecy obfuscation and supervisory control under the framework of qualitative and quantitive graph games. I also contributed to infinite-horizon optimal non-stochastic/stohastic supervisory control theories, with applications in autonomous driving and motion planning of robotics.