Specifying and verifying PLC systems with TLAC: A case studyI

We report on a method for formally specifying and verifying programmable logic controllers (PLCs) in the specification language TLAC. 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 TLAC help to obtain clear, well-organized, and configurable specifications, finite instances of which are verified by the TLAC 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.