Precise Monitoring of Cyber-Physical Technology under Uncertainty (PreCePT)

• Applicants: Professor Dr. Bernd Finkbeiner; Professor Dr. Martin Fränzle
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Computer Architecture, Embedded and Massively Parallel Systems ; Theoretical Computer Science
• Term: since 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 521273327

Cyber-Physical Systems (CPS) joining a physical environment and numerous embedded computational devices via digital networking into a tightly coupled system are rapidly becoming reality. They are at the heart of the recent push towards so-called smart environments. Most of these applications are inherently safety-critical in that malfunctions may endanger life, property, or the environment. The quest for ensuring the predictable, reliable, and safe operation of complex cyber-physical infrastructures is often addressed via stringent run-time monitoring. The applications pose high demands on the accuracy of the monitoring mechanisms, as lacking detection of an anomaly in system behaviour may induce the aforementioned risks, while spurious signalling of a potential problem may lead to performance-degrading exception handling up to full system lock-down. The PreCePT project addresses these demands by rigorously bridging formal methods and metrology in that it provides automatic generation of run-time monitors from formal specifications, with the generated monitors being faithful to the inevitable and significant inaccuracies and uncertainties arising when observing physical state through actual sensor devices. It develops best-in-class algorithms for the automatic monitoring of durational spatio-temporal properties under epistemic as well as aleatory uncertainties. These algorithms reconcile maximal exactness given the inaccuracies and partiality of the sensory equipment with hard real-time guarantees for their execution on embedded hardware in-situ. They are based on rigorous semantic models of both CPS dynamics and sensory equipment and on the use of advanced arithmetic constraint-solving technology, and are consequently provably optimal.

• DFG Programme: Research Grants