Formal Modelling of PLC Systems by BIP Components

Programable logic controllers (PLCs) are complex embedded systems which are widely used in industry. The formal modeling of PLC system for verification is a rough task. Good verification model should be faithful with the system, and also should have suitable scale because of the state explosion problem of verification. This paper proposes an automatic framework for the construction of verification model of PLC systems. BIP (Behavior, Interaction, Priority) separates behavioral and architectural aspects in modelling. Specifical PLC features and system architecture are modelled by BIP framework. They are universal for all PLC applications. We define the operational semantics of PLC instruction and present an automatic translation based modeling method for PLC software. A small example is demonstrated for our approach.