Главная страница « Научно-исследовательский семинар « 2001 «

Доклад посвящен проблеме проверки правильности программ путем формальной верификации. Метод проверки на модели (Model Checking) основан на построении конечной модели распределенной программы, на которой доказывается истинность свойства, представленного формулой темпоральной логики.

Автором разработан эффективный алгоритм проверки истинности формул на моделях программ. В докладе описывается две модификации этого метода, основывающиеся на графовом и символьном представлении модели. Предлагаемые алгоритмы используют понятие справедливости, позволяющее уточнить результат верификации. Приводится алгоритм выделения трассы вычисления, на которой нарушается проверяемое свойство.

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

Разработанные алгоритмы были реализованы в системе верификации среды имитационного моделирования DYANA. Система прошла апробацию на модели бортового вычислительного комплекса, решающего задачи навигации.

Приглашаются аспиранты и стажеры программистских кафедр.