GF_LL_SMC2000_oct_2000

Frey,G.; Litz, L.:
Formal methods in PLC programming
Proceedings of the IEEE SMC 2000, Nashville, October 08-11, 2000, pp. 2431-2436.

A detailed generic model of the control design process is introduced and discussed. It is used for surveying different formal approaches in the context of PLC-programming. The survey focuses on formal methods for verification and validation (V&V). The varying works in this area are categorized using three criteria: the general Approach to the task (model based, constrained based or without a model), the Formalism (Petri net, automata,...) used to state the formal description, and the Method (Model-Checking, Reachability Analysis, ...) used to analyze the properties. Based on these three criteria (A-F-M) a three letter code for V&V approaches is introduced. Some works from the multitude of V&V research are presented and categorized using this new system.