ВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНО-ПОТОКОВЫХ ПАРАЛЛЕЛЬНЫХ ПРОГРАММ МЕТОДОМ ИНДУКТИВНЫХ УТВЕРЖДЕНИЙ | Научно-инновационный портал СФУ

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

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

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

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

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

Аннотация: Метод индуктивных утверждений изначально был сформулирован для верификации последовательных императивных программ. В статье предложено его использование для верификации функционально-потоковых параллельных программ на языке Пифагор. Представленная адаптация метода опирается на информационный граф функционально-потоковой модели параллельных вычислений. Спецификация пользователя задается с применением классических начальных и промежуточных утверждений. Для описания спецификации применяются формулы, которые реализованы с применением специализированного языка. Начальное утверждение описывает общий вид аргумента функции. Для его описания доступны константы, определяющие тип аргумента, а также формулы, определяющие принадлежность аргумента к указанным интервалам, если он является численным. Промежуточные утверждения ставятся в соответствие с узлами информационного графа программы. Для описания промежуточных утверждений доступны все базовые операторы языка Пифагор, а также формулы, применяемые к начальному утверждению. Это позволяет накладывать на выполняемую программу различные условия и ограничения. Условия рекомендуется формулировать таким образом, чтобы они возвращали булево значение. В этом случае можно однозначно сделать заключение о том, соответствует или нет выполнение программы заданному утверждению. Помимо этого, полученное булево значение используется для отображения ошибок, возникающих в программе. Эти ошибки отображаются на информационном графе программы. Применение метода индуктивных утверждений для верификации функционально-потоковых параллельных программ позволяет проверить соответствие вычислений программы спецификации пользователя и интервально оценить вычисленные программой результаты. Это облегчает процесс разработки, тестирования и отладки функционально-потоковых параллельных программ. The method of inductive assertions was originally formulated for the verification of successive imperative programs. The use of this method for the verification of functional dataflow parallel programs developed in the Pythagor programming language is suggested in this paper. The adaptation of the inductive assertions method presented in the paper is based on the dataflow graph of a functional dataflow model of parallel calculation. A user's specification is specified by classical initial and intermediate assertions described by special formulas. These formulas are implemented by using a special language. An initial assertion describes a general form of an argument of a function. To describe it there are constants that determine the type of the argument. The formulas can specify the intervals in which arguments can be changed. Intermediate assertions correspond to the nodes of an information graph of the program. All basic language statements of the Pythagor language and formulas used to the initial assertion are available to describe intermediate assertions. This makes it possible to impose various conditions and constraints on the program which is running. Conditions must be formulated in such a way that they return a Boolean value. In this case it possible to make a definite conclusion whether the execution of the program corresponds to the specified assertion or not, In addition, the obtained Boolean value is used for displaying errors occurring in the program. These errors are displayed in the information graph of the program. The application of the method of inductive assertions to verify functional dataflow parallel programs makes it possible to check the agreement of the program computations with a user’s specification and to estimate the results of the program computation by intervals. This simplifies the process of developing, testing and debugging of functional dataflow parallel programs.

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

Издание

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

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

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

ISSN журнала: 17272769

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

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

Авторы

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

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

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