Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0003-2936-4185
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering.ORCID iD: 0000-0002-7001-3435
Computer Science Department, Penza State University, Penza, Penza State University.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0002-9315-9920
2015 (English)In: Technological Innovation for Cloud-Based Engineering Systems: 6th IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems, DoCEIS 2015, Costa de Caparica, Portugal, April 13-15, 2015, Proceedings / [ed] Luis M. Camarinha-Matos ; Thais A. Baldissera ; Giovanni Di Orio; Francisco Marques, Encyclopedia of Global Archaeology/Springer Verlag, 2015, p. 73-81Conference paper, Published paper (Refereed)
Abstract [en]

In this paper we address practical aspects of applying the model-checking method for industrial automation systems verification. Several measures are proposed to cope with the high computational complexity of model-checking. To improve scalability of the method, cloud-based verification tools infrastructure is used. Besides, closed-loop plant controller modelling and synchronization of transitions in the SMV (input language for symbolic model checking) model aim at complexity reduction. The state explosion problem is additionally dealt with by using an abstraction of the model of the plant with net-condition event systems, which is then translated to SMV. In addition, bounded model-checking is applied, which helps to achieve results in cases when the state space is too high. The paper concludes with comparison of performance for different complexity reduction methods

Place, publisher, year, edition, pages
Encyclopedia of Global Archaeology/Springer Verlag, 2015. p. 73-81
Series
IFIP AICT - Advances in Information and Communication technology, ISSN 1868-4238 ; 450
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-27186DOI: 10.1007/978-3-319-16766-4_8Local ID: 088264c1-5bc4-4c29-94c9-3202f012e9c2ISBN: 978-3-319-16765-7 (print)ISBN: 978-3-319-16766-4 (electronic)OAI: oai:DiVA.org:ltu-27186DiVA, id: diva2:1000368
Conference
IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems : 13/04/2015 - 15/04/2015
Note
Validerad; 2015; Nivå 1; 20150408 (andbra)Available from: 2016-09-30 Created: 2016-09-30 Last updated: 2018-04-03Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Patil, SandeepDrozdov, DmitriiVyatkin, Valeriy
By organisation
Computer ScienceDepartment of Computer Science, Electrical and Space Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 70 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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