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

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

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




Створити нову тему Відповісти  [ 18 повідомлень ]  На сторінку Поперед.  1, 2
Автор Повідомлення
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:41 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
V. FORMAL DEFINITION OF THE RAC


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:41 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
VI. INDUSTRIAL EXAMPLES
A. Actuator Library Component


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:41 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
B. Safety Library Components


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:42 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
C. Automatic Packing Application


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:42 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
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-базисній мові специфікацій.


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:43 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
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. Однак, якщо специфікація не виконується в початковому стані, як наслідок ініціалізації, користувач може вибрати ігнорування початкового стану при перевірці.


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:43 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
A. Translation to Verification Tool


Догори
 Профіль  
 
 Тема повідомлення: Re: Formal Specification and Verification of Industrial Control
ПовідомленняДодано: 09 жовтня 2014, 12:44 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
B. Design Discussions


Догори
 Профіль  
 
Відображати повідомлення за:  Сортувати за  
Створити нову тему Відповісти  [ 18 повідомлень ]  На сторінку Поперед.  1, 2

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



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

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


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

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