Model Checking of PLC Code Specifications: Impact of GRAFCET Features to State Space Size
摘要
Formal methods can help make safety-critical systems safer by detecting problems before they occur. In general, the earlier a problem is caught during development, the better. Therefore, applying formal methods not to the actual code, but to its specification, before a line of code is even written, can make fixing problems much easier. A property of formal verification, however, is that the state space tends to scale exponentially with the size of the analysed system, which applies to verification of specifications as much as it applies to verification of code. In this work, we take previous work to translate the specification language GRAFCET to GAL for verification purposes and analyse which components of GRAFCET especially impact the size of the resulting state space. Our approach is to construct families of GRAFCET that vary specific parameters while leaving other parameters the same, then feed the resulting GAL models into the model checker ITS-tools and query the size of the state space to draw conclusions about the impact of the different structures in GRAFCET.