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

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

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




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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
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.
опис
Цитата:
Component-based programming frameworks for industrial control logic development promise to shorten development and modification times, and to reduce programming errors. To get these benefits, it is, however, important that the components are specified and verified to work properly. This work introduces Reusable Automation Components (RACs), which contain not only the implementation details but also a formal specification defining the correct use and behaviour of the component. This formal specification uses temporal logic to describe time-related properties and has a special structure developed to meet industrial control needs. The RAC can be formally verified, to determine whether the implementation fulfils the specification or not. A RAC prototype development tool has been developed to demonstrate this capability. The main difference between the RAC and other frameworks for formal verification of control logic is the specification modeling. In RAC, not only the implementation but also the specification is based on the structure and languages of conventional control logic, aiming at being easy to comprehend for control logic engineers. Several industrial examples are discussed in this paper, showing the benefits and potential of the framework.


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
[5] O. Ljungkrantz and K. Åkesson, “A study of industrial logic control programming using library components,” in Proc. 3rd Ann. IEEE Conf. Autom. Sci. Eng., Scottsdale, AZ, 2007, pp. 117–122.
[7]G. Frey and L. Litz, “Formal methods in PLC programming,” in Proc. 2000 IEEE Int. Conf. Syst., Man, Cybern., Nashville, TN, 2000, pp. 2431–2436.
[9] B. Meyer, “Applying “design by contract”,” Computer (IEEE), vol. 25, no. 10, pp. 40–51, 1992.
[10] H. W. Schmidt, B. J. Krämer, I. Poernomo, and R. Reussner, “Predictable component architectures using dependant finite state machines,” in Radical Innovations of Software and Systems Engineering in the Future, ser. Lecture Notes in Computer Science. New York: Springer, 2004, vol. 2941, pp. 310–324.
[11] S. Lu and W. A. Halang, “Platform-independent specification of component architectures for embedded real-time systems based on an extended UML,” in Component-Based Software Development for Embedded Systems, ser. Lecture Notes in Computer Science. New York: Springer, 2005, vol. 3778, pp. 123–142.
[13] O. Ljungkrantz, K. Åkesson, and M. Fabian, “Formal specification and verification of components for industrial logic control programming,” in Proc. 4th IEEE Conf. Autom. Sci. Eng., Washington, DC, 2008, pp. 935–940.


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Abstract
Використання Component-based programming frameworks повинні скоротити час розробки ПЗ і знизити помилки програмування. Однак ці компоненти повинні бути специфіковані і верифіковані, щоб працювали належним чином. Дана стаття представляє Reusable Automation Components (RACs), які містять не тільки деталі реалізації, а і формальні специфікації, які визначають правильну поведінку і використання компонентів. Ці формальні специфікації використовують темпоральні логіки для опису властивостей, пов'язаних з часом і мають спеціальну структуру, розроблену для задоволення потреб промислового управління.
RAC можуть бути формально верифіковані перевірені, щоб визначити, чи відповідає реалізація специфікації чи ні. Був розроблений прототип інструменту розробки RAC для демонстрації цієї здатності.
Основна відмінність між RAC та іншими фреймворками для формальної верифікації логіки управління є специфікація моделі.
У RAC, не тільки реалізація, але і специфікація базується на структурі і мовах звичайної логіки управління, спрямованих на їх легке зрозуміння для автоматчиків. В даній роботі обговорюються кілька прикладів з промисловості, що показують переваги і потенціал фреймворку.
Практичне використання
Програми на ПЛК важко і довго відлагоджуються, що для рального виробництва приводить до надмірних витрат. Для полегшення розробки програм пропонується ввести RAC (надалі по тексту буду писати РАК). Повторне використання компонентів (перевірених) прискорить написання програми і забезпечить захист від помилок. Для цього розробляється специфікація для первірки компонентів. Ці специфікації можуть бути використані для перевірки в спец.інтсрмуентах (модельчекерах) на моделях, в які транслюються компоненти РАК. Оскільки специфікація повинна задаватися автоматчиками, то специфікація РАК задається на мовах ПЛК.


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
I. INTRODUCTION
Описується багато проблем пов'язаних з необхідністю тестувати код на реальному виробництві. Деякі рішають шляхом розробки і інкапсуляції кода в типові ФБ [5], деякі перевіряють код на системах імітаційного моделювання.
Розробка ПЗ для ПЛК на базі повторновикористовуваних компонентах (РК) дозволяє швидко і коректно змінювати програму. Однак тільки інкапсулювати код в ФБ - замало. Ефективне використання цих РК потребує знань ЯК їх використати і ЩО вони гарантують. Слід перевірити чи відповідають компоненти заданій специфікації.
Польові перевірки компонентів і перевірка на імітаторах може бути використані для верифікації, що специфікація виконується. Тим не менш, у багатьох випадках, це забирає багато часу або навіть неможливо перевірити чи імітувати всі можливі сценарії, в яких можуть бути використані компоненти. Тому ми пропонуємо також використовувати формальну верифікацію. Формальна верифікація компонента означає автоматичне дослідження всіх можливих поведінок компонента, для перевірки відповідності специфікації.
Багато дослідників запропонували інструменти і методи, щоб використовувати формальну перевірку в розробці програм PLC [7]. Багато з них пропонують автоматчикам вивчити нові мови для реалізації або для створення моделі. Інші пропонують автоматично переводити існуючі програми ПЛК в моделі, але специфікацію все одно задавати на нових для них інструментах та мовах. Однак автоматчики добре знають мови ПЛК і зовсім не орієтуються в мовах та інструментах задання специфікацій. Тому ця стаття пропонує метод, який підьтримує формальну специфікацію і верифікацію однак з невеликими додатковими вимогами до знань автоматчиків.
Пропонується використовувати РАС, який містить компоненти як для реалізації так і для опису специфікації, що дозволить використати формальну верифікацію на моделях. Представлений також прототип інтсрументу який автоматично транслює РАК на вхід моделчекера Cadence SMV. Моделчекер Cadence SMV автоматично перевіряє відповідність специфікації і у негативному випадку дає контрприклад, по якому можна визначити місце помилки і виправити в РАС. Основна новизна RAC в структурі специфікації, натхненний "дизайн за контрактом" [9] і адаптовані для програм з циклічним виконанням (для ПЛК). Також в статті представлена мова опису специфікації і прототип утиліти розробки.
"Дизайн за контрактом" був використаний разом з IEC 61131-3 і раніше, але по-різному [10] - [12]. Ці статті показують як розробити або генерувати програми ПЛК, реалізовані на IEC 61131-3 мовах, але жоден з них не показує, як може бути зроблена специфікація за допомогою IEC 61131-3 в поєднанні з "дизайн-контрактних" понять.
Фреймворк RAC також обговорюється в [13], в якій представлено застосування їх в промислових системах управління. Ця стаття описує RAC більш ретельно, ніж [13] і включає в себе формальну модель РАК і деталі інструменту розробки RAC. Мова специфікації також скоригована в цій статті.
Наступний розділ знайомить з основними частинами RAC, а також прикладом. Структура специфікації додатково обговорюється в розділі III, мова специфікацій описаний в розділі IV. У цих розділах для пояснення специфікація використовується приклад . RAC підсумовується і формалізовується в розділі V. Приклади використання в промисловості представлені в розділі VI, з наступним представленням та обговорення інструменту розробки RAC в розділі VII. Нарешті, робота полягає в Розділі VIII.


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
II. OVERVIEW OF THE REUSABLE AUTOMATION COMPONENT

Зображення
Основні частини RAC для побудови програм управління ПЛК наведені ліворуч. Праворуч показана структура специфікації для ПЛК-орієнтованих моделей див розділ III.
Надалі слово "компонент" використовується тільки в контексті РАК. Рак має інтерйес і тіло. Інтерфейс складається з входів(I), виходів(O) і специфікації. Тіло реалізує функції компоненту і декларує будь які внутрішні змінні (V). Тіло доступне тільки для розробників компоненту (інкапсуляція). Специфікація РАК розроблена для використання формальної верифікації, для перевірки чи відповідає реалізація повністю специфікації.
Основні принципи побудови РАК носять загальний характер і відкриті для різних мов програмування для реалізації. Приклади реалізацій є на ФБ для IEC 61131-3 та IEC 61499. У реалізації RAC оновлення може бути як на основі циклу (IEC 61131-3) так на основі подій (IEC 61499). Коли RAC оновлюється нові значення ​​виходів і внутрішніх змінних обчислюються в залежності від поточних значень вхідних і внутрішніх значень змінних.
Таким чином, кожне оновлення позначається унікальним індексом K є N, воно збільшується на одиницю з кожним апдейтом блоку.
Зображення
Формальне визначення RAC, I,O,V,f дані в секції V.

Хоча неформальні описи в RAC (природною мовою, картинки і т.д.) може допомогти в розумінні RAC, такі описи не підходять для формальної верифікації, так як вони можуть бути неоднозначними і можуть бути неправильно витлумачені. Формальна верифікація вимагає формальної специфікації. Таким чином, RAC доповнюється формальними специфікаціями. Формальна специфікація може розглядатися як однозначна абстракція реалізації; Наприклад, вона може вказати, що певна комбінація входів завжди призводить до певної комбінації виходів.
Структура специфікації базується на концепції "Дизайну за контрактом" [9]. Проектування за контрактом був введений Бертраном Мейером, щоб отримати надійні і повторно-використовувані об'єктно-орієнтовані програми на мові програмування Eiffel. Для кожної процедури програмного забезпечення, договір може виразити парою передумови і постумови. Передумова висловлює вимоги, яким повинен задовільняти виклик підпрограми, для гарантування постумови.


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
A. Example


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
III. SPECIFICATION STRUCTURE


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
III. SPECIFICATION STRUCTURE


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
IV. SPECIFICATION LANGUAGE
A. Temporal Logic
Зображення


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

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
B. Specification in IEC 61131-3


Догори
 Профіль  
 
Відображати повідомлення за:  Сортувати за  
Створити нову тему Відповісти  [ 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