ДОКЛАДЫ АКАДЕМИИ НАУК
ВЫСШЕЙ ШКОЛЫ РОССИЙСКОЙ ФЕДЕРАЦИИ

Print ISSN: 1727-2769    Online ISSN: 2658-3747
English | Русский

Последний выпуск
№3(40) июль-сентябрь 2018

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

Выпуск № 2-3 (23-24) апрель-сентябрь 2014
Авторы:

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

Список литературы
  1. Легалов А.И. Функциональный язык для создания архитектурно-независимых параллельных программ // Вычислительные технологии. – 2005. – Т. 10, № 1. – С. 71–89. 
  2. Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Средства отладки функционально-потоковых параллельных программ // Доклады Академии наук высшей школы Российской Федерации. – 2008. – № 1 (10). – С. 96–105. 
  3. Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Методы отладки и верификации функционально-потоковых параллельных программ // Журнал Сибирского федерального университета. Серия: Техника и технологии. – 2011. – Т. 4, № 2. – С. 213–224. 
  4. Лисков Б., Гатэг Дж. Использование абстракций и спецификаций при разработке программ. – М.: Мир, 1989. – 424 с. 
Просмотров: 912