Paper Info
Title
Sensor Graphs for Discrete Event Modeling Applied to Formal Verification of PLCs.
Abstract
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.
Year
DOI
Venue
2012
10.1109/TCST.2011.2168607
IEEE Trans. Contr. Sys. Techn.
Keywords
DocType
Volume
Discrete event systems,Formal verification,Process control,Sensors,Programmable logic devices
Journal
20
Issue
ISSN
Citations 
6
1063-6536
7
PageRank 
References 
Authors
0.47
23
3
Name
Order
Citations
PageRank
Tord Alenljung1152.35
Bengt Lennartson2934118.87
Mona Noori Hosseini3284.85