  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.
