Standard

Two-Step Deductive Verification of Control Software Using Reflex. / Anureev, Igor; Garanina, Natalia; Liakh, Tatiana и др.

Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers. ред. / Nikolaj Bjørner; Irina Virbitskaite; Andrei Voronkov. Springer International Publishing AG, 2019. стр. 50-63 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 11964 LNCS).

Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференцийстатья в сборнике материалов конференциинаучнаяРецензирование

Harvard

Anureev, I, Garanina, N, Liakh, T, Rozov, A, Zyubin, V & Gorlatch, S 2019, Two-Step Deductive Verification of Control Software Using Reflex. в N Bjørner, I Virbitskaite & A Voronkov (ред.), Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Том. 11964 LNCS, Springer International Publishing AG, стр. 50-63, 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Novosibirsk, Российская Федерация, 02.07.2019. https://doi.org/10.1007/978-3-030-37487-7_5

APA

Anureev, I., Garanina, N., Liakh, T., Rozov, A., Zyubin, V., & Gorlatch, S. (2019). Two-Step Deductive Verification of Control Software Using Reflex. в N. Bjørner, I. Virbitskaite, & A. Voronkov (Ред.), Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers (стр. 50-63). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 11964 LNCS). Springer International Publishing AG. https://doi.org/10.1007/978-3-030-37487-7_5

Vancouver

Anureev I, Garanina N, Liakh T, Rozov A, Zyubin V, Gorlatch S. Two-Step Deductive Verification of Control Software Using Reflex. в Bjørner N, Virbitskaite I, Voronkov A, Редакторы, Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers. Springer International Publishing AG. 2019. стр. 50-63. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-37487-7_5

Author

Anureev, Igor ; Garanina, Natalia ; Liakh, Tatiana и др. / Two-Step Deductive Verification of Control Software Using Reflex. Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers. Редактор / Nikolaj Bjørner ; Irina Virbitskaite ; Andrei Voronkov. Springer International Publishing AG, 2019. стр. 50-63 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

BibTeX

@inproceedings{ebe3628d26354ff08fb5e2dd97027c40,
title = "Two-Step Deductive Verification of Control Software Using Reflex",
abstract = "In this paper, we introduce a new verification method for control software. The novelty of the method consists in reducing the verification of temporal properties of a control software algorithm to the Hoare-like deductive verification of an imperative program that explicitly models time and the history of the execution of the algorithm. The method is applied to control software specified in Reflex—a domain-specific extension of the C language developed as an alternative to IEC 61131-3 languages. As a process-oriented language, Reflex enables control software description in terms of interacting processes, event-driven operations, and operations with discrete time intervals. The first step of our method rewrites an annotated Reflex program into an equivalent annotated C program. The second step is deductive verification of this C program. We illustrate our method with deductive verification of a Reflex program for a hand dryer device: we provide the source Reflex program, the set of requirements, the resulting annotated C program, the generated verification conditions, and the results of proving these conditions in Z3py – a Python-based front-end to the SMT solver Z3.",
keywords = "Control software, Deductive verification, Process-oriented languages, Reflex language, SMT solver, Z3",
author = "Igor Anureev and Natalia Garanina and Tatiana Liakh and Andrei Rozov and Vladimir Zyubin and Sergei Gorlatch",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-37487-7_5",
language = "English",
isbn = "9783030374860",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer International Publishing AG",
pages = "50--63",
editor = "Nikolaj Bj{\o}rner and Irina Virbitskaite and Andrei Voronkov",
booktitle = "Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers",
address = "Switzerland",
note = "12th International Andrei P. Ershov Informatics Conference, PSI 2019 ; Conference date: 02-07-2019 Through 05-07-2019",

}

RIS

TY - GEN

T1 - Two-Step Deductive Verification of Control Software Using Reflex

AU - Anureev, Igor

AU - Garanina, Natalia

AU - Liakh, Tatiana

AU - Rozov, Andrei

AU - Zyubin, Vladimir

AU - Gorlatch, Sergei

PY - 2019/1/1

Y1 - 2019/1/1

N2 - In this paper, we introduce a new verification method for control software. The novelty of the method consists in reducing the verification of temporal properties of a control software algorithm to the Hoare-like deductive verification of an imperative program that explicitly models time and the history of the execution of the algorithm. The method is applied to control software specified in Reflex—a domain-specific extension of the C language developed as an alternative to IEC 61131-3 languages. As a process-oriented language, Reflex enables control software description in terms of interacting processes, event-driven operations, and operations with discrete time intervals. The first step of our method rewrites an annotated Reflex program into an equivalent annotated C program. The second step is deductive verification of this C program. We illustrate our method with deductive verification of a Reflex program for a hand dryer device: we provide the source Reflex program, the set of requirements, the resulting annotated C program, the generated verification conditions, and the results of proving these conditions in Z3py – a Python-based front-end to the SMT solver Z3.

AB - In this paper, we introduce a new verification method for control software. The novelty of the method consists in reducing the verification of temporal properties of a control software algorithm to the Hoare-like deductive verification of an imperative program that explicitly models time and the history of the execution of the algorithm. The method is applied to control software specified in Reflex—a domain-specific extension of the C language developed as an alternative to IEC 61131-3 languages. As a process-oriented language, Reflex enables control software description in terms of interacting processes, event-driven operations, and operations with discrete time intervals. The first step of our method rewrites an annotated Reflex program into an equivalent annotated C program. The second step is deductive verification of this C program. We illustrate our method with deductive verification of a Reflex program for a hand dryer device: we provide the source Reflex program, the set of requirements, the resulting annotated C program, the generated verification conditions, and the results of proving these conditions in Z3py – a Python-based front-end to the SMT solver Z3.

KW - Control software

KW - Deductive verification

KW - Process-oriented languages

KW - Reflex language

KW - SMT solver

KW - Z3

UR - http://www.scopus.com/inward/record.url?scp=85077497915&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-37487-7_5

DO - 10.1007/978-3-030-37487-7_5

M3 - Conference contribution

AN - SCOPUS:85077497915

SN - 9783030374860

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 50

EP - 63

BT - Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers

A2 - Bjørner, Nikolaj

A2 - Virbitskaite, Irina

A2 - Voronkov, Andrei

PB - Springer International Publishing AG

T2 - 12th International Andrei P. Ershov Informatics Conference, PSI 2019

Y2 - 2 July 2019 through 5 July 2019

ER -

ID: 23122254