论文标题
plc的正确性执行的过程计算方法（完整版）
A process calculus approach to correctness enforcement of PLCs (full version)
论文作者
论文摘要
我们根据Hennessy和Regan的定时过程语言来定义一个简单的过程微积分，用于指定通信可编程逻辑控制器（PLC）的网络，并具有强制执行规格合规性的监视器。我们定义了一个综合算法，即给定未腐烂的PLC返回一个监视器，该监视器可以强制执行PLC的正确性，即使注射了可能会伪造/删除执行器命令和Inter-Controller Communications的恶意软件。然后，我们通过允许插入动作来减轻恶意软件活动来增强监视器的功能。这为我们提供了死锁自由监控：恶意软件可能不会将受监控的控制器拖入僵局。
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.
