A process calculus approach to correctness enforcement of PLCs (full version)

Autor:	Lanotte, Ruggero, Merro, Massimo, Munteanu, Andrei
Rok vydání:	2020
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	We define a simple process calculus, based on Hennessy and Regan's Timed Process Language, for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specifications compliance. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/drop actuator commands and inter-controller communications. Then, we strengthen the capabilities of our monitors by allowing the insertion of actions to mitigate malware activities. This gives us deadlock-freedom monitoring: malware may not drag monitored controllers into deadlock states. Comment: 21-st Italian Conference on Theoretical Computer Science (ICTCS 2020). CEUR Workshop Proceedings
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2007.09399 Zobrazit plný text záznamu View this record from Arxiv