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: [email protected] |
Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |