Specifying and verifying PLC systems with TLA+ : A case study

We report on a method for formally specifying and verifying programmable logic controllers (PLCs) in the specification language TLA+. The specification framework is generic. It separates the description of the environment from that of the controller itself and its structure is consistent with the scan cycle mechanism used by PLCs. Specifications can be parameterized with the number of replicated components. In our experience, the structuring mechanisms of TLA+ help to obtain clear, well-organized, and configurable specifications, finite instances of which are verified by the TLA+ model checker TLC. We have validated our approach on a concrete case study, a controller for fire fighting equipment in a ship dock, and report on the results obtained for this case study.