Перевод названия: 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
Место издания: Новосибирск
Издатель: Федеральное государственное бюджетное образовательное учреждение высшего образования Новосибирский государственный технический университет