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

Formal verification of PLC controlled systems using sensor graphs

Tord Alenljung (Institutionen för signaler och system, Automation) ; Bengt Lennartson (Institutionen för signaler och system, Automation)
2009 IEEE Conference on Automation Science and Engineering, CASE 2009, Bangalore, India p. 164-170. (2009)
[Konferensbidrag, refereegranskat]

This paper describes how a system, consisting of a discrete controller (e.g. a PLC) that controls a physical plant/process, can be formally verified. The physical process is assumed to be modeled using Sensor Graphs, a discrete event modeling language directed at physical systems with binary and identity sensors (e.g. RFID). The formal and graphical syntaxes of Sensor Graphs are presented and exemplified. The "semitimed" semantics is defined considering a process model together with a controller model, represented as a discrete state equation. Finally, it is shown how requirements on the closedloop system, represented by a Sensor Graph and a controller model, can be verified using the model checker Cadence SMV.


Article number 5234187



Denna post skapades 2010-01-18. Senast ändrad 2016-08-16.
CPL Pubid: 108776

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för signaler och system, Automation

Ämnesområden

Elektroteknik och elektronik

Chalmers infrastruktur