Academic Journal
أعرض في EDS

Automation of Formal Verification of Programs in the Pifagor Language ; Автоматизация формальной верификации программ на языке Пифагор

التفاصيل البيبلوغرافية
العنوان: Automation of Formal Verification of Programs in the Pifagor Language ; Автоматизация формальной верификации программ на языке Пифагор
المؤلفون: M. S. Ushakova, A. I. Legalov, М. С. Ушакова, А. И. Легалов
المصدر: Modeling and Analysis of Information Systems; Том 22, № 4 (2015); 578-589 ; Моделирование и анализ информационных систем; Том 22, № 4 (2015); 578-589 ; 2313-5417 ; 1818-1015
بيانات النشر: Yaroslavl State University
سنة النشر: 2015
المجموعة: Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
مصطلحات موضوعية: инструментальные средства для поддержки формальной верификации, Pifagor programming language, programs formal verification, toolkit for supporting formal verification, язык программирования Пифагор, формальная верификация программ
الوصف: 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. ; В связи с увеличением сложности программного обеспечения корректность программы всёчаще доказывается с помощью методов формальной верификации. Дедуктивный анализ на основе исчисления Хоара применим для произвольных языков программирования и допускает частичную автоматизацию процесса. Однако дедуктивный ...
نوع الوثيقة: article in journal/newspaper
وصف الملف: application/pdf
اللغة: Russian
Relation: https://www.mais-journal.ru/jour/article/view/274/283; 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.; 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.; 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.; 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.; 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., 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 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].; 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.; 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.; 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]; https://www.mais-journal.ru/jour/article/view/274
DOI: 10.18255/1818-1015-2015-4-578-589
الاتاحة: https://www.mais-journal.ru/jour/article/view/274
https://doi.org/10.18255/1818-1015-2015-4-578-589
Rights: Authors who publish with this journal agree to the following terms:Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access). ; Авторы, публикующие статьи в данном журнале, соглашаются на следующее:Авторы сохраняют за собой авторские права и предоставляют журналу право первой публикации работы, которая после публикации автоматически лицензируется на условиях Creative Commons Attribution License , которая позволяет другим распространять данную работу с обязательным сохранением ссылок на авторов оригинальной работы и оригинальную публикацию в этом журнале.Авторы имеют право размещать их работу в сети Интернет (например в институтском хранилище или персональном сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению и большему количеству ссылок на данную работу (См. The Effect of Open Access).
رقم الانضمام: edsbas.C9D69E5B
قاعدة البيانات: BASE
ResultId 1
Header edsbas
BASE
edsbas.C9D69E5B
856
3
Academic Journal
academicJournal
855.848266601563
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&scope=site&db=edsbas&AN=edsbas.C9D69E5B&custid=s6537998&authtype=sso
FullText Array ( [Availability] => 0 )
Array ( [0] => Array ( [Url] => https://www.mais-journal.ru/jour/article/view/274# [Name] => EDS - BASE [Category] => fullText [Text] => View record in BASE [MouseOverText] => View record in BASE ) )
Items Array ( [Name] => Title [Label] => Title [Group] => Ti [Data] => Automation of Formal Verification of Programs in the Pifagor Language ; Автоматизация формальной верификации программ на языке Пифагор )
Array ( [Name] => Author [Label] => Authors [Group] => Au [Data] => <searchLink fieldCode="AR" term="%22M%2E+S%2E+Ushakova%22">M. S. Ushakova</searchLink><br /><searchLink fieldCode="AR" term="%22A%2E+I%2E+Legalov%22">A. I. Legalov</searchLink><br /><searchLink fieldCode="AR" term="%22М%2E+С%2E+Ушакова%22">М. С. Ушакова</searchLink><br /><searchLink fieldCode="AR" term="%22А%2E+И%2E+Легалов%22">А. И. Легалов</searchLink> )
Array ( [Name] => TitleSource [Label] => Source [Group] => Src [Data] => Modeling and Analysis of Information Systems; Том 22, № 4 (2015); 578-589 ; Моделирование и анализ информационных систем; Том 22, № 4 (2015); 578-589 ; 2313-5417 ; 1818-1015 )
Array ( [Name] => Publisher [Label] => Publisher Information [Group] => PubInfo [Data] => Yaroslavl State University )
Array ( [Name] => DatePubCY [Label] => Publication Year [Group] => Date [Data] => 2015 )
Array ( [Name] => Subset [Label] => Collection [Group] => HoldingsInfo [Data] => Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС) )
Array ( [Name] => Subject [Label] => Subject Terms [Group] => Su [Data] => <searchLink fieldCode="DE" term="%22инструментальные+средства+для+поддержки+формальной+верификации%22">инструментальные средства для поддержки формальной верификации</searchLink><br /><searchLink fieldCode="DE" term="%22Pifagor+programming+language%22">Pifagor programming language</searchLink><br /><searchLink fieldCode="DE" term="%22programs+formal+verification%22">programs formal verification</searchLink><br /><searchLink fieldCode="DE" term="%22toolkit+for+supporting+formal+verification%22">toolkit for supporting formal verification</searchLink><br /><searchLink fieldCode="DE" term="%22язык+программирования+Пифагор%22">язык программирования Пифагор</searchLink><br /><searchLink fieldCode="DE" term="%22формальная+верификация+программ%22">формальная верификация программ</searchLink> )
Array ( [Name] => Abstract [Label] => Description [Group] => Ab [Data] => 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. ; В связи с увеличением сложности программного обеспечения корректность программы всёчаще доказывается с помощью методов формальной верификации. Дедуктивный анализ на основе исчисления Хоара применим для произвольных языков программирования и допускает частичную автоматизацию процесса. Однако дедуктивный ... )
Array ( [Name] => TypeDocument [Label] => Document Type [Group] => TypDoc [Data] => article in journal/newspaper )
Array ( [Name] => Format [Label] => File Description [Group] => SrcInfo [Data] => application/pdf )
Array ( [Name] => Language [Label] => Language [Group] => Lang [Data] => Russian )
Array ( [Name] => NoteTitleSource [Label] => Relation [Group] => SrcInfo [Data] => https://www.mais-journal.ru/jour/article/view/274/283; 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.; 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.; 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.; 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.; 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., 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 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].; 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.; 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.; 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]; https://www.mais-journal.ru/jour/article/view/274 )
Array ( [Name] => DOI [Label] => DOI [Group] => ID [Data] => 10.18255/1818-1015-2015-4-578-589 )
Array ( [Name] => URL [Label] => Availability [Group] => URL [Data] => https://www.mais-journal.ru/jour/article/view/274<br />https://doi.org/10.18255/1818-1015-2015-4-578-589 )
Array ( [Name] => Copyright [Label] => Rights [Group] => Cpyrght [Data] => Authors who publish with this journal agree to the following terms:Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access). ; Авторы, публикующие статьи в данном журнале, соглашаются на следующее:Авторы сохраняют за собой авторские права и предоставляют журналу право первой публикации работы, которая после публикации автоматически лицензируется на условиях Creative Commons Attribution License , которая позволяет другим распространять данную работу с обязательным сохранением ссылок на авторов оригинальной работы и оригинальную публикацию в этом журнале.Авторы имеют право размещать их работу в сети Интернет (например в институтском хранилище или персональном сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению и большему количеству ссылок на данную работу (См. The Effect of Open Access). )
Array ( [Name] => AN [Label] => Accession Number [Group] => ID [Data] => edsbas.C9D69E5B )
RecordInfo Array ( [BibEntity] => Array ( [Identifiers] => Array ( [0] => Array ( [Type] => doi [Value] => 10.18255/1818-1015-2015-4-578-589 ) ) [Languages] => Array ( [0] => Array ( [Text] => Russian ) ) [Subjects] => Array ( [0] => Array ( [SubjectFull] => инструментальные средства для поддержки формальной верификации [Type] => general ) [1] => Array ( [SubjectFull] => Pifagor programming language [Type] => general ) [2] => Array ( [SubjectFull] => programs formal verification [Type] => general ) [3] => Array ( [SubjectFull] => toolkit for supporting formal verification [Type] => general ) [4] => Array ( [SubjectFull] => язык программирования Пифагор [Type] => general ) [5] => Array ( [SubjectFull] => формальная верификация программ [Type] => general ) ) [Titles] => Array ( [0] => Array ( [TitleFull] => Automation of Formal Verification of Programs in the Pifagor Language ; Автоматизация формальной верификации программ на языке Пифагор [Type] => main ) ) ) [BibRelationships] => Array ( [HasContributorRelationships] => Array ( [0] => Array ( [PersonEntity] => Array ( [Name] => Array ( [NameFull] => M. S. Ushakova ) ) ) [1] => Array ( [PersonEntity] => Array ( [Name] => Array ( [NameFull] => A. I. Legalov ) ) ) [2] => Array ( [PersonEntity] => Array ( [Name] => Array ( [NameFull] => М. С. Ушакова ) ) ) [3] => Array ( [PersonEntity] => Array ( [Name] => Array ( [NameFull] => А. И. Легалов ) ) ) ) [IsPartOfRelationships] => Array ( [0] => Array ( [BibEntity] => Array ( [Dates] => Array ( [0] => Array ( [D] => 01 [M] => 01 [Type] => published [Y] => 2015 ) ) [Identifiers] => Array ( [0] => Array ( [Type] => issn-locals [Value] => edsbas ) [1] => Array ( [Type] => issn-locals [Value] => edsbas.oa ) ) [Titles] => Array ( [0] => Array ( [TitleFull] => Modeling and Analysis of Information Systems; Том 22, № 4 (2015); 578-589 ; Моделирование и анализ информационных систем; Том 22, № 4 (2015); 578-589 [Type] => main ) ) ) ) ) ) )
IllustrationInfo