Форум АСУ в Україні
http://asu.in.ua/

Formal Specification and Verification of Industrial Control
http://asu.in.ua/viewtopic.php?f=235&t=867
Сторінка 2 з 2

Автор:  san [ 09 жовтня 2014, 12:41 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

V. FORMAL DEFINITION OF THE RAC

Автор:  san [ 09 жовтня 2014, 12:41 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

VI. INDUSTRIAL EXAMPLES
A. Actuator Library Component

Автор:  san [ 09 жовтня 2014, 12:41 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

B. Safety Library Components

Автор:  san [ 09 жовтня 2014, 12:42 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

C. Automatic Packing Application

Автор:  san [ 09 жовтня 2014, 12:42 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

VII. RAC DEVELOPMENT TOOL
Реалізований прототим інструменту розробки RAC.
У цьому інструменті РАК можуть бути розроблені як IEC 61131-3 ФБ розширені специфікацією. Специфікація і реалізація може бути автоматично трансльовані на модельчекер Cadence SMV [8] для формальної верифікації. Якщо специфікація не виконується, SMV виробляє контрприклад для виправлення реалізації або специфікації. Інструмент розробки RAC обговорюється нижче, трансляція на SMV розглядається в розділі VII-A, і проектні рішення і можливі покращення обговорюються в розділі VII-B.
Щоб не бути пов'язаним до конкретного розробника PLC, в інструменті використовуються принципи і формати запропоновані PLCopen. PLCopen [18]. PLCopen визначив відкритий інтерфейс для програм ПЛК з XML (Extensible Markup Language) схемами. РАК можуть бути збережені в цьому форматі XML, злегка розширеними для обробки специфікації.
Редактор RAC заснований на відкритому редакторі PLCopenEditor розробленому Beremiz [19].
Редактор RAC розширює PLCopenEditor:
1) редактором специфікації;
2) можливістю зберегти закінчені РАК в форматі XML;
3) автоматичною трансляцією в інструменту верифікації.
В даний час реалізація RAC повинні бути розроблені в Ladder Diagram, а специфікація повинна бути розроблена на ST-базисній мові специфікацій.

Автор:  san [ 09 жовтня 2014, 12:43 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

A. Translation to Verification Tool
Для того щоб перевірити RAC, і інтерфейс і тіло RAC повинні бути трансльовані у вхід модельчекера. Модельчекер виконує перебір у всьому просторі станів і визначає, чи виконується специфікація[6].
Перевірка може бути виконана автоматично і може генерувати контрприклади, що показують, чому специфікація не була виконана.
Хоча верифікація може бути виконана тільки на кінцевій кількості станів системи, вона може бути використана в багатьох випадках і добре підходить до фреймворка RAC.
Використовується модельчекер Cadence SMV. SMV приймає в якості вхідних даних текстові описи систем з кінцевим числом станів. Кожна система може бути реалізована у вигляді окремого модуля, або мережі модулів. Модулі описані з використанням декларативного підходу, де наступний стан змінної описується виразом.
Next(V)=...
Специфікації включені в модулі. SMV може перевірити великі системи за допомогою OBDDs (Ordered Binary Decision Diagrams) представити систему символічно. Для отримання додаткової інформації про SMV [8] і [20].
Перетворення інтерфейсу досить проста допомогою таблиці I.
Якщо використовуються змінні з суфіксом _previous, ці змінні повинні бути ініціалізовані в SMV. Вони за замовчуванням ініціалізуються в початкове значення визначеного в редакторі RAC. Однак, якщо специфікація не виконується в початковому стані, як наслідок ініціалізації, користувач може вибрати ігнорування початкового стану при перевірці.

Автор:  san [ 09 жовтня 2014, 12:43 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

A. Translation to Verification Tool

Автор:  san [ 09 жовтня 2014, 12:44 ]
Тема повідомлення:  Re: Formal Specification and Verification of Industrial Control

B. Design Discussions

Сторінка 2 з 2 Часовий пояс UTC + 2 годин [ DST ]
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group
http://www.phpbb.com/