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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Model Checking of PLC Code Specifications: Impact of GRAFCET Features to State Space Size

  • Robin Mroß,
  • Marcus Völker,
  • Stefan Kowalewski,
  • Aron Schnakenbeck,
  • Alexander Fay

摘要

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.