论文标题
PLCVERIF：可编程逻辑控制器的形式验证工具的状态
PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller
论文作者
论文摘要
可编程逻辑控制器（PLC）广泛用于工业自动化，包括CERN的安全系统。 PLC控制系统逻辑的不正确行为可能会因财产或环境损害甚至在某些情况下受伤而造成重大财务损失，因此确保其正确行为至关重要。虽然测试一直是验证PLC控制系统逻辑的传统方式，但CERN开发了一个模型检查平台，以进一步迈进并正式验证PLC逻辑。该平台称为PLCVERIF，该平台于2019年首次在CERN使用内部发布，自2020年9月以来，任何人都可以通过开放源代码许可证使用。在本文中，我们将首先概述PLCVERIF平台功能，然后再关注自2019年以来所做的改进，例如Siemens PLC编程语言的更大支持覆盖范围，对C边界模型检查器后端（CBMC）的更好支持以及释放PLCVERIF作为开放式软件的过程。
Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.
