A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
DOI:
https://doi.org/10.14529/cmse150205Keywords:
функционально-потоковое параллельное программирование, язык программирования Пифагор, верификация программ, инструментальные средства для поддержки формальной верификацииAbstract
The article is devoted to the architecture development of the toolkit for supporting formal verification of functional data-flow parallel programs in the Pifagor Language. The method of deduction based on Hoare logic is used for formal verification. A proof process is considered as a tree where each node is a program data-flow graph, whose edges are marked with formulas in a specification language. The tree root is the initial Hoare triple, namely the program data-flow graph with a precondition and a postcondition. In this article basic transformations of the data-flow graph are considered: edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the initial triple is being transformed and finally is reduced to a set of formulas in the specification language. If all of these formulas are identically true, then the program is correct. Architecture of the toolkit for supporting formal verification of functional data-flow parallel programs is proposed, which allows to construct a proof three. The implementation of the toolkit is introduced and its main functionality is considered.
References
Непомнящий, В.А. Прикладные методы верификации программ /
В.А. Непомнящий, О.М. Рякин - М.: Радио и связь, 1988. - 255 с.
Hoare, C. A. R. An axiomatic basis for computer programming /
C. A. R. Hoare // Communications of the ACM. - 1969. - Vol. 10, No. 12. -P. 576-585.
Barnett, M. Boogie: A modular reusable verifier for object-oriented
programs / M. Barnett, B.Y.E. Chang, R. Deline, B. Jacobs, K.R.M. Leino // FMCO 2005. LNCS. - 2006. - Vol. 4111. - P. 364-387.
Непомнящий, В.А. Верификация C-программ в мультиязыковой системе СПЕКТР / В.А. Непомнящий, И.С. Ануреев, М.М. Атучин, И.В. Марьясов, А.А. Петров, А.В. Промский // Моделирование и анализ информационных систем. - 2010. - № 17 (4). - С. 88-100.
Van den Berg, J. The LOOP compiler for Java and JML /
J. Van den Berg, B. Jacobs // Tools and Algorithms for the Construction and Analysis of Systems. LNCS. - 2001. - Vol. 2031. -P. 299-312.
Ahrendt, W. The KeY Tool / W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. H"ahnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, P.H. Schmitt
// Software and System Modeling. - 2005. - Vol. 4 (1). - P. 32 -54.
Легалов, А.И. На пути к переносимым параллельным программам / А.И. Легалов, Д.А. Кузьмин, Ф.А. Казаков, Д.В. Привалихин // Открытые системы. - 2003. - № 5. - C. 36-42.
Легалов, А.И. Функциональный язык для создания архитектурно-независимых параллельных программ / А.И. Легалов
// Вычислительные технологии. - 2005. - № 1 (10). - С. 71-89.
Kropacheva, M.S. Formal Verification of Programs in the Pifagor Language / M.S. Kropacheva, A.I. Legalov // Parallel Computing Technologies (PaCT-2013) 12th International Conference, September 30 - October 4, 2013. Saint-Petersburg, Russia. LNCS. - 2013. - Vol. 7979. - P. 80-89.
Кропачева, М.С. Формализация семантики функционально-потокового языка параллельного программирования Пифагор / М.С. Кропачева // Проблемы информатизации региона (ПИР-2011): Материалы XII Всероссийской научно-практической конференции (Красноярск, 22-23 ноября 2011 г.). - Красноярск: Сибирский федеральный университет, 2011. - С. 144-148.
Матковский, И.В. Параллельная событийная машина для функционально-потокового языка "Пифагор" / И.В. Матковский // Информационные и математические технологии в науке и управлении: Сборник трудов XVVII Байкальской Всероссийской конференции с международным участием (Иркутск -- Байкал, 30 июня~-- 9 июля 2012 г.). Часть II. - Иркутск: ИСЭМ СО РАН, 2012. - С. 186-193.
Легалов, А.И. Событийная модель вычислений, поддерживающая выполнение функционально-потоковых параллельных программ / А.И. Легалов, Г.В. Савченко, В.С. Васильев // Системы. Методы. Технологии. - 2012. - № 1 (13). - С. 113-119.
