Paper Info
Title
Formal Modelling of PLC Systems by BIP Components
Abstract
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.
Year
DOI
Venue
2013
10.1109/COMPSAC.2013.85
COMPSAC
Keywords
Field
DocType
programmable controllers,bip framework,bip components,automatic framework,specifical plc feature,plc application,plc software,plc systems,good verification model,plc modeling,control engineering computing,bip,programable logic controllers,complex embedded system,system architecture,state explosion problem,formal modelling,verification model,automatic translation based modeling method,embedded systems,plc system,plc instruction,operational semantics,formal verification,complex embedded systems,hardware,semantics,computational modeling,synchronization
Synchronization,Operational semantics,Computer science,Real-time computing,Software,Programmable logic controller,Systems architecture,Automatic translation,Semantics,Formal verification
Conference
ISSN
Citations 
PageRank 
0730-3157
0
0.34
References 
Authors
9
5
Name
Order
Citations
PageRank
Rui Wang161.89
Yong Guan278782.67
Liming Luo384.41
Xiaoyu Song431846.99
Jie Zhang5366.46