CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Tord Alenljung (Institutionen för signaler och system, Automation) ; Bengt Lennartson (Institutionen för signaler och system, Automation) ; Mona Noori Hosseini (Institutionen för signaler och system, Automation)
IEEE Transactions on Control Systems Technology (1063-6536). Vol. 20 (2012), 6, p. 1506-1521.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: Discrete event systems, formal verification, logic control, modeling languages, process modeling, failure diagnosis, petri nets, systems, validation, controller, framework, programs



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2012-10-29. Senast ändrad 2013-01-16.
CPL Pubid: 165184

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för signaler och system, Automation

Ämnesområden

Produktion
Data- och informationsvetenskap

Chalmers infrastruktur