Specifying and Verifying PLC Systems with TLA+

In this paper, we developed a format for the specification of PLC systems using the specification language TLA+. Correctness properties for TLA+ specifications can be verified using the TLC model checker. The format we propose clearly distinguishes between user actions, system actions, and plant feedback. The different categories of actions are specified separately by TLA+ action formulas, which are then composed to form the overall specification. This separation makes us confident that we avoided overspecification, in particular of the environment. Working in a high-level language such as TLA+ allows a designer to focus on the essential features of a system specification. It also helps to avoid low-level encodings, which combined with parameterization leads to configurable and concise specifications. The resulting models can nevertheless be analyzed by the TLA+ model checker in a reasonable amount of time.