Аннотация:
Обсуждаются вопросы построения технологии анализа корректности программ логических контроллеров. Рассматривается пример моделирования и верификации «дискретных» LD-программ с таймером с помощью программного средства символьной проверки модели SMV при спецификации свойств на языке темпоральной логики линейного времени LTL.
Ключевые слова:верификация, проверка модели, программы логических контроллеров, LD-диаграммы.
Полный текст:
PDF файл (186 kB)