Программные продукты и системы

Верификация работы программных и технических систем является неотъемлемой частью их жизненного цикла. Существует целый ряд инструментов и средств верификации, которые являются более удобными и эффективными при тех или иных условиях, на тех или иных этапах проектирования и сопровождения. Однако за последние два десятилетия лучше всего себя зарекомендовали инструменты формальной верификации, работа которых может быть автоматизирована, а корректность функционирования – доказана формально. Наиболее активно используемым инструментом на сегодняшний день является метод формальной верификации на моделях, или Model Checking.

Технология процесса верификации программных и технических систем методом проверки на моделях подразумевает создание моделей систем, свойства которых требуется проверить. Так, например, модель системы может быть задана с помощью различных структур данных, в частности таких, как структура Крипке, язык асинхронных процессов Promela, в виде конечного автомата и т.д. Однако независимо от представления модели системы и верифицируемых свойств, заданных на базе логики линейного времени (LTL), необходим, как правило, процесс их преобразования к автоматам Бюхи. При этом алгоритмы преобразования формул LTL в автоматы Бюхи являются нетривиальными, а принципы их функционирования непонятны на интуитивном уровне.

Подробное описание дается в статье «Построение моделей систем на базе эквациональной характеристики формул LTL», авторы: Кораблин Ю.П. (Российский государственный социальный университет, г. Москва), Шипов А.А. (Московский технологический университет (МИРЭА), Москва).