Автоматизация формальной верификации программ на языке Пифагор

В связи с увеличением сложности программного обеспечения корректность программы всё
чаще доказывается с помощью методов формальной верификации. Дедуктивный анализ на основе исчисления Хоара применим для произвольных языков программирования и допускает частичную автоматизацию процесса. Однако дедуктивный анализ не нашёл широкого применения для верификации параллельных программ из-за высокой сложности процесса. Использование функционально-потоковой парадигмы параллельного программирования позволяет снизить сложность доказательства. В работе рассматривается процесс доказательства корректности функционально-потоковых параллельных программ на языке Пифагор и предлагается архитектура инструментального средства для поддержки процесса доказательства. Процесс доказательства корректности программы представляется в виде дерева, каждый узел которого — информационный граф программы, в котором дуги размечены формулами на языке спецификации. Корнем дерева является информационный граф программы с предусловием и постусловием, которые описывают ограничения на входные переменные и условия корректности результата работы программы соответственно. Основные преобразования, применимые к информационному графу программы: разметка дуг, эквивалентное преобразование, расщепление, свертка программы. Посредством данных преобразований информационный граф модифицируется и, в конечном счете, сводится к набору формул на языке спецификации, истинность которых будет свидетельствовать о корректности программы. Предложена архитектура системы поддержки процесса доказательства, которая позволяет строить дерево доказательства. В системе выделено несколько основных модулей: «Модуль доказательства корректности программы», «Система управления библиотекой аксиом и теорем» и «Модуль анализа ошибок и выдачи информации об ошибках». Согласно описанной архитектуре, разработано инструментальное средство для поддержки формальной верификации, которая позволяет строить дерево доказательства. Описана основная функциональность реализации системы.

1. Nepomnyaschiy V. A., Ryakin O. M., Prikladnyie metodyi verifikatsii programm, Radio i svyaz, Moscow, 1988, 255 pp., [in Russian].

2. Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 10:12 (1969), 576–585.

3. Floyd R. W., “Assigning meaning to programs”, Mathematical Aspects of Computer Science, ed. J. T. Schwartz, 1967, 19–32.

4. Barnett M., Chang B. Y. E., Deline R., et al., “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, LNCS, 4111, 2006, 364–387.

5. Nepomniaschy V. A., Anureev I. S., Atuchin M. M., “C Program Verification in SPECTRUM Multilanguage System”, Automatic Control and Computer Sciences, 45:7 (2011), 413–420.

6. Van den Berg J., Jacobs B., “The LOOP compiler for Java and JML”, LNCS, 2031, 2001, 299–312.

7. Ahrendt W., Baar T., Beckert B., “The KeY Tool”, Software and System Modeling, 4:1 (2005), 32–54.

8. Detlefs D., Nelson G., Saxe J. B., “Simplify: a theorem prover for program checking”, Journal of the ACM, 52:3 (2005), 365–473.

9. Owre S., Rajan S., Rushby J. M., “PVS: Combining Specification, Proof Checking, and Model Checking”, LNCS, 1102, 1996, 411–414.

10. Legalov A. I., “Funktsionalnyiy yazyik dlya sozdaniya arhitekturno-nezavisimyih parallelnyih programm”, Vyichislitelnyie tehnologii, 10:1 (2005), 71–89, [in Russian].

11. Legalov A. I., Kuzmin D. A., Kazakov F. A., “Na puti k perenosimyim parallelnyim programmam”, Otkryityie sistemyi, 5 (2003), 36–42, [in Russian].

12. Kropacheva M. S., Legalov A. I., “Formal Verification of Programs in the Functional Data-Flow Parallel Language”, Automatic Control and Computer Sciences, 47:7 (2013), 373–384.

13. Kropacheva M. S., Legalov A. I., “Formal Verification of Programs in the Pifagor Language”, Parallel Computing Technologies (PaCT-2013), 12th International Conference (September 30 - October 4, 2013. Saint-Petersburg, Russia), LNCS, 7979, 2013, 80–89.

14. Kropacheva M. S., “Formalizatsiya semantiki funktsionalno-potokovogo yazyika parallelnogo programmirovaniya Pifagor”, Problemyi informatizatsii regiona (PIR-2011): Materialyi XII Vserossiyskoy nauchno-prakticheskoy konferentsii (Krasnoyarsk, 22 – 23 noyabrya 2011), Publishing of the Siberian Federal University, Krasnoyarsk, 2011, 144–148, [in Russian].

15. The Seventeen Provers of the World, AI Systems, LNAI, 3600, ed. Wiedijk F., 2006, 169 pp.

16. Gordon M., Melham T., Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, 1993.

17. Bertot Y., Casteran P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, Springer, 2004, 494 pp.

18. Nipkow T., Paulson L., Wenzel M., Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, 2283, 2002, 205 pp.

19. Legalov A. I., Savchenko G. V., Vasilev V. S., “Sobyitiynaya model vyichisleniy, podderzhivayuschaya vyipolnenie funktsionalno-potokovyih parallelnyih programm”, Sistemyi. Metodyi. Tehnologii, 1:13 (2012), 113–119, [in Russian].

20. Matkovskiy I. V., “Parallelnaya sobyitiynaya mashina dlya funktsionalno-potokovogo yazyika “Pifagor””, Informatsionnyie i matematicheskie tehnologii v nauke i upravlenii: Sbornik trudov XVVII Baykalskoy Vserossiyskoy konferentsii s mezhdunarodnyim uchastiem (Irkutsk – Baykal, 30 iyunya – 9 iyulya 2012), 2, Publishing of the Melentiev Energy Systems Institute of Siberian Branch of the Russian Academy of Sciences, Irkutsk, 2012, 186–193, [in Russian]