ИНСТРУМЕНТАЛЬНАЯ ПОДДЕРЖКА ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ПРОГРАММ, НАПИСАННЫХ НА ЯЗЫКЕ ФУНКЦИОНАЛЬНО-ПОТОКОВОГО ПАРАЛЛЕЛЬНОГО ПРОГРАММИРОВАНИЯ

Перевод названия: A TOOLKIT FOR SUPPORTING FORMAL VERIFICATIONOF PROGRAMS IN THE FUNCTIONAL DATA-FLOWPARALLEL PROGRAMMING LANGUAGE

Тип публикации: статья из журнала

Год издания: 2015

Идентификатор DOI: 10.14529/cmse150205

Ключевые слова: functional data-flow parallel programming, Pifagor programming language, programs formal verification, toolkit for supporting formal verification, функционально-потоковое параллельное программирование, язык программирования Пифагор, верификация программ, инструментальные средства для поддержки формальной верификации

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

Ссылки на полный текст

Издание

Журнал: Вестник Южно-Уральского государственного университета. Серия: Вычислительная математика и информатика

Выпуск журнала: Т.4, 2

Номера страниц: 58-70

ISSN журнала: 23059052

Место издания: Челябинск

Издатель: Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования Южно-Уральский государственный университет (национальный исследовательский университет)

Авторы

Вхождение в базы данных

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

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