Верификация модели технической системы средствами линейной темпоральной логики

Решается задача верификации электромеханического устройства с переменным числом контактов с помощью модальной логики LTL (Linear Temporal Logic). В ходе анализа доказываются теоремы о непрерывности и однозначности работы устройства, а также уясняются ограничения, необходимые для того, чтобы алгоритм работы устройства мог считаться полностью корректным.

Статья представлена к публикации членом редколлегии: О. П. Кузнецов