Automatic abstraction for verification of cyber-physical systems


Models of cyber-physical systems are inherently complex since they must represent hardware, software, and the physical environment. Formal verification of these models is often precluded by state explosion. Fortunately, many important properties may only depend upon a relatively small portion of the system being accurately modeled. This paper presents an automatic abstraction methodology that simplifies the model accordingly. Preliminary results on a fault-tolerant temperature sensor are encouraging.

Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems
Hao Zheng
Hao Zheng
University of South Florida, Associate Professor