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
Towards formal verification for cyber-physically agnostic software: A case study
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0002-7001-3435
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0003-2936-4185
Penza State University.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Aalto University, Helsinki.ORCID iD: 0000-0002-9315-9920
2017 (English)In: Proceedings IECON 2017: 43rd Annual Conference of the IEEE Industrial Electronics Society, Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017, p. 5509-5514Conference paper, Published paper (Refereed)
Abstract [en]

Cyber-physical agnosticism (CPA) is a property of software in cyber-physical systems (CPS) to withstand various disturbances and keep maintaining the required behaviour of the physical process. With the increased research on the use of internet of things (IoT) in industrial automation (IoT-A), there is a need for robust distributed automation control systems that can take into account some overheads of using wireless devices in such an IoT setup. For example, data transfer delays between wireless sensors and the controller might result in the controller acting on a stale sensor value. In this paper, we present an approach of using time-aware computations to let the controller to assess quality of the input data and formal verification as a method to check the CPA property of the IoT-A applications. The paper specifically considers IEC 61499 standard for implementation of distributed IoT-A application. Ptolemy II PTIDES inspired time stamped event semantics is used in the application to keep track of the origin of different events. Timed automata are used to model the plant. The IEC 61499 application together with abstract plant model is then converted to SMV language and NuSMV model checker is used for formal verification. The paper presents a case study of an elevator example to demonstrate the proposed approach. A random delay is used to model the communication delay in the wireless network. It is shown that if the communication delay was not accounted for, then the elevator would stop in-between the floors and open the doors that is considered unsafe. The paper then shows how time-aware computation is used to make sure that the elevator always follows safe behaviour.

Place, publisher, year, edition, pages
Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017. p. 5509-5514
Series
IEEE Industrial Electronics Society, ISSN 1553-572X
National Category
Computer Systems
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-68177DOI: 10.1109/IECON.2017.8216953ISI: 000427164805072Scopus ID: 2-s2.0-85046663009ISBN: 9781538611272 (electronic)OAI: oai:DiVA.org:ltu-68177DiVA, id: diva2:1195318
Conference
43rd Annual Conference of the IEEE Industrial Electronics Society, IECON 2017, Bejing, China, 29 October - 1 November 2017
Available from: 2018-04-05 Created: 2018-04-05 Last updated: 2018-05-21Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Drozdov, DmitriiPatil, SandeepVyatkin, Valeriy
By organisation
Computer Science
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 8 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