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

Перевод названия: VERIFICATION FUNCTIONAL DATAFLOW PARALLEL PROGRAMS USING METHOD OF INDUCTIVE APPROVALS

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

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

Ключевые слова: verification, specification, correctness, functional dataflow parallel programming, верификация, спецификация, корректность, функционально-потоковое параллельное программирование

Аннотация: Метод индуктивных утверждений изначально был сформулирован для верификации последовательных императивных программ. В статье предложено его использование для верификации функционально-потоковых параллельных программ на языке Пифагор. Представленная адаптация метода опирается на информационный граф функционально-потоковой модели параллельных вычислений. Спецификация пользователя задается с применением классических начальных и промежуточных утверждений. Для описания спецификации применяются формулы, которые реализованы с применением специализированного языка. Начальное утверждение описывает общий вид аргумента функции. Для его описания доступны константы, определяющие тип аргумента, а также формулы, определяющие принадлежность аргумента к указанным интервалам, если он является численным. Промежуточные утверждения ставятся в соответствие с узлами информационного графа программы. Для описания промежуточных утверждений доступны все базовые операторы языка Пифагор, а также формулы, применяемые к начальному утверждению. Это позволяет накладывать на выполняемую программу различные условия и ограничения. Условия рекомендуется формулировать таким образом, чтобы они возвращали булево значение. В этом случае можно однозначно сделать заключение о том, соответствует или нет выполнение программы заданному утверждению. Помимо этого, полученное булево значение используется для отображения ошибок, возникающих в программе. Эти ошибки отображаются на информационном графе программы. Применение метода индуктивных утверждений для верификации функционально-потоковых параллельных программ позволяет проверить соответствие вычислений программы спецификации пользователя и интервально оценить вычисленные программой результаты. Это облегчает процесс разработки, тестирования и отладки функционально-потоковых параллельных программ.

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

Издание

Журнал: Доклады Академии наук высшей школы Российской Федерации

Выпуск журнала: 2-3

Номера страниц: 125-132

ISSN журнала: 17272769

Место издания: Новосибирск

Издатель: Федеральное государственное бюджетное образовательное учреждение высшего образования Новосибирский государственный технический университет

Авторы

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

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

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