Formal methods in PLC programming 论文

详细信息

发表日期

2002-11-08

发表年份

2002

摘要

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 (A) to the task (model based, constraint based or without a model), the formalism (F) (Petri net, automata, etc.,) used to state the formal description, and the method (M) (model-checking, reachability analysis, etc.,) 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.