ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2016 г.)
2-летний импакт-фактор РИНЦ: 0,493
2-летний импакт-фактор РИНЦ без самоцитирования: 0,389
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,732
5-летний импакт-фактор РИНЦ: 0,364
5-летний импакт-фактор РИНЦ без самоцитирования: 0,303
Суммарное число цитирований журнала в РИНЦ: 5022
Пятилетний индекс Херфиндаля по цитирующим журналам: 355
Индекс Херфиндаля по организациям авторов: 499
Десятилетний индекс Хирша: 11
Место в общем рейтинге SCIENCE INDEX за 2016 год: 304
Место в рейтинге SCIENCE INDEX за 2016 год по тематике "Автоматика. Вычислительная техника": 11

Больше данных по публикационной активности нашего журнале за 2008-2016 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

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

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

2
Ожидается:
16 Марта 2018

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

27.12.2017

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

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

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

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

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

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

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

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