Towards Formal Verification for Cyber-physically Agnostic Software: a Case Study

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.