maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2015-4-578-589mais-274Research ArticleОригинальные статьиArticlesАвтоматизация формальной верификации программ на языке ПифагорAutomation of Formal Verification of Programs in the Pifagor LanguageУшаковаМ. С.UshakovaM. S.

аспирант

ул. Академика Киренского, 26, г. Красноярск, 660074 Россия

 graduate student

26 Kirenskogo street, Krasnoyarsk, 660074, Russia

ksv@akadem.ruЛегаловА. И.LegalovA. I.

д-р техн. наук, профессор, заведующий кафедрой вычислительной техники

ул. Академика Киренского, 26, г. Красноярск, 660074

PhD

26 Kirenskogo street, Krasnoyarsk, 660074, Russia

legalov@mail.ruИнститут космических и информационных технологий, Сибирский федеральный университетРоссияSiberian Federal University, Institute of Space and Information TechnologyRussian Federation201520082015224578589Copyright © Ушакова М.С., Легалов А.И., 20152015Ушакова М.С., Легалов А.И.Ushakova M.S., Legalov A.I.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/274

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

Nowadays, due to software sophistication, programs correctness is more often proved by means of formal verification. The method of deduction based on Hoare logic could be used for any programminglanguage and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for verification of parallel programs because of high complexity of theprocess. The usage of the functional data-flow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-flow parallel programs in the Pifagor language is considered. The proof process of a program correctness 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 program data-flow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-flow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-flow graph is transformed and finally is reduced to a set of formulas in the specification language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: “Program correctness prover”, “Axioms and theorems library management system” and “Errors analysis and output of information about errors”. According to this architecture, the toolkit for supporting formal verification was developed. The main functionality of the system implementation is considered.

функционально-потоковое параллельное программированиеязык программирования Пифагорформальная верификация программинструментальные средства для поддержки формальной верификацииfunctional data-flow parallel programmingPifagor programming languageprograms formal verificationtoolkit for supporting formal verificationReferencesNepomnyaschiy V. A., Ryakin O. M., Prikladnyie metodyi verifikatsii programm, Radio i svyaz, Moscow, 1988, 255 pp., [in Russian].Nepomnyaschiy V. A., Ryakin O. M., Prikladnyie metodyi verifikatsii programm, Radio i svyaz, Moscow, 1988, 255 pp., [in Russian].Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 10:12 (1969), 576–585.Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 10:12 (1969), 576–585.Floyd R. W., “Assigning meaning to programs”, Mathematical Aspects of Computer Science, ed. J. T. Schwartz, 1967, 19–32.Floyd R. W., “Assigning meaning to programs”, Mathematical Aspects of Computer Science, ed. J. T. Schwartz, 1967, 19–32.Barnett M., Chang B. Y. E., Deline R., et al., “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, LNCS, 4111, 2006, 364–387.Barnett M., Chang B. Y. E., Deline R., et al., “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, LNCS, 4111, 2006, 364–387.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.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.Van den Berg J., Jacobs B., “The LOOP compiler for Java and JML”, LNCS, 2031, 2001, 299–312.Van den Berg J., Jacobs B., “The LOOP compiler for Java and JML”, LNCS, 2031, 2001, 299–312.Ahrendt W., Baar T., Beckert B., “The KeY Tool”, Software and System Modeling, 4:1 (2005), 32–54.Ahrendt W., Baar T., Beckert B., “The KeY Tool”, Software and System Modeling, 4:1 (2005), 32–54.Detlefs D., Nelson G., Saxe J. B., “Simplify: a theorem prover for program checking”, Journal of the ACM, 52:3 (2005), 365–473.Detlefs D., Nelson G., Saxe J. B., “Simplify: a theorem prover for program checking”, Journal of the ACM, 52:3 (2005), 365–473.Owre S., Rajan S., Rushby J. M., “PVS: Combining Specification, Proof Checking, and Model Checking”, LNCS, 1102, 1996, 411–414.Owre S., Rajan S., Rushby J. M., “PVS: Combining Specification, Proof Checking, and Model Checking”, LNCS, 1102, 1996, 411–414.Legalov A. I., “Funktsionalnyiy yazyik dlya sozdaniya arhitekturno-nezavisimyih parallelnyih programm”, Vyichislitelnyie tehnologii, 10:1 (2005), 71–89, [in Russian].Legalov A. I., “Funktsionalnyiy yazyik dlya sozdaniya arhitekturno-nezavisimyih parallelnyih programm”, Vyichislitelnyie tehnologii, 10:1 (2005), 71–89, [in Russian].Legalov A. I., Kuzmin D. A., Kazakov F. A., “Na puti k perenosimyim parallelnyim programmam”, Otkryityie sistemyi, 5 (2003), 36–42, [in Russian].Legalov A. I., Kuzmin D. A., Kazakov F. A., “Na puti k perenosimyim parallelnyim programmam”, Otkryityie sistemyi, 5 (2003), 36–42, [in Russian].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.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.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.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.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].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].The Seventeen Provers of the World, AI Systems, LNAI, 3600, ed. Wiedijk F., 2006, 169 pp.The Seventeen Provers of the World, AI Systems, LNAI, 3600, ed. Wiedijk F., 2006, 169 pp.Gordon M., Melham T., Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, 1993.Gordon M., Melham T., Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, 1993.Bertot Y., Casteran P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, Springer, 2004, 494 pp.Bertot Y., Casteran P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, Springer, 2004, 494 pp.Nipkow T., Paulson L., Wenzel M., Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, 2283, 2002, 205 pp.Nipkow T., Paulson L., Wenzel M., Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, 2283, 2002, 205 pp.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].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].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]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]

The authors declare that there are no conflicts of interest present.