Formal Verification of Programs in Functional Dataflow Parallel Language
https://doi.org/10.18255/1818-1015-2012-5-81-99
Abstract
The article is devoted to the methods of proving parallel programs correctness that are based on the axiomatic approach. Formal system for functional data-flow parallel programming language Pifagor is described. On the basis of this system programs correctness could be proved.
About the Authors
M. S. Kropacheva
Сибирский федеральный университет
Russian Federation
Russian Federation
аспирант
A. I. Legalov
Сибирский федеральный университет
Russian Federation
профессор
Russian Federation
профессор
References
1. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988. 255 с.
2. Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. Vol. 10. N. 12. P. 576–585.
3. Ануреев И. С., Марьясов И. В., Непомнящий В. А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, № 3. C. 5–28.
4. Легалов А.И. Функциональный язык для создания архитектурно-независимых параллельных программ // Вычислительные технологии. 2005. № 1 (10). С. 71–89.
5. Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Методы отладки и верификации функционально-потоковых параллельных программ // Журнал Сибирского федерального университета. Серия: Техника и технологии. 2011. Т. 4. № 2. С. 213–224.
6. Легалов А.И., Казаков Ф.А., Кузьмин Д.А., Привалихин Д.В. Функциональная модель параллельных вычислений и язык программирования «Пифагор»: ttp://www.softcraft.ru/fppp.shtml
7. Легалов А.И. Использование асинхронно поступающих данных в потоковой модели вычислений / Третья сибирская школа-семинар по параллельным вычислениям. Томск: Изд-во Томского ун-та, 2006. С. 113–120.
8. Кропачева М.С. Формализация семантики функционально-потокового языка параллельного программирования Пифагор // Проблемы информатизации региона. ПИР-2011: Материалы XII Всероссийской научно-практической конференции. Красноярск: Сибирский федеральный университет. 2011. С. 144–148.
9. Чень Л. Математическая логика и автоматическое доказательство теорем / Под ред. С.Ю. Маслова. М.: Наука, 1983. 358 с.
10. Harrison J. Handbook Of Practical Logic And Automated Reasoning New York: Cambridge University Press, 2009. 781 p.
Review
For citations:
Kropacheva M.S., Legalov A.I. Formal Verification of Programs in Functional Dataflow Parallel Language. Modeling and Analysis of Information Systems. 2012;19(5):81-99. (In Russ.) https://doi.org/10.18255/1818-1015-2012-5-81-99
Views:
978
Email this article 