|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Lulea Tekniska Universitet (SWEDEN),
Aalto University (FINLAND),
and
INRIA Grenoble / CONVECS team (FRANCE)
|
|---|---|
| Method: |
LNT
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Industrial Manufacturing Systems.
|
| Period: |
2024
|
| Size: |
n/a
|
| Description: |
The ever-increasing complexity of industrial automation systems
generates a demand for reliable development methods. IEC 61499 is a
recent standard devoted to the development of industrial automation
systems by promoting reusability, reconfigurability, interoperability,
and portability. Formal verification techniques, such as model
checking, are useful to ensure the correctness of IEC 61499
applications at design time. However, they do not consider the impact
of the environment on the application behaviour at runtime.
This work combines design time and runtime analyses to apply probabilistic model checking on an IEC 61499-based manufacturing application, namely a turntable for drilling products. The approach used (see http://cadp.inria.fr/software/22-a-probabilistic-iiot.html ) consists of several steps: (1) translation of the application into an LNT specification; (2) compilation of the LNT specification into an LTS model; (3) integration of a monitoring function block into the application; (4) execution of the application and generation of traces; (5) computation of a PTS (Probabilistic Transition System) from the LTS and the traces; (6) model checking a probabilistic property, expressed as an MCL formula, on the PTS using CADP. Several probabilistic properties were identified and checked on the manufacturing application. The results obtained were visualised graphically for analysis purposes, enabling the optimisation of the system's quantitative features, such as productivity. |
| Conclusions: |
The results of probabilistic model checking, visualised using charts,
are helpful for analysing the impact of the environment (i.e.,
strategies of interacting with the system) on performance. This enables
to compare various strategies and also to propose new, more productive
ones.
|
| Publications: |
[Faqrizal-Liakh-Xavier-et-al-24]
Irman Faqrizal, Tatiana Liakh, Midhun Xavier, Gwen Salaün, and
Valeriy Vyatkin. "Probabilistic Model Checking for IEC 61499:
A Manufacturing Application". Proc. of the 25th IEEE International
Conference on Industrial Technology (ICIT'2024), Bristol, UK,
March 25-27, 2024.
Available on-line at: https://inria.hal.science/hal-04533520/en [Faqrizal-24] Irman Faqrizal. "Quantitative Verification and Runtime Techniques for Industrial Automation Systems". PhD Thesis, Univ. Grenoble Alpes, December 2024. Available on-line at: https://theses.hal.science/tel-04998327/en |
| Contact: | Gwen Salaün INRIA Centre of University Grenoble Alpes 655, avenue de l'Europe F-38330 Montbonnot Saint Martin FRANCE Email: gwen.salaun@inria.fr |
| Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page