mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Applying REMES behavioral modeling to PLC systems
Mälardalen University, School of Innovation, Design and Engineering. (Industrial Software Engineering)ORCID iD: 0000-0003-2383-7981
Mälardalen University, School of Innovation, Design and Engineering. (Real-Time Systems Modelling and Analysis)ORCID iD: 0000-0001-5293-3804
2009 (English)In: 2009 XXII INTERNATIONAL SYMPOSIUM ON INFORMATION, COMMUNICATION AND AUTOMATION TECHNOLOGIES, IEEE , 2009, 98-105 p.Conference paper, Published paper (Refereed)
Abstract [en]

Abstract—Programmable logic controllers (PLCs), as aspecialized type of embedded systems, have been introduced toincrease system flexibility and reliability, but at the same time togive faster response time and lower cost of implementation. Inthe beginning, their use brought a revolutionary change, but withthe constant growth of system complexity, it became harder toguarantee both functional and extra functional properties, asearly as possible in the development process. In this paper, weshow how formal methods can be applied to describe PLC-basedsystems and illustrate it on an example of a car wash system.First, we show how the existing behavioral modeling languageREMES (REsource Model for Embedded Systems) can beextended to model the behavior of such systems. Second, we showhow REMES can be translated into networks of timed automataand priced timed automata in order to support safety andresource-wise reasoning about PLC systems. The formalverification of PLC systems is carried out in the UPPAAL andUPPAAL CORA tools.

Place, publisher, year, edition, pages
IEEE , 2009. 98-105 p.
Keyword [en]
behavioral model; model checking; PLC systems; timed automata; priced timed automata
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-7569DOI: 10.1109/ICAT.2009.5348453ISI: 000283478400015Scopus ID: 2-s2.0-74549199480ISBN: 978-1-4244-4221-8 (print)OAI: oai:DiVA.org:mdh-7569DiVA: diva2:278313
Conference
22nd International Symposium on Information Communication and Automation Technologies Location: Sarajevo, BOSNIA & HERCEG Date: OCT 29-31, 2009
Projects
ProgressQ-Impress
Available from: 2009-11-27 Created: 2009-11-25 Last updated: 2013-12-19Bibliographically approved

Open Access in DiVA

fulltext(1302 kB)540 downloads
File information
File name FULLTEXT01.pdfFile size 1302 kBChecksum SHA-512
e3a70aa6ce568abe578601a511643ee36a09bfdbd84b914ffebd77e96efcaab599c6a6b020c125ad2b7f5ff911ef9e20b0386eaf412200f4268e4b7533ecaf4d
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Vulgarakis, AnetaCausevic, Aida
By organisation
School of Innovation, Design and Engineering
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 540 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 55 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf