Visible to the public Methods and Tools for Verification of Cyber-Physical Systems


Cyber-Physical Systems (CPS) are deployed in a wide variety of safety critical applications from avionics, medical, and automotive domains. For these applications, it is essential to create a precise specification and formally verify that the implementation behaves as specified. The formal verification of these systems presents a wide variety of challenges. Models of these systems must represent the physical world, analog sensors and actuators, computer hardware and software, networks, and feedback control.


Visible to the public Automatic Abstraction for Verification of Cyber-Physical Systems

Verification of cyber-physical systems is complicated by both their heterogeneous nature as well as their sheer complexity. Cyber-physical systems include hardware, software, and physical  environment, so a formal model must integrate all of these concerns.