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

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

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




Створити нову тему Відповісти  [ 9 повідомлень ] 
Автор Повідомлення
 Тема повідомлення: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 02 жовтня 2014, 19:03 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
A formal specification language for PLC-based control logic
посилання на опис
Ljungkrantz, O. Dept. of Signals & Syst., Chalmers Univ. of Technol., Goteborg, Sweden
Akesson, K. ; Fabian, M. ; Chengyin Yuan
Industrial Informatics (INDIN), 2010 8th IEEE International Conference on
13-16 July 2010
Цитата:
Formal verification, using model checking tools, is promising in developing (IEC 61131) industrial control logic. Formal verification requires a formal specification of the properties to be verified. Specifications in model checking tools are typically expressed using temporal logic. However, the standard temporal logic dialects are not well suited for control engineers who do rarely have a background within computer science. In this paper a new dialect of linear temporal logic, ST-LTL, is introduced that intends to be easier to use for control engineers than the existing dialects. The relation of ST-LTL compared to existing temporal logic dialects is analyzed.


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification language for PLC-based control logic
ПовідомленняДодано: 02 жовтня 2014, 19:28 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
загальна теорія Model Checking - тут
I. INTRODUCTION
Розказується про Моделчекінг та його важливість при верифікації ПЗ.
Можна використати Моделчекінг і для верифікації програм ПЛК. Різні підходи до формальної верифікації програм ПЛК можна прочитати в
[4].G. Frey and L. Litz, “Formal methods in PLC programming,” in Proceedings of the 2000 IEEE International Conference on Systems,
Man and Cybernetics, Nashville, TN, USA, 2000, pp. 2431–2436.
Тим не меше широкого вжитку в промисловій автоматиці не набули. Дослідженн програмування в автомобільній промисловості
[5] M. Lucas and D. Tilbury, “A study of current logic design practices in the automotive manufacturing industry,” Int. J. Human-Computer Studies, vol. 59, no. 5, pp. 725–753, 2003.
[6] O. Ljungkrantz, K. A° kesson, and M. Fabian, “Practice of industrial control logic programming using library components,” in Programmable Logic Controller, L. A. Guedes, Ed. Intech, 2010, ch. 2, pp. 17–32.
Проблема є формування специфікації на темпоральній логіці.
В статті розглядається мова специфікації програм ПЛК для використання формальної верифікації і для повторного використання програм на мові ФБД. Мова повинна бути формальна але зрозуміла для ПЛК-програмерів. Пропонується новий діалект LTL(Linear Temporal Logic).
Порівняльний аналіз даний в:
[8] T. Mertke and T. Menzel, “Methods and tools to the verification of safety-related control software,” in Proceedings of the 2000 IEEE International Conference on Systems, Man and Cybernetics, Nashville, TN, USA, 2000, pp. 2455–2457.
[9] V. Vyatkin and G. Bouzon, “Using visual specifications in verification of industrial automation controllers,” EURASIP Journal on Embedded Systems, vol. 2008, no. 5, 2008.
В [10] описано як створити та реалізувати формальну модель.
[10] O. Ljungkrantz, K. A° kesson, M. Fabian, and C. Yuan, “Formal specification and verification of industrial control logic components,” accepted for publication in IEEE Transactions on Automation Science and Engineering, 2010.
Дана робота доповнює [10]
Наступний розділ стисло описує темпоральну логіку та LTL. Розділ III описує пропоновану мову специфікації, а потім деякі приклади в Розділі IV. Синтаксис формалізується в розділі V і виразність мови специфікації формально доведено в розділі VI. Робота показана в розділі VII.


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 16:10 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
II. TEMPORAL LOGIC
Розповідається про темпоральну логіку, логіки LTL, CTL та CTL*. В роботі використовують логіку LTL.


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 17:07 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
III. IEC 61131-3 BASED SPECIFICATION LANGUAGE
Пропонується нова мова специфікацій як комбінація LTL та IEC 61131-3. Такий підхід дасть можливість використовувати цю мову для формування специфікації програмерам ПЛК.
Для програмних компонентів ПЛК, послідовність спрацювання входів, як правило, невідома. Тому найбільш актуальним є вказати і перевірити, що станеться у всіх можливих послідовностях спрацювання входів, і чи існує послідовність, в якій деяка властивість виконується. Це головна причина, чому LTL була обрана в якості основи, для специфікацій на базі IEC 61131-3. Хоча мало місце тривалі дебати в спільноті компютерщиків, стосовно використання CTL чи LTL, більш пізні роботи показують, що
лінійна структура LTL є "більш природною для інженерів-верифікаторщиків" [11].
[11] M. Y. Vardi, “Branching vs. linear time: Final showdown,” in Tools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science. Springer, 2001, vol. 2031, pp. 1–22.
Крім того, вирази, які можуть бути виражені в CTL але не в LTL, наприклад AGEFp, як правило є структурними, а не поведінковими, тобто вони не можуть бути виявлені з точки зору вводу/виводу [12].
[12] S. Nain and M. Y. Vardi, “Branching vs. linear time: Semantical perspective,” in Automated Technology for Verification and Analysis, ser. Lecture Notes in Computer Science. Springer, 2007, vol. 4762, pp. 19–34.
The proposed specification language is as expressive as LTL, see proof in Section VI, but with different syntax and semantics. Three major changes can be observed:
Запропонована мова специфікація як як виразний LTL, описана в розділі VI, але з іншим синтаксисом і семантикою. Три основні відмінності від оригіналу:
  • Використовується IEC 61131-3 сумісна булева логіка. Обидва оператори і функції використовуються, щоб підтримати і графічної текстові мови, засновані.
  • Перейменовано темпоральні оператори і вбудовані конструкції. Пропонована мова специфікація містить не тільки перейменовані темпоральні оператори, але і вбудовані в специфікації конструкції (оператори, функції та змінні суфікси) для полегшення процесу специфікації.
  • Попередні значення змінних в наступному стані. Суфікс _previous може бути використаний, щоб посилатися до попередніх значень змінних, в тому числі не-булевих змінних, замість того, щоб посилатися на значення наступного стану, використовуючи X.


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 19:54 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
Пропоновані додаткові оператори, функції та змінні суфікси можна побачити в таблиці I.

Зображення


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 20:26 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
Ці зімни показані на прикладі.
Має бути спеицифікована властивість: "передній фронт логічного входу I (переход з 0 в 1) буде завжди гарантувати, що принаймні один з двох виходів O1 і O2, в кінцевому рахунку буде 1". В LTL це може бути виражено як:
G(¬I ∧ (X I ) ⇒ FX(O1 ∨ O2) ) (Spec1)
мої коменти написав:
G - утверждение Gq истинно в момент времени t (t |=Gq) , если для любого момента времени t' в будущем утверждение q истинно
X - утверждение Xq истинно в момент времени t , если q истинно в следующий момент t +1:
F - утверждение Fq истинно в момент времени t (t |=Fq ) , если для какого-то момента времени t' в будущем q станет истинным;
⇒ - імплікація "якщо...то"
¬ - заперечення "НЕ"
∨ - дизюнкція"АБО"
∧ - конюнкція"ТА"


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 20:28 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
В текстовому варіанті запропонованої мови це може бути як
Spec1 := ALWAYS (NOT I_previous & I -> EVENTUALLY(O1 OR O2) );
або
Spec1 := ALWAYS (I_risingEdge -> EVENTUALLY(O1 OR O2) );


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 22:02 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
IEC 61131-3 based boolean logic:
Аналогічно використанню двох підходів до написанню логіки в МЕК61131 (в текстових за допомогою операторів або функцій, наприклад "AND" або "&"), так саме можно і в запропонованій мові специфікацій.
Зображення
В ході бесід з автоматчиками, виявилося, що специфікація на мові ST вважалася самою інтуїтивною і зрозумілою альтернативою. Ця мова позначається ST-LTL в статті.


Догори
 Профіль  
 
 Тема повідомлення: Re: A formal specification lang for PLC-based control(+укрнот)
ПовідомленняДодано: 08 жовтня 2014, 22:09 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 5033
Renamed temporal operators and built-in constructs:
Прикладом додаткових темпоральних операторів є функція NEVER. Іншими прикладами є суфікси risingEdge і fallingEdge, які використовуються для позначення фронтів змінних.

Previous variable values instead of next state:


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

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



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

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


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

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