RUS ENG

< Синтез распределенного супервизорного управления в дискретно-событийных системах по LTL спецификации
12.10.2012 12:00 Давность: 7 yrs
Категория: Семинар

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

И. Шошмина, Д. Тимофеев, каф. РВКС, СПбГПУ


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

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

Формализация спецификации производится на языках Alloy и OWL.

Рассматривается вопрос проверки непротиворечивости формальной спецификации методами перечисления и доказательства.