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.
|Titolo:||A process calculus approach to correctness enforcement of PLCs|
MERRO, Massimo (Corresponding)
|Data di pubblicazione:||2020|
|Appare nelle tipologie:||04.01 Contributo in atti di convegno|