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
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: 2021-08-09Bibliographically approved
In thesis
1. Development and Verification of Dependable Software of Cyber-Physical Systems using Time-aware Computations
Open this publication in new window or tab >>Development and Verification of Dependable Software of Cyber-Physical Systems using Time-aware Computations
2021 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Wired and wireless networking is becoming a necessary part of industrial control systems’ design and is one of the reasons that required a new cyber-physical approach to modelling. The phenomenon observed in cyber-physical systems (CPS) is a variety of cross-dependencies and influences between physical processes, computational devices and communications, which needs to be taken into account at the design and verification stage. Since most of the systems' functionality nowadays is implemented via software, the ability of software to be agnostic to the mentioned cross-influences is of high importance. 

This work introduces a concept called time-aware computations (TAC), which, instead of aiming at determinism, that is very expensive in distributed systems, aims at adaptability and robustness. It is based on the event-timestamping mechanism and is intended to let the developer handle each communication delay case individually thus minimizing its impact on functional properties of the automation system. It allows the controller to take into account actual point-to-point delay of the measured sensor readings, and adjust the control reaction accordingly, instead of trying to put the upper bound on it and wait for the maximum possible delay time. 

In industrial automation, the function block architecture of the IEC 61499 standard is increasingly used for modelling complex  distributed  automation  systems. It is  based  on  the  concepts  of  event-driven  block  diagrams, and originally was created as a new programming paradigm for industrial automation controllers, but as a number of recent studies show, it also  allows (and has been used) for  modelling  of CPS  composed of  physical  processes  combined  with  control and communication.

The second major co-contribution of this work is a formal model of IEC 61499-based systems with timestamps that allows for modelling and verification of control logic (and closed-loop models) designed with TAC approach in mind. This would also allow for application of model-driven design methodologies later down the road.

Third contribution is a software tool-chain that aims to greatly reduce the engineering work when applying formal verification to the designed systems.

The proposed contributions' feasibility and effectiveness are demonstrated on a number of case studies.

Place, publisher, year, edition, pages
Luleå: Luleå University of Technology, 2021
Series
Doctoral thesis / Luleå University of Technology 1 jan 1997 → …, ISSN 1402-1544
Keywords
Abstract state machines, CPS, formal semantics, formal verification, IEC 61499, time-aware computations
National Category
Computer Sciences Computer Systems
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-86536 (URN)978-91-7790-900-2 (ISBN)978-91-7790-901-9 (ISBN)
Public defence
2021-09-29, A2527 (remote), Luleå University of Technology, Luleå, 13:00 (English)
Opponent
Supervisors
Funder
Swedish Research Council, 2015-04675EU, Horizon 2020, 723248EU, Horizon 2020, 871743
Available from: 2021-08-11 Created: 2021-08-09 Last updated: 2021-09-08Bibliographically 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: 148 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