maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2018-5-465-480mais-752Research ArticleМатериалы конференцииConference PapersУпрощение процесса верификации кибер-физических систем с использованием подхода с графом потока управления в средстве KeYmaeA Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easierhttps://orcid.org/0000-0002-8443-1558БаарТомасBaarThomas

Профессор.

Wilhelminenhofstrasse 75 A, D-12459, Berlin, Germany.

 PhD.

 75 A Wilhelminenhofstrasse, D-12459, Berlin.

thomas.baar@htw-berlin.dehttps://orcid.org/0000-0001-5183-9736СтаролетовСергей МихайловичStaroletovSergey

Канд. физ.-мат. наук, доцент. 

проспект Ленина, 46, г. Барнаул, Алтайский край, 656038.

 PhD.

46 Lenina avenue, Barnaul, Altai region, 656038. 

serg_soft@mail.ruУниверситет прикладных технических и экономических наук г. БерлинаГерманияHochschule für Technik und Wirtschaft Berlin University of Applied SciencesGermanyАлтайский государственный технический университет им. И.И. ПолзуноваРоссияPolzunov Altai State Technical UniversityRussian Federation201828102018255465480Copyright © Баар Т., Старолетов С.М., 20182018Баар Т., Старолетов С.М.Baar T., Staroletov S.Данная работа распространяется под лицензией 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/752

KeYmaera является средством интерактивного доказательства теорем и используется для проверки свойств безопасности кибер-физических систем (CPS). Проверка таких свойств в интерактивном режиме может быть осложнена, поскольку доказательство осуществляется с использованием классического секвентного логического исчисления и успешное доказательство требует от пользователя глубоких знаний о доступных правилах, имеющихся в логике исчисления. Еще одним препятствием для широкого применения KeYmaera является представление текущих целей только в виде текста, что предполагает хорошую подготовку пользователя для построения успешных доказательств. В этой статье мы представляем альтернативный метод верификации для KeYmaera, который значительно повышает удобство использования и минимизирует работу пользователей. Основная идея заключается в том, чтобы позволить пользователю добавлять аннотации в виде инвариантов и контрактов к состояниям гибридной программы. В нашем подходе пользователь может использовать графический язык представления моделируемой системы, что позволяет ему не работать с чисто текстовым форматом гибридных программ, являющимся входным для средства KeYmaera. Исходя из предоставленных пользователем контрактов, можно получать доказательства, которые гораздо проще, чем исходная цель доказательств в KeYmaera, и которые могут быть обработаны в большинстве случаев полностью автоматически. Статья публикуется в авторской редакции.

KeYmaera is an interactive theorem prover and is used to verify safety properties of cyber-physical systems (CPSs). It implements a Dynamic Logic for Hybrid Programs (HPs), while a HP models a CPS very precisely. Verifying properties of a given system in KeYmaera can become a challenge for a user since the proof is authored in a classical sequent calculus framework and a successful proof requires from the user intimate knowledge of the available calculus rules. Another barrier for widespread application of KeYmaera is the purely textual representation of current proof goals, what requires from the user very good training, experience, and patience. In this paper, we present an alternative verification approach based on KeYmaera, which drastically improves usability and minimizes user interaction. The main idea is to let the user annotate invariants and contracts to states of the hybrid automaton. Thus, the user can employ the graphical representation of the modelled system and is not bound to the purely textual form of hybrid programs as in KeYmaera. Based on the user-provided contracts, one can generate proof obligations, which are much simpler than the original proof goal in KeYmaera. The article is published in the authors’ wording.

кибер-физические системыKeYmaeraконтрактыверификациягибридные системыинтерактивные доказатели теоремCPSKeYmaeraproof contractsverificationhybrid systemsusabilityinteractive proversReferencesBaudin P. et al., ACSL: ANSI/ISO C Specification Language. Version 1.12, https:// frama-c.com/download/acsl_1.12.pdf.Baudin P. et al., ACSL: ANSI/ISO C Specification Language. Version 1.12, https:// frama-c.com/download/acsl_1.12.pdf.Spin: Promela reference. float - floating point numbers, http://spinroot.com/spin/Man/ float.html.Spin: Promela reference. float - floating point numbers, http://spinroot.com/spin/Man/ float.html.Alur R. et al., Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems", Hybrid Systems, Lecture Notes in Computer Science, 736, 1993, 209-229, https://doi.org/10.1007/3-540-57318-6_30.Alur R. et al., \Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems", Hybrid Systems, Lecture Notes in Computer Science, 736, 1993, 209-229, https://doi.org/10.1007/3-540-57318-6_30.Behrmann G. et al., "A tutorial on uppaal", Formal methods for the design of real-time systems, Springer, 2004, 200-236.Behrmann G. et al., "A tutorial on uppaal", Formal methods for the design of real-time systems, Springer, 2004, 200-236.Booch G. et al., The unified modeling language user guide - covers UML 2.0, Second Edition, Addison Wesley object technology series, Addison-Wesley, 2005.Booch G. et al., The unified modeling language user guide - covers UML 2.0, Second Edition, Addison Wesley object technology series, Addison-Wesley, 2005.David A. et al., "Uppaal SMC tutorial", International Journal on Software Tools for Technology Transfer, 17:4 (2015), 397-415.David A. et al., "Uppaal SMC tutorial", International Journal on Software Tools for Technology Transfer, 17:4 (2015), 397-415.Floyd R.W., "Assigning Meanings to Programs", Proceedings of Symposium on Applied Mathematics, 19 (1967), 19-32.Floyd R.W., "Assigning Meanings to Programs", Proceedings of Symposium on Applied Mathematics, 19 (1967), 19-32.Hybrid Systems, Lecture Notes in Computer Science, 736, ed. Robert L. Grossman et al., 1993.Hybrid Systems, Lecture Notes in Computer Science, 736, ed. Robert L. Grossman et al., 1993.Henzinger Thomas A., "The Theory of Hybrid Automata", Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996, 278-292.Henzinger Thomas A., "The Theory of Hybrid Automata", Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996, 278-292.Kirchner F. et al., "Frama-C: A software analysis perspective", Formal Aspects of Computing, 27:3 (2015), 573-609.Kirchner F. et al., "Frama-C: A software analysis perspective", Formal Aspects of Computing, 27:3 (2015), 573-609.Nuzzo P. et al., "A platform-based design methodology with contracts and related tools for the design of cyber-physical systems", Proceedings of the IEEE, 103:11 (2015), 2104-2132.Nuzzo P. et al., "A platform-based design methodology with contracts and related tools for the design of cyber-physical systems", Proceedings of the IEEE, 103:11 (2015), 2104-2132.Platzer A., Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, Heidelberg, 2010.Platzer A., Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, Heidelberg, 2010.Platzer A., "Logic and Compositional Verification of Hybrid Systems (Invited Tutorial)", Computer Aided Verification, 23rd International Conference, Lecture Notes in Computer Science, 6806, 2011, 28-43.Platzer A., "Logic and Compositional Verification of Hybrid Systems (Invited Tutorial)", Computer Aided Verification, 23rd International Conference, Lecture Notes in Computer Science, 6806, 2011, 28-43.Quesel J.-D. et al., "How to Model and Prove Hybrid Systemswith KeYmaera:A Tutorial on Safety", STTT, 18:1 (2016), 67-91.Quesel J.-D. et al., "How to Model and Prove Hybrid Systemswith KeYmaera:A Tutorial on Safety", STTT, 18:1 (2016), 67-91.Rümmer Ph., Princess Homepage, http://www.philipp.ruemmer.org/princess.shtml.Rümmer Ph., Princess Homepage, http://www.philipp.ruemmer.org/princess.shtml.

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