Information Technology Reference
In-Depth Information
of PLCs is simple due to its use in safety-critical systems, well structured,
and extensively documented. The use of a SSA form enables to come up with
invariants, which are, for example, only valid after the last iteration of a loop
during a PLC cycle as in the case of
from_byte
variable. This is especially
helpful in PLC programs as the values of variables are only visible after the
execution of a complete cycle and not during the cycle.
As shown by our examples, the approach delivers invariants that capture
the behavior of programs in a way easily accessible by users. Additionally,
the examples show that the approach also scales well for larger programs.
There are several directions for future improvement. First, not all proper-
ties can be expressed using invariants and it is therefore useful to investigate
whether the same approach can be used to automatically generate properties
using a more complex logic. Furthermore, users want to check whether their
properties are satisfied by the program. This can be achieved by checking
whether their invariants are entailed by the invariants generated by our ap-
proach. If the user-provided invariants are satisfied, it could be useful to also
provide information about the additional properties which are satisfied by
the program but not specified by the users. This process could be supported
by a graphical representation of the invariants.
References
1. M.BaniYounisandG.Frey. FormalizationofexistingPLCprograms:Asurvey.
In
CESA
, 2003.
2. L. Baresi, M. Mauri, A. Monti, and M. Pezze. PLCTools: Design, formal vali-
dation, and code generation for programmable logic controllers. In
SMC
, pages
2437-2442, 2000.
3. S. Bornot, R. Huuck, B. Lukoschus, and Y. Lakhnech. Utilizing static analysis
for programmable logic controllers. In
ADPM
, pages 183-187, 2000.
4. A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri,
R. Sebastiani, and A. Tacchella. NuSMV version 2: An opensource tool for
symbolic model checking. In
CAV (2002)
, volume 2404 of
LNCS
, pages 241-
268. Springer, 2002.
5. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Ef-
fciently computing static single assignment form and the control dependence
graph.
ACM Trans. Program. Lang. Syst.
, pages 451-590, 1991.
6. E. A. Emerson.
Handbook of Theoretical Computer Science
, volume B, chapter
Temporal and Modal Logics, pages 995-1072. The MIT Press, 1991.
7. C. A. R. Hoare. An axiomatic basis for computer programming.
Comm. of the
ACM
, 12(10):576-585.
8. R. Huuck.
Software Verification for Programmable Logic Controllers
. Disser-
tation, University of Kiel, Germany, April 2003.
9. International Electrotechnical Commission.
IEC 61131-3 Ed. 1.0: Pro-
grammable Controllers — Part 3: Programming languages
. International Elec-
trotechnical Commission, Geneva, Switzerland, 1993.
10. International Electrotechnical Commission.
IEC 61508: Functional Safety of
Electrical, Electronic and Programmable Electronic Safety-Related Systems
.In-
ternational Electrotechnical Commission, Geneva, Switzerland, 1998.
