Инструментальная поддержка формальной верификации программ, написанных на языке функционально-потокового параллельного программирования

Мария Сергеевна Ушакова, Александр Иванович Легалов

Аннотация


Работа посвящена разработке архитектуры инструментальных средств для поддержки формальной верификации функционально-потоковых параллельных программ на языке Пифагор. Используемый метод формальной верификации --- дедуктивный анализ на базе исчисления Хоара. Процесс доказательства корректности программы представляется в виде дерева,каждый узел которого --- информационный граф программы в котором дуги размечены формулами на языке спецификации. Корнем дерева является исходная тройка Хоара: информационный граф с редусловием и постусловием. В работе рассматриваются основные преобразования, применяемые к информационному графу программы: разметка дуг, эквивалентное преобразование, расщепление, свертка программы. Посредством данных преобразований исходная тройка модифицируется и в конечном счете сводится к набору формул на языке спецификации, истинность которых будет свидетельствовать о корректности программы. Предложена архитектура системы поддержки формальной верификации функционально-потоковых параллельных программ, которая позволяет строить дерево доказательства. Представлена реализация этой системы, описана ее основная
функциональность.

Ключевые слова


функционально-потоковое параллельное программирование; язык программирования Пифагор; верификация программ; инструментальные средства для поддержки формальной верификации

Полный текст:

PDF

Литература


Непомнящий, В.А. Прикладные методы верификации программ /

В.А. Непомнящий, О.М. Рякин - М.: Радио и связь, 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.




DOI: http://dx.doi.org/10.14529/cmse150205