Форум АСУ в Україні

форум з автоматизації для викладачів, студентів та спеціалістів
Сьогодні: 12 листопада 2019, 21:41

Часовий пояс UTC + 2 годин [ DST ]




Створити нову тему Відповісти  [ 10 повідомлень ] 
Автор Повідомлення
 Тема повідомлення: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 28 вересня 2014, 11:25 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
A toolset for model checking of PLC software
Pakonen, A. ; VTT Tech. Res. Centre of Finland, Espoo, Finland ; Matasniemi, T. ; Lahtinen, J. ; Karhela, T.
посилання
Цитата:
Model checking is a powerful formal verification method that can also be used to evaluate PLC software. A lot of manual work and some expertise are still needed. Proposed methods for automating the process rely on standardised specification languages, but PLC software is often vendor-specific, and the source code for function blocks may not even be available. We propose a toolset for model checking of function block based software. After manually modelling the elementary function block library, the model of any block diagram can be specified with easy-to-use graphical tools. The counterexamples output by the model checker can also be visualised using a “living” function block diagram. Our toolset is based on integrating the popular model checker NuSMV with the open source modelling platform Simantics.


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software
ПовідомленняДодано: 01 жовтня 2014, 20:18 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Відкритий робочий матеріал(може комусь ще знадобиться).
Стаття про використання одного з підходів верифікації програм Model Checking для програм, написаних на мові FBD.
2.1. Model checking
Розповідається про метод верифікації програм - Model Checking, який описаний viewtopic.php?f=235&t=859
Далі про модель-чекер (опен сорс програма для перевірки) NuSMV viewtopic.php?f=235&t=859

2.2. PLC software verification
Автори використоували метод Model Checking з 2007 року для перевірки програм управління на атомних станціях [3] J. Lahtinen, J. Valkonen, K. Björkman, J. Frits, I. Niemelä, K. Heljanko, ”Model checking of safety-critical software in the nuclear engineering domain”, Reliability Engineering and System Safety, Vol. 105, pp. 104-113, 2012.
Перша проблема в тому, що необхідно провести дуже багато ручної роботи для застосування цього методу в області програм управління, оскільки не існує інтсрументальних засобів. Усі інструменти направлені на перевірку на стандартних мовах.
Друга проблема - це завдання властивостей, які будуть перевірені. Сепцифікація вимог до системи розмита, а для методу повинні бути чіткі специфікації.
Третя проблема - інтерпритація контрприкладів.[4] E. Jee, S. Jeon, S. Cha, K. Koh, J. Yoo, G. Park, P. Seong, “FBDVerifier: Interactive and Visual Analysis of Counter-Example in Formal Verification of Function Block Diagram”, Journal of Research and Practice in Information Technology, Vol. 42, pp. 171-188, 2010. Як правило контрприклади повертаються сотнями рядків що важко інтерпретувати.

3. Related research
Різні автори досліджували використання Моделчекінг для ПЛК:

[5] B. Schlich, J. Brauer, J. Wernerus, S. Kowalewski, “Direct Model Checking of PLC Programs in IL”, 2nd IFAC Workshop on Dependable Control of Discrete Systems, Bari, Italy, June 10-12, 2009.
[6] V. Gourcuff, O. De Smet, J. Faure, “Efficient representation for formal verification of PLC programs”, 8th International Workshop on Discrete Event Systems, Ann Arbor, MI, USA, July 10-12, 2006.
[7] D. Soliman, K. Thramboulidis, G. Frey, “Transformation of Function Block Diagrams to UPPAAL timed automata for the verification of safety applications”, Annual Reviews in Control, Vol. 36, pp. 338-345, 2012.
[8] J. Yoo, S. Cha, E. Jee, “Verification of PLC Programs Written in FBD with VIS”, Nuclear Engineering and Technology, Vol. 41, pp. 79-90, 2009.
[9] R. Huuck, Software Verification for Programmable Logic Controllers, Dissertation, University of Kiel, 2003.
[10] O. Rossi, P. Schnoebelen, “Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs”, The 4th International Conference on Automation of Mixed Processes (ADPM 2000), Dortmund, Germany, Sep 18-19, 2000.
Проблеми:
1) Ці методи базуються на автоматичній трансляції з МЕКовських мов (61131). Але ці мови хоч і стандартизовані, але різні.
2) Передбачається, що реалізація або вихідний код з елементарних функціональних блоків (EFB) відомі і доступні, але це не так.
3) Способи часто мають обмеження, пов'язані з, наприклад, обробкою часових або аналогових сигналів: моделі можуть потребувати ручної настройки, щоб належним чином врегулювати таймери або лічильники [8], або такі змінні можуть бути опущені [6] [9].
Для усунення проблем інтерпритації результатів контрприкладів пропонують:
1) алгоритми мінімізації [11] (K. Ravi, F. Somenzi, “Minimal Assignments for Bounded Model Checking”, K. Jensen, & A. Podelski (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 2988, pp. 31-45, 2004.).
2) Але більш практичної точки зору заслуговують методи візуалізації. Інтуїтивно зрозумілим методом візуалізації є тренди [4](E. Jee, S. Jeon, S. Cha, K. Koh, J. Yoo, G. Park, P. Seong, “FBDVerifier: Interactive and Visual Analysis of Counter-Example in Formal Verification of Function Block Diagram”, Journal of Research and Practice in Information Technology, Vol. 42, pp. 171-188, 2010.)
Але при сотянях змінних моделі - це проблема. Користувачі вибирають найзручніший для них та процесу
[12] K. Loer, M. Harrison, “Integrating Model Checking with the Industrial Design of Interactive Systems”, 26th International Conference on Software Engineering, Edinburgh, Scotland, UK, May 23-28, 2004


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 21:17 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
4. Modular approach to model checking of PLC software
4.1. The function block model code library
Запропонований підхід для моделчекінг програм на FBD заснована на ручній специфікації модельчекер коду для кожного EFB Підставою для прибігання до ручної специфікації блоку наступні:
1) багато з виробників замість стандартного мають Вендор-специфік ФБД
2) часто ФБ є ноу-хау протектед (чорний ящик), і юзер має тільки опис інтерфейсу
3) навіть якщо ФБ є білим ящиком, мови його реалізації не дають можливість конвертувати їх в такі інструменти як NuSMV
Відправною точкою для моделювання є функціональний опис елементарних функціональних блоків. Відповідний код моделчекера потім записується для кожного блоку. Моделчекінг може бути використаний для того, щоб перевірити правильність моделі ФБ , шляхом перевірки властивостей, отриманих з функціонального опису.
Як невеликий приклад на рис 1 нижче показує фрагмент (нестандартного) функції блок-схемі з двома з'єднаних між собою блоків: більшої-ніж блок, і бістабільних набір-скидання пам'яті блоку.
Зображення
Відповідний код в NuSMV для двох функціональних блоків читатиметься таким чином:
Зображення
Код для виклику і з'єднання двох об'єктів блоків на діаграмі в такій редакції:
Код:
VAR
IN1 : 4..20;
IN2 : boolean;
GT001 : GT(IN1, 15);
SR001 : SR(GT001.out, IN2);

NuSMV містить тільки основні вирази і прості типи (boolean, integer, enumeration, bit word, array), це означає, що алгоритмічно багаті функціональні блоки (наприклад, PID) не можуть бути змодельовані з достатньою точністю. Логіка управління Комплекс тому або абстракції, або повністю виключити з перевірки. Тому сукупна логіка управління або абстрактна, або повністю виключена з верифікації. (Complex control logic is therefore either abstracted away, or completely omitted from verification.)


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 21:42 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
4.2. Function block diagram modelling
Як тільки бібліотека модулів кодів моделей (що відповідає набору ЕФБ для конкретного вендора) була побудована, задача моделювання будь-якої ФБД зводиться до створення тієї ж самої сполуки блоків в моделі NuSMV. Це досягається за рахунок або а) вручну копіювати структуру схема, або б) імпорту структуру схема безпосередньо з іншого інструменту. Для цих цілей ми використовуємо інструмент Simantics введений в наступному розділі.

4.3. Challenges in diagram modelling
Ключовою перешкодою для застосування моделчекінга є занадто великі автомати станів. У нашій роботі, ми рідко виявивляли, що це є проблемою. Особливо, коли йде перевірка двійкової логіки, метод ваги показує хороші результати з часом аналізу для кінцевих автоматів з 1040 станів в діапазоні від хвилин, якщо не секунд. Навіть з аналоговими (цілими) значеннями та простою математикою, NuSMV дуже ефективний. Проблеми звичайно виникають від надмірної кількості петель зворотного зв'язку і, наприклад, ФБ для зберігання цілочисельних даних в пам'ять.
Є, однак, аспекти моделювання ФБД, які потребують особливої ​​уваги від модельєра: синхронізація, асинхронності (в розподілених системах), і дискретизації аналогових змінних. Крім того, оскільки NuSMV може обробляти тільки цілі числа, то масштабування назад і вперед іноді необхідно правильно змоделювати просту арифметику.


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 22:19 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
5. A graphical toolset for model checking
5.1. Simantics
Simantics є відкритою, онтологіє-орієнтованою інтеграційною платформою для різних інструментів моделювання та імітації
[13] T. Karhela, A. Villberg, H. Niemistö, “Open ontologybased integration platform for modeling and simulation in engineering”, International Journal of Modeling, Simulation, and Scientific Computing, Vol. 3, 2012.
Спочатку розроблена в VTT, в даний час випущений і підтримується як засіб з відкритим кодом по THTH Association of Decentralized Information Management for Industry (http://www.ththry.org).
Simantics має архітектуру клієнт-сервер на основі платформи Eclipse. Для наших цілей, Simantics надає фреймворк для графічного моделювання з можливістю перегляду і редагування структури моделі, повторного використання компонентів моделі, підтримка валідації моделі, управління версіями ... і легкої інтеграції з існуючою інструменту Model Checker. З'єднання з САПР надає можливості імпорту моделі на основі даних, отриманих від інструментів розробки програмного забезпечення [13] T. Karhela, A. Villberg, H. Niemistö, “Open ontologybased integration platform for modeling and simulation in engineering”, International Journal of Mod
Зображення
Figure 2. The Simantics modelling tool allows the user to specify the function block diagram in a graphical view, and generates the corresponding input file for the NuSMV model checker.


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 22:34 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
5.2. NuSMV integration
Ми розробили утиліту модельчекінга для Simantics, який в даний час дозволяє побудувати або відтворити ФБД, використовуючи графічний інтерфейс користувача для перетворення структури діаграми на вхідний файл NuSMV.
Моделчекінгтул складається з чотирьох основних модулів. Є два онтологічні плагіни, плагін для інтеграції NuSMV, і плагін для оновлення інтерфейсу користувача та моделі. Перший модуль онтології визначає фундаментні концепції для моделювання, а інший модуль використовує їх, щоб встановити різні зумовлені концепції, такі як типи змінних, які доступні.
Плагін інтеграції NuSMV дозволяє управління конфігурацією для різних версій Model Checker, і надає інтерфейс для зв'язку з NuSMV. Плагін узер-інтерфейсу пов'язує елементи разом, -і надає можливості для управління моделями.


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 22:47 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
5.3. Modelling with Simantics
З метою визначення коду моделі ЕФБ, користувачеві надається з textbased редактор коду. Для кожного типу ЕФБ, користувач вказує інтерфейс блоку (вхідних і вихідних портів), пише внутрішній код, і визначає графічний елемент. Після того, як побудований, бібліотека функціональних блоків може бути експортована і рошарена між різними користувачами.
Після того як бібліотека кодів ЕФБ завершена, користувач може побудувати модель системи в графічному вигляді, шляхом драг/дроп і зєднання (малюнок 2)...
Композитні типи функціональних блоків також можуть бути визначені. Внутрішня логіка спочатку складається з наборів функціональних блоків. Логіка потім инкапсулируются в композитному блоці, і відповідний графічний елемент знову визначений. Після цього, композитні блоки можуть бути додані так саме як ЕФБ. Багаторівнева ієрархічна модель може бути безпосередньо переглянута, як двічі клацнувши будь-яку складовою блок на діаграмі буде виявити основні внутрішню логіку.
Потім користувач може згенерувати вхідний файл для NuSMV що містить всі необхідні елементи моделі (код для використовуваних елементарних блоків, а також модулі верхнього рівня). Властивості системи в даний час входять у вигляді звичайного текстового файлу (дивіться розділ 5.5).


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 22:53 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
5.4. Counterexample visualisation
Графічно контрприклади відображаються підсвічуванням сигналів (червоний=1/чорний=0) з можливістю покрокового проходження в обидва боки, а також доступні тренди.


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 23:06 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
5.5. Future work
На додаток до моделі системи, в якості входу для модельчекінга також необхідні властивості, що визначають правильну поведінку системи. Класично вони виражаються за допомогою темпоральної логіки, однак вони можуть стати заплутаним і важким для розуміння. Щоб полегшити це, ми в даний час працюємо над формуванням для формалізації властивостей на основі шаблонів, чи роботі про моделей специфікації властивостей разом с Dwyer et al. [14].
[14] M. B. Dwyer, G. S. Avrunin, J. C. Corbett, “Patterns in Property Specification for Finite-State Verification”, Proceedings of the 21st International Conference on Software Engineering, ACM, New York, 2012.
З Simantics наша наступна мета полягає в реалізації автоматичного імпорту структури ФБД з існуючих програмних забезпеченнь .
Ми також беремо участь у теоретичних дослідженнях з Університетом Аалто по таким темам, як: 1) композиційного аналізу дуже великих моделей з використанням ітеративного пошуку абстракції 2) розробка інструментів і методів для аналізу асинхронних явища в розподілених системах, і 3) моделювання режимів збоїв апаратного забезпечення ПЛК.


Догори
 Профіль  
 
 Тема повідомлення: Re: A toolset for model checking of PLC software (+укр.нот)
ПовідомленняДодано: 01 жовтня 2014, 23:10 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
6. Conclusions
Careful verification and validation of PLC software is an important issue for not only systems that are safetycritical, but also for applications whose downtime leads to substantial financial loss. Practise has shown that model checking is a valuable V&V method, since hidden errors can be found from systems already evaluated using more traditional means.
Although the use of relatively simple modelling languages means that systems with arithmetically complex elements (PID blocks, for example) cannot be effectively analysed, model checking is very powerful in the verification of more straightforward binary logic.
Function block diagrams specify a clear input-output mapping and have a well-defined modular structure.
Both these factors make model checkers like NuSMV a viable tool for the evaluation of PLC software. Due to lack of domain-specific tools, however, application of model checking is all but mainstream in the control engineering domain. A lot of time and expertise are needed, as is common with formal methods. Other proposed methods of automating the work process rely on the use of standard programming languages (most often IEC 61131-3) and/or access to function block source code, both of which are far from guaranteed when dealing with many system vendors.
Having to specify the function block model code library manually may seem rudimentary, but in many cases, it might be the only option, and it only has to be done once for each vendor-specific function block specification. Certainly the approach is universal, and our claim that it is also very effective is supported by the several years of experience we have in model checking real-world systems in customer projects.
Using the open source modelling platform Simantics, we have been developing tools to support model checking of function block based software. The advantages have been obvious, since (notwithstanding the initial work phase of defining block model code library) specifying the model now requires very little understanding of the modelling languages involved.
By far the most useful feature, however, is the visualisation of counterexamples as a “living” function block diagram, a step-by-step animation that can be freely manipulated. This intuitive presentation is clearly superior to trend displays in helping the modeller or analyst find the root of the cause. This sophisticated feature would also be difficult to implement if the model specification used in model checking did not follow the modular structure of the original function block diagram.


Догори
 Профіль  
 
Відображати повідомлення за:  Сортувати за  
Створити нову тему Відповісти  [ 10 повідомлень ] 

Часовий пояс UTC + 2 годин [ DST ]



Хто зараз онлайн

Зараз переглядають цей форум: Немає зареєстрованих користувачів і 1 гість


Ви не можете створювати нові теми у цьому форумі
Ви не можете відповідати на теми у цьому форумі
Ви не можете редагувати ваші повідомлення у цьому форумі
Ви не можете видаляти ваші повідомлення у цьому форумі
Ви не можете додавати файли у цьому форумі

Знайти:
Вперед:  
cron
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group
Вы можете бесплатно создать форум PHPBB2 на MyBB2.ru, Также возможно создать форум бесплатно PHPBB3 на Getbb.ru
Український переклад © 2005-2007 Українська підтримка phpBB