загальна теорія 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.