Sensor Graphs for Discrete Event Modeling Applied to Formal Verification of PLCs

• This paper introduces Sensor Graphs, a discrete event modeling language directed at physical systems with binary and identity sensors (e. g., RFID). The aim of Sensor Graphs is to simplify the modeling of the plant/process that is to be controlled by a discrete controller, for example a programmable logic controller (PLC); thereby making formal verification and other model-based formal methods more applicable for PLC programmers. The formal syntax and semantics of Sensor Graphs are defined and a compact graphical representation is presented. The language is exemplified by modeling a conveyor module and a lab process. For comparison, the latter is also modeled using Statecharts and Net Condition/Event systems. A controller, modeled as a discrete state equation, can be composed with a Sensor Graph of the process in order to form a model of the closed-loop system. It is demonstrated how requirements on such a closed-loop system, based on a PLC program and a Sensor Graph process model, can be formally verified using the model checker Cadence SMV.

Subject headings

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Keyword

logic control

failure diagnosis

petri nets

process modeling

validation

modeling languages

Discrete event systems

formal verification

programs

systems

controller

framework

Publication and Content Type

art (subject category)

ref (subject category)