Відкритий робочий матеріал(може комусь ще знадобиться).
Стаття про використання одного з підходів верифікації програм Model Checking для програм, написаних на мові FBD.
2.1. Model checkingРозповідається про метод верифікації програм - Model Checking, який описаний
viewtopic.php?f=235&t=859Далі про модель-чекер (опен сорс програма для перевірки) NuSMV
viewtopic.php?f=235&t=8592.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