Component-based formal modeling of PLC systems (Q2375648)

Summary: Functional validation is an important task in complex embedded system. The formal modeling of PLC systems for verification is a rough task. Good verification models should be faithful and concise. On the one hand, the model must be consistent with the system and on the other hand, the model must have suitable scale because of the state explosion problem of verification. This paper proposes a systemic method for the construction of a verification model. The PLC system architecture and PLC features are modeled as components. This is universal for all PLC applications. We give an automatic translation method for software modeling based on operational semantics. A small example is demonstrated for our approach.