Probabilistic Analysis of Industrial IoT Applications

Organisation:	Inria center of University Grenoble Alpes and LIG (FRANCE)
Functionality:	Functional and quantitative analysis of IIoT applications.
Tools used:	4DIAC-IDE CADP (Construction and Analysis of Distributed Processes)
Period:	2022
Description:	The IEC (International Electrotechnical Commission) 61499 is a recent standard for developing industrial automation. This standard conceptualises interconnected FBs (Function Blocks) to express industrial processes. Each FB encapsulates some logic describing its behaviour, while the connections with other FBs are defined using input and output interfaces. The main benefit of IEC 61499 is that it is suitable for developing a fully distributed system. However, this advantage also raises a challenge, because when the system is complex and composed of many control devices and FBs, it becomes error-prone. Ultimately, verifying the correctness of an IEC 61499 application is not straightforward, since the standard has loosely defined semantics. This work proposes to combine design time and runtime analyses to verify industrial IoT applications described with the IEC 61499 framework. Firstly, at design time, all possible executions of the application under verification are captured using an LTS (Labelled Transition System) model, obtained by translating the IEC 61499 application into an LNT specification and using the CADP compilers. Next, the application is instrumented by inserting a monitor as a FB, which allows to execute a monitored version of the verified system with the existing IEC 61499 runtime environments. Once the application executes, the monitor can observe and store the execution traces of this application. Then, the generated LTS model is enriched with the probabilistic values computed from these executions, resulting in a PTS (Probabilistic Transition System). Finally, probabilistic model checking is used to verify quantitative requirements of the system by invoking the EVALUATOR 5.0 model checker of CADP on the PTS. The approach is illustrated on a capping station described in IEC 61499.
Conclusions:	The proposed approach combines design time and runtime analyses for computing a model of an industrial IoT application described with the IEC 61499 framework. The approach is particularly useful in observing how the environment of industrial applications can influence the truth values of probabilistic properties.
Publications:	[Falcone-Faqrizal-Salaun-22-b] Yliès Falcone, Irman Faqrizal, and Gwen Salaün. "Probabilistic Analysis of Industrial IoT Applications". Proc. of the 12th International Conference on the Internet of Things (IoT'2022), Delft, The Netherlands, pp. 41-48. ACM, November 2022. Available on-line at: http://hal.inria.fr/hal-03848674/en or from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün Inria center of University Grenoble Alpes / CONVECS team 655, avenue de l'Europe F-30330 Montbonnot Saint Martin FRANCE Email: gwen.salaun@inria.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page