Towards formal verification for cyber-physically agnostic software: A case study

Dmitrii Drozdov*, Sandeep Patil, Victor Dubinin, Valeriy Vyatkin

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

6 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 43rd Annual Conference of the IEEE Industrial Electronics Society, IECON 2017
PublisherIEEE
Pages5509-5514
Number of pages6
Volume2017-January
ISBN (Electronic)9781538611272
DOIs
Publication statusPublished - 15 Dec 2017
MoE publication typeA4 Article in a conference publication
EventAnnual Conference of the IEEE Industrial Electronics Society - Beijing, China
Duration: 29 Oct 20171 Nov 2017
Conference number: 43
http://iecon2017.csp.escience.cn/

Publication series

NameProceedings of the Annual Conference of the IEEE Industrial Electronics Society
PublisherIEEE
ISSN (Print)1553-572X

Conference

ConferenceAnnual Conference of the IEEE Industrial Electronics Society
Abbreviated titleIECON
CountryChina
CityBeijing
Period29/10/201701/11/2017
Internet address

Keywords

  • cyber-physical agnosticism
  • distributed automation systems
  • IEC 61499
  • model checking
  • time-aware computations
  • timestamp

Fingerprint Dive into the research topics of 'Towards formal verification for cyber-physically agnostic software: A case study'. Together they form a unique fingerprint.

Cite this