mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Applying REMES behavioral modeling to PLC systems
Mälardalens högskola, Akademin för innovation, design och teknik. (Industrial Software Engineering)ORCID-id: 0000-0003-2383-7981
Mälardalens högskola, Akademin för innovation, design och teknik. (Real-Time Systems Modelling and Analysis)ORCID-id: 0000-0001-5293-3804
2009 (Engelska)Ingår i: 2009 XXII INTERNATIONAL SYMPOSIUM ON INFORMATION, COMMUNICATION AND AUTOMATION TECHNOLOGIES, IEEE , 2009, s. 98-105Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
IEEE , 2009. s. 98-105
Nyckelord [en]
behavioral model; model checking; PLC systems; timed automata; priced timed automata
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
datavetenskap
Identifikatorer
URN: urn:nbn:se:mdh:diva-7569DOI: 10.1109/ICAT.2009.5348453ISI: 000283478400015Scopus ID: 2-s2.0-74549199480ISBN: 978-1-4244-4221-8 (tryckt)OAI: oai:DiVA.org:mdh-7569DiVA, id: diva2:278313
Konferens
22nd International Symposium on Information Communication and Automation Technologies Location: Sarajevo, BOSNIA & HERCEG Date: OCT 29-31, 2009
Projekt
ProgressQ-ImpressTillgänglig från: 2009-11-27 Skapad: 2009-11-25 Senast uppdaterad: 2018-01-12Bibliografiskt granskad

Open Access i DiVA

fulltext(1302 kB)642 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 1302 kBChecksumma SHA-512
e3a70aa6ce568abe578601a511643ee36a09bfdbd84b914ffebd77e96efcaab599c6a6b020c125ad2b7f5ff911ef9e20b0386eaf412200f4268e4b7533ecaf4d
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Vulgarakis, AnetaCausevic, Aida

Sök vidare i DiVA

Av författaren/redaktören
Vulgarakis, AnetaCausevic, Aida
Av organisationen
Akademin för innovation, design och teknik
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 642 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 106 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf