Software Verification for Programmable Logic Controllers
Ralf Huuck · MACAU: Open Access Repository of Kiel University (University Library Kiel) · 2006
Interpretation . . . . . . . . . . . . 26 2.1.3 Other Approaches . . . . . . . . . . . . . . . . . . . . 27 2.2 PLC Verification . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.2.1 Approaches Based on Instruction List . . . . . . . . . 28 2.2.2 Approaches Based on Sequential Function Charts . . . 29 2.2.3 Approaches Based on Ladder Diagrams . . . . . . . . 30 2.2.4 Miscellaneous Other Approaches . . . . . . . . . . . . 31 2.2.5 Matrix of Surveyed PLC Papers . . . . . . . . . . . . 31 2.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3 Foundations of Software Verification 35 3.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.2.1 Lattices . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.2.2 Complete Partial Orders . . . . . . . . . . . . . . . . . 39 3.2.3 Fixed Points . . . . . . . . . . . . . . . . . . . . . . . 40 3.3 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.3.1 System Model . . . . . . . . . . . . . . . . . . . . . . . 43 3.3.2 Computational Model . . . . . . . . . . . . . . . . . . 46 3.3.3 Temporal Logics . . . . . . . . . . . . . . . . . . . . . 47 3.3.4 Tools and Limitations . . . . . . . . . . . . . . . . . . 49 3.3.5 Complexity Issues . . . . . . . . . . . . . . . . . . . . 50 3.4 Data Flow Analysis . . . . . . . . . . . . . . . . . . . . . . . . 53 3.4.1 Basic Definitions . . . . . . . . . . . . . . . . . . . . . 53 3.4.2 Classical Data Flow Examples . . . . . . . . . . . . . 56 3.4.3 Formal Data Flow Framework . . . . . . . . . . . . . . 61 3.4.4 Iterative Solvers for General Frameworks . . . . . . . 64 3.5 Abstract Interpretation . . . . . . . . . . . . . . . . . . . . . 67 3.5.1 Galois Connections . . . . . . . . . . . . . . . . . . . . 68 3.5.2 Fixed Point Appr...