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

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

Данная модель представляет собой концентрированное описание проектируемого программного продукта и служит основой для разработки программы и анализа ВП. Для ГАМ разработан формальный язык описания (версия 1), который содержит библиотеку примитивных вершин и правила их соединения для описания алгоритмов любой сложности. Более сложные конструкции языка (например, циклы или switch-case-конструкции) представляются в виде комбинации простейших.

Анализ программы на основе ГАМ осуществляется в несколько этапов.

1.  Описание ВП в формате ГАМ и составление его формального описания на языке описания ГАМ (ЯОГ).

2.  Проектирование программы на языке C#.

3.  Конвертация исходного кода программы в ЯОГ.

4.  Сравнение формального (эталонного) и сконвертированного (реального) описаний; в случае расхождения в структурах описаний программа отправляется на доработку (повторяются этапы 2–4); в случае совпадения можно утверждать, что разработанная программа соответствует ГАМ и формальная верификация прошла успешно, на основе чего можно осуществлять приемку исполняемого модуля.

Подробное описание дается в статье «Синтезирование программ на основе описания графоаналитической модели», авторы: Зыков А.Г., Кочетков И.В., Поляков В.И., Чистиков Е.Г. (Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики (Университет ИТМО), Санкт-Петербург).