Инструментальная поддержка формальной верификации программ, написанных на языке функционально-потокового параллельного программирования
Автор: Ушакова Мария Сергеевна, Легалов Александр Иванович
Рубрика: Информатика, вычислительная техника и управление
Статья в выпуске: 2 т.4, 2015 года.
Бесплатный доступ
Работа посвящена разработке архитектуры инструментальных средств для поддержки формальной верификации функционально-потоковых параллельных программ на языке Пифагор. Используемый метод формальной верификации - дедуктивный анализ на базе исчисления Хоара. Процесс доказательства корректности программы представляется в виде дерева, каждый узел которого - информационный граф программы в котором дуги размечены формулами на языке спецификации. Корнем дерева является исходная тройка Хоара: информационный граф с предусловием и постусловием. В работе рассматриваются основные преобразования, применяемые к информационному графу программы: разметка дуг, эквивалентное преобразование, расщепление, свертка программы. Посредством данных преобразований исходная тройка модифицируется и в конечном счете сводится к набору формул на языке спецификации, истинность которых будет свидетельствовать о корректности программы. Предложена архитектура системы поддержки формальной верификации функционально-потоковых параллельных программ, которая позволяет строить дерево доказательства. Представлена реализация этой системы, описана ее основная функциональность.
Функционально-потоковое параллельное программирование, язык программирования пифагор, верификация программ, инструментальные средства для поддержки формальной верификации
Короткий адрес: https://sciup.org/147160564
IDR: 147160564 | DOI: 10.14529/cmse150205
Список литературы Инструментальная поддержка формальной верификации программ, написанных на языке функционально-потокового параллельного программирования
- Непомнящий, В.А. Прикладные методы верификации программ/В.А. Непомнящий, О.М. Рякин -М.: Радио и связь, 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. DOI: DOI: 10.1145/363235.363259
- 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. DOI: DOI: 10.1007/11804192_17
- Непомнящий, В.А. Верификация C-программ в мультиязыковой системе СПЕКТР/В.А. Непомнящий, И.С. Ануреев, М.М. Атучин, И.В. Марьясов, А.А. Петров, А.В. Промский//Моделирование и анализ информационных систем. -2010. -№ 17 (4). -С. 88-100. DOI: DOI: 10.3103/s014641161107011x
- 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. 2015, т. 4, № 2. -P. 299-312. DOI: DOI: 10.1007/3-540-45319-9_21
- 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. DOI: DOI: 10.1007/s10270-004-0058-x
- Легалов, А.И. На пути к переносимым параллельным программам/А.И. Легалов, Д.А. Кузьмин, Ф.А. Казаков, Д.В. Привалихин//Открытые системы. -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. DOI: DOI: 10.1007/978-3-642-39958-9_7
- Кропачева, М.С. Формализация семантики функционально-потокового языка параллельного программирования Пифагор/М.С. Кропачева//Проблемы информатизации региона (ПИР-2011): Материалы XII Всероссийской научно-практической конференции (Красноярск, 22 -23 ноября 2011 г.). -Красноярск: Сибирский федеральный университет, 2011. -С. 144-148.
- Матковский, И.В. Параллельная событийная машина для функционально-потокового языка «Пифагор»/И.В. Матковский//Информационные и математические технологии в науке и управлении: Сборник трудов XVVII Байкальской Всероссийской конференции с международным участием (Иркутск -Байкал, 30 июня -9 июля 2012 г.). Часть II. -Иркутск: ИСЭМ СО РАН, 2012. -С. 186-193.
- Легалов, А.И. Событийная модель вычислений, поддерживающая выполнение функционально-потоковых параллельных программ/А.И. Легалов, Г.В. Савченко, В.С. Васильев//Системы. Методы. Технологии. -2012. -№ 1 (13). -С. 113-119.
