Loading…
Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs
As a complement to testing procedures, verification techniques as e.g. model checking have been proposed to analyze logic controllers specified as sequential function charts (SFC). For the success of these techniques suitable execution models of the SFC and of the programmable logic controllers (PLC...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Conference Proceeding |
| Language: | English |
| Subjects: | |
| Online Access: | Request full text |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| cited_by | |
|---|---|
| cites | |
| container_end_page | 3611 |
| container_issue | |
| container_start_page | 3606 |
| container_title | |
| container_volume | |
| creator | Lohmann, S. Stursberg, O. Engell, S. |
| description | As a complement to testing procedures, verification techniques as e.g. model checking have been proposed to analyze logic controllers specified as sequential function charts (SFC). For the success of these techniques suitable execution models of the SFC and of the programmable logic controllers (PLC) on which the SFC are implemented and operated in practice are crucial. This paper investigates and compares two different suggested transformation schemes for mapping SFC into timed automata (TA): an event-triggered and a cycle driven scheme. For the example of a laboratory experiment, the paper shows how the schemes lead to TA models of the controller which can, when complemented with appropriate plant models, be used for verifying properties as e.g. safety by employing the software tool UPPAAL. The event-triggered transformation scheme is found to lead to considerably smaller TA models and hence to be more suitable for verification purposes. |
| doi_str_mv | 10.1109/ACC.2007.4282937 |
| format | conference_proceeding |
| fullrecord | <record><control><sourceid>ieee_CHZPO</sourceid><recordid>TN_cdi_ieee_primary_4282937</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>4282937</ieee_id><sourcerecordid>4282937</sourcerecordid><originalsourceid>FETCH-LOGICAL-i90t-469bfd911f4eb46a288afd6e9c52f462800bd7a53e98c9657a37a226d5cb96223</originalsourceid><addsrcrecordid>eNo1kMtKAzEUQOMLbGv3gpv8QGpek-QuS2xVqFiwuC2Zyc0QaWdKpgj9ewXr6iwOnMUh5F7wmRAcHufezyTndqalk6DsBRkLLbXm4MBckpFU1rHKGXFFpmDdv3P6moy41YoJI-CWjIfhi3MBYPiIrH2_P4SSh76jfaKLb-yObFNy22LBSEMXqT81O2RPJf86-tZH3A009YV-YsnplLuWfiw9XZe-LWE_3JGbFHYDTs-ckM1ysfEvbPX-_OrnK5aBH5k2UKcIQiSNtTZBOhdSNAhNJZM20nFeRxsqheAaMJUNygYpTayaGoyUakIe_rIZEbeHkvehnLbnMeoHB5hR-w</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs</title><source>IEEE Xplore All Conference Series</source><creator>Lohmann, S. ; Stursberg, O. ; Engell, S.</creator><creatorcontrib>Lohmann, S. ; Stursberg, O. ; Engell, S.</creatorcontrib><description>As a complement to testing procedures, verification techniques as e.g. model checking have been proposed to analyze logic controllers specified as sequential function charts (SFC). For the success of these techniques suitable execution models of the SFC and of the programmable logic controllers (PLC) on which the SFC are implemented and operated in practice are crucial. This paper investigates and compares two different suggested transformation schemes for mapping SFC into timed automata (TA): an event-triggered and a cycle driven scheme. For the example of a laboratory experiment, the paper shows how the schemes lead to TA models of the controller which can, when complemented with appropriate plant models, be used for verifying properties as e.g. safety by employing the software tool UPPAAL. The event-triggered transformation scheme is found to lead to considerably smaller TA models and hence to be more suitable for verification purposes.</description><identifier>ISSN: 0743-1619</identifier><identifier>ISBN: 9781424409884</identifier><identifier>ISBN: 1424409888</identifier><identifier>EISSN: 2378-5861</identifier><identifier>EISBN: 1424409896</identifier><identifier>EISBN: 9781424409891</identifier><identifier>DOI: 10.1109/ACC.2007.4282937</identifier><language>eng</language><publisher>IEEE</publisher><subject>Automata ; Automatic control ; Computer languages ; Cooling ; IEC standards ; Laboratories ; Logic programming ; Logic testing ; Programmable control ; Safety</subject><ispartof>2007 American Control Conference, 2007, p.3606-3611</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/4282937$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,780,784,789,790,2058,27925,54555,54920,54932</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/4282937$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Lohmann, S.</creatorcontrib><creatorcontrib>Stursberg, O.</creatorcontrib><creatorcontrib>Engell, S.</creatorcontrib><title>Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs</title><title>2007 American Control Conference</title><addtitle>ACC</addtitle><description>As a complement to testing procedures, verification techniques as e.g. model checking have been proposed to analyze logic controllers specified as sequential function charts (SFC). For the success of these techniques suitable execution models of the SFC and of the programmable logic controllers (PLC) on which the SFC are implemented and operated in practice are crucial. This paper investigates and compares two different suggested transformation schemes for mapping SFC into timed automata (TA): an event-triggered and a cycle driven scheme. For the example of a laboratory experiment, the paper shows how the schemes lead to TA models of the controller which can, when complemented with appropriate plant models, be used for verifying properties as e.g. safety by employing the software tool UPPAAL. The event-triggered transformation scheme is found to lead to considerably smaller TA models and hence to be more suitable for verification purposes.</description><subject>Automata</subject><subject>Automatic control</subject><subject>Computer languages</subject><subject>Cooling</subject><subject>IEC standards</subject><subject>Laboratories</subject><subject>Logic programming</subject><subject>Logic testing</subject><subject>Programmable control</subject><subject>Safety</subject><issn>0743-1619</issn><issn>2378-5861</issn><isbn>9781424409884</isbn><isbn>1424409888</isbn><isbn>1424409896</isbn><isbn>9781424409891</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2007</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNo1kMtKAzEUQOMLbGv3gpv8QGpek-QuS2xVqFiwuC2Zyc0QaWdKpgj9ewXr6iwOnMUh5F7wmRAcHufezyTndqalk6DsBRkLLbXm4MBckpFU1rHKGXFFpmDdv3P6moy41YoJI-CWjIfhi3MBYPiIrH2_P4SSh76jfaKLb-yObFNy22LBSEMXqT81O2RPJf86-tZH3A009YV-YsnplLuWfiw9XZe-LWE_3JGbFHYDTs-ckM1ysfEvbPX-_OrnK5aBH5k2UKcIQiSNtTZBOhdSNAhNJZM20nFeRxsqheAaMJUNygYpTayaGoyUakIe_rIZEbeHkvehnLbnMeoHB5hR-w</recordid><startdate>200707</startdate><enddate>200707</enddate><creator>Lohmann, S.</creator><creator>Stursberg, O.</creator><creator>Engell, S.</creator><general>IEEE</general><scope>6IE</scope><scope>6IH</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIO</scope></search><sort><creationdate>200707</creationdate><title>Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs</title><author>Lohmann, S. ; Stursberg, O. ; Engell, S.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i90t-469bfd911f4eb46a288afd6e9c52f462800bd7a53e98c9657a37a226d5cb96223</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2007</creationdate><topic>Automata</topic><topic>Automatic control</topic><topic>Computer languages</topic><topic>Cooling</topic><topic>IEC standards</topic><topic>Laboratories</topic><topic>Logic programming</topic><topic>Logic testing</topic><topic>Programmable control</topic><topic>Safety</topic><toplevel>online_resources</toplevel><creatorcontrib>Lohmann, S.</creatorcontrib><creatorcontrib>Stursberg, O.</creatorcontrib><creatorcontrib>Engell, S.</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan (POP) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE/IET Electronic Library (IEL)</collection><collection>IEEE Proceedings Order Plans (POP) 1998-present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Lohmann, S.</au><au>Stursberg, O.</au><au>Engell, S.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs</atitle><btitle>2007 American Control Conference</btitle><stitle>ACC</stitle><date>2007-07</date><risdate>2007</risdate><spage>3606</spage><epage>3611</epage><pages>3606-3611</pages><issn>0743-1619</issn><eissn>2378-5861</eissn><isbn>9781424409884</isbn><isbn>1424409888</isbn><eisbn>1424409896</eisbn><eisbn>9781424409891</eisbn><abstract>As a complement to testing procedures, verification techniques as e.g. model checking have been proposed to analyze logic controllers specified as sequential function charts (SFC). For the success of these techniques suitable execution models of the SFC and of the programmable logic controllers (PLC) on which the SFC are implemented and operated in practice are crucial. This paper investigates and compares two different suggested transformation schemes for mapping SFC into timed automata (TA): an event-triggered and a cycle driven scheme. For the example of a laboratory experiment, the paper shows how the schemes lead to TA models of the controller which can, when complemented with appropriate plant models, be used for verifying properties as e.g. safety by employing the software tool UPPAAL. The event-triggered transformation scheme is found to lead to considerably smaller TA models and hence to be more suitable for verification purposes.</abstract><pub>IEEE</pub><doi>10.1109/ACC.2007.4282937</doi><tpages>6</tpages></addata></record> |
| fulltext | fulltext_linktorsrc |
| identifier | ISSN: 0743-1619 |
| ispartof | 2007 American Control Conference, 2007, p.3606-3611 |
| issn | 0743-1619 2378-5861 |
| language | eng |
| recordid | cdi_ieee_primary_4282937 |
| source | IEEE Xplore All Conference Series |
| subjects | Automata Automatic control Computer languages Cooling IEC standards Laboratories Logic programming Logic testing Programmable control Safety |
| title | Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs |
| url | http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-01T11%3A13%3A00IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_CHZPO&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=Comparison%20of%20Event-Triggered%20and%20Cycle-Driven%20Models%20for%20Verifying%20SFC%20Programs&rft.btitle=2007%20American%20Control%20Conference&rft.au=Lohmann,%20S.&rft.date=2007-07&rft.spage=3606&rft.epage=3611&rft.pages=3606-3611&rft.issn=0743-1619&rft.eissn=2378-5861&rft.isbn=9781424409884&rft.isbn_list=1424409888&rft_id=info:doi/10.1109/ACC.2007.4282937&rft.eisbn=1424409896&rft.eisbn_list=9781424409891&rft_dat=%3Cieee_CHZPO%3E4282937%3C/ieee_CHZPO%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i90t-469bfd911f4eb46a288afd6e9c52f462800bd7a53e98c9657a37a226d5cb96223%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=4282937&rfr_iscdi=true |