Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911067515387904 |
|---|---|
| author | Lee, Jaeseo Bae, Kyungmin |
| author_facet | Lee, Jaeseo Bae, Kyungmin |
| contents | Programmable Logic Controllers (PLCs) are widely used in industrial automation to control physical systems. As PLC applications become increasingly complex, ensuring their correctness is crucial. Existing formal verification techniques focus on individual PLC programs in isolation, often neglecting interactions with physical environments and network communication between controllers. This limitation poses significant challenges in analyzing real-world industrial systems, where continuous dynamics and communication delays play a critical role. In this paper, we present a unified formal framework that integrates discrete PLC semantics, networked communication, and continuous physical behaviors. To mitigate state explosion, we apply partial order reduction, significantly reducing the number of explored states while maintaining correctness. Our framework enables precise analysis of PLC-driven systems with continuous dynamics and networked communication. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_15596 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Analysis of Networked PLC Controllers Interacting with Physical Environments Lee, Jaeseo Bae, Kyungmin Programming Languages Logic in Computer Science Programmable Logic Controllers (PLCs) are widely used in industrial automation to control physical systems. As PLC applications become increasingly complex, ensuring their correctness is crucial. Existing formal verification techniques focus on individual PLC programs in isolation, often neglecting interactions with physical environments and network communication between controllers. This limitation poses significant challenges in analyzing real-world industrial systems, where continuous dynamics and communication delays play a critical role. In this paper, we present a unified formal framework that integrates discrete PLC semantics, networked communication, and continuous physical behaviors. To mitigate state explosion, we apply partial order reduction, significantly reducing the number of explored states while maintaining correctness. Our framework enables precise analysis of PLC-driven systems with continuous dynamics and networked communication. |
| title | Formal Analysis of Networked PLC Controllers Interacting with Physical Environments |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2507.15596 |