IEEE Control Systems · 1994 · 115 citations · 6 references
EngineeringComputer EngineeringComputer ScienceFormal MethodsSafety EngineeringSystems ModelingAssertion-based VerificationDeductive VerificationModel CheckingProgrammable Logic ControllersTemporal LogicVerificationPlc Programming LanguagesProgrammable Logic DesignSafety Programmable Logic ControllersSequential Logic DesignState Space ExplorationState-space StructureTemporal Logic AssertionsTemporal Logic Verification
Verification method has been developed for determining the safety and operability of programmable logic controller (PLC) based systems. The method automatically checks sequential logic embedded in PLCs and provides counterexamples if it finds errors. The method consists of a system model, assertions, and a model checker. The model is a Boolean-based representation of a PLC's behavior. Assertions are questions about the behavior of the system, expressed in temporal logic. The model checker generates a state space based on the above two inputs, searches the space efficiently, determines the consistency of the model and assertions, and supplies counterexamples. A modeling technique has been developed to verify relay ladder logic (RLL), a PLC programming language. The performance of the model checker is studied in a series of alarm designs.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
6
Symbolic model checking: 1020 States and beyond
Jerry R. Burch, E. M. Clarke, Kenneth L. McMillan et al. · Information and Computation · 1992 · 2.7K citations
Automatic verification of sequential control systems using temporal logic
Il Moon, Gary J. Powers, Jerry R. Burch et al. · AIChE Journal · 1992 · 91 citations · Full text
Design recovery for relay ladder logic
A. Falcione, Bruce H. Krogh · IEEE Control Systems · 1993 · 79 citations