Sökning: onr:"swepub:oai:research.chalmers.se:fbc2bf56-3efe-4689-8000-131144079e97" >
Sensor Graphs for D...
Sensor Graphs for Discrete Event Modeling Applied to Formal Verification of PLCs
-
- Alenljung, Tord, 1977 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Lennartson, Bengt, 1956 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Noori-Hosseini, Mona, 1982 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- Institute of Electrical and Electronics Engineers (IEEE), 2012
- 2012
- Engelska.
-
Ingår i: IEEE Transactions on Control Systems Technology. - : Institute of Electrical and Electronics Engineers (IEEE). - 1063-6536 .- 1558-0865. ; 20:6, s. 1506-1521
- Relaterad länk:
-
http://dx.doi.org/10...
-
visa fler...
-
https://doi.org/10.1...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- logic control
- failure diagnosis
- petri nets
- process modeling
- validation
- modeling languages
- Discrete event systems
- formal verification
- programs
- systems
- controller
- framework
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas