Formal Verification of CPS
This page covers projects on formal verification of cyber-physical systems (CPS), including timing, safety, and correctness guarantees.
Key Themes
- Timed automata and model checking for CPS
- Tool chains that connect real code to formal models
- Verification-guided design of controllers and schedulers
- Bridging the gap between theory and real systems
Selected Projects
- Timed Automata to Go (TADA): A pipeline for deriving timed automata models from system designs and code.
- Verification of Medical Devices: Applying formal methods to safety-critical monitoring and control algorithms.
- Education in Formal Methods: Teaching materials that connect real CPS examples with verification tools.