There are three levels of control in vacuum control system. The bottom level control is performed on the local instruments manually; the medium level control is based on Siemens S7-400 PLC; the top level control is conducted on IPCs with communication through profi_bus network. In addition remote handling and centralized monitoring could be realized by a remote control server.
Specifying and verifying PLC systems with TLA+ : A case study
PLC工作测试系统:案例研究
Abstract
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 +

