The graphical modeling language GRAFCET is used as a formal specification language in industrial control design. This paper proposes a static analysis approach based on the control flow of GRAFCET using abstract interpretation to allow verification on specification level. GRAFCET has different elements leading to concurrent behavior, which in general results in a large state space. To get precise results and reduce the state space, we propose an analysis suitable for GRAFCET instances without concurrent behavior. We point out how to check for the absence of concurrency and present a flow-sensitive analysis for these GRAFCET instances. The proposed approach is evaluated on an industrial-sized example.

翻译：图形化建模语言GRAFCET在工业控制设计中用作形式化规范语言。本文提出一种基于GRAFCET控制流并采用抽象解释的静态分析方法，以实现规范层面的验证。GRAFCET包含不同元素，可导致并发行为，这通常会产生庞大的状态空间。为获得精确结果并缩减状态空间，我们提出一种适用于无并发行为的GRAFCET实例的分析方法。本文阐述了如何检测并发性的缺失，并针对此类GRAFCET实例提出一种流敏感分析。该方法在工业规模实例上进行了评估。