FMitF develops a provably correct stack that links formal hybrid-system models to PLC implementations, combining verified runtime monitoring with bidirectional model-code translation for industrial control systems.
Overview
This project advances a full formal-methods workflow from high-level differential dynamic logic models to executable PLC controller logic, with explicit links that preserve safety guarantees across design and runtime.
The public materials center on modular verification, monitor synthesis, and translation methods that connect model-level proofs with implementation artifacts used in realistic ICS settings.
The work builds on and extends prior HyPLC efforts, and informs follow-on work such as HyTwin for digital-twin-based security interventions.
Capabilities
Bidirectional translation between verified hybrid-program models and PLC control-logic structure
Runtime monitor synthesis that checks model-to-runtime compliance
Modular verification workflows for scalable ICS controller development
Reproducible experiment and evaluation artifacts rooted in water-treatment-style ICS case studies
Use Cases
Design-time verification of PLC control logic against hybrid-system safety requirements
Runtime validation of assumptions to detect deviations that invalidate offline proofs
Evaluation of resilient control behavior under representative cyber-physical perturbations
Figures
Publications
2019 / Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems
Luis Garcia, Stefan Mitsch, Andr{\'e} Platzer
ICCPS 2019 Best Paper Award Honorable Mention
2025 / NASA Formal Methods Symposium
Jainta Paul, Stefan Mitsch, Luis Garcia
Related Work
NSF Mid-Scale RI / 2024–2028
SPHERE CPS Enclave is a reconfigurable, remotely accessible industrial-control experimentation environment for repeatable and shareable cybersecurity studies spanning PLC logic, SCADA/HMI interaction, process telemetry, and configurable network behavior.
DARPA / 2020–2021 (18 months)
SMELL-CPS developed methods to extract interpretable mathematical expressions and semantic structure from low-level CPS control binaries, enabling reverse engineering, assurance analysis, and downstream automated testing workflows.