На правах рекламы:
ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Авторитетность издания

ВАК - К1
RSCI, ядро РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2024

В Санкт-Петербургском национальном исследовательском университете информационных технологий, механики и оптики (Университет ИТМО) исследовалась верификация вычислительных процессов на основе графоаналитической модели.

27.12.2017

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

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

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

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

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

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

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

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