Below is the survey result of comparing PLC on Instruction List (IL) with the criteria and see what tools are available to support verification. This survey does not in any sense pretend to be completed, but hopefully useful as a guide to presents approaches.
• In a timed automation semantics is given to Instruction List. The fragment language does not consist function and Function Block calls. Timers, i.e. of type TON, can be modeled. The scan cycle is modeled explicitly, with upper and lower time bound. Based on this work a tool was developed. It translates IL programs to automata of timed. The IL programs considered to allow integers as variable types.
• In the class models used in condition/event systems. The programs that can be modeled are in an Instruction List fragment without jumps. The types of data are restricted to Booleans. The three type’s timers can be modeled, under the assumption that timers are started only at the beginning of a program, resulting in a model. The verification of the whole system can be done with help of the VERDICT tool. VERDICT provides an interface to available verification tools, such as HyTech, KRONOS and SMV.
• In a fragment programs of Instruction List are modeled by Petri Nets. The fragment includes of the standard set of instructions without commands from libraries. Possible structures of data are what are expressible within an 8-bit word. The cyclic execution mode of the program is modeled in the way of the Petri Nets representing the program and environment are composed into one net.
• The deals with program of Instruction List. The models are Net Condition or Event system extended by time. There is an explicit scan cycle considered with upper and lower time bounds. The data structure available seems to Booleans. Instruction execution is modeled by a transitions sequence, which suggests that branching is not considered which should not at all be a problem in this modeling way.