.png){kind=icon}
.png){kind=icon}
Return
Automatic assertion generation with LLM for ICS program verification
.png){kind=icon}
PRE
AI
DOI：10.1016/j.jss.2025.112659.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Industrial Control System (ICS) programs are critical to industrial automation However, many ICS programs suffer from insufficient verification and pervasive logic flaws, posing significant risks to both system integrity and human safety. Existing ICS program verification approaches rely heavily on predefined logical assertions derived from expert knowledge, utilizing formal verification or testing-based methods to ensure correctness. This process is labor-intensive, requiring substantial manual effort and specialized expertise, which hampers automation and scalability. In this paper, we present a novel approach to automated assertion generation for ICS program verification, leveraging the critical insight that ICS execution logic is often documented in system specifications and user manuals. These documents can be used as constraints for validating logical correctness of ICS program. In particular, we abstract the constraints from ICS specification using large language models and map the variable names from these constraints to ICS program, enabling the automatic generation of ICS assertions. We implemented a prototype of our approach and conducted real-world experiments to demonstrate its effectiveness under 155 PLC projects. The results showed that our proposed method successfully generated 1251 assertions, achieving the correctness rate of 88.5%. Furthermore, we performed comparative experiments using different models to highlight the hardware efficiency and robustness of our solution.
Journal
IF:
4.1
Papers:
5.4K
Citations:
8.4K