Two-Step Deductive Verification of Control Software Using Reflex

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

3 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationPerspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Revised Selected Papers
EditorsNikolaj Bjørner, Irina Virbitskaite, Andrei Voronkov
PublisherSpringer International Publishing AG
Pages50-63
Number of pages14
ISBN (Print)9783030374860
DOIs
Publication statusPublished - 1 Jan 2019
Event12th International Andrei P. Ershov Informatics Conference, PSI 2019 - Novosibirsk, Russian Federation
Duration: 2 Jul 20195 Jul 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11964 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Andrei P. Ershov Informatics Conference, PSI 2019
CountryRussian Federation
CityNovosibirsk
Period02.07.201905.07.2019

Keywords

  • Control software
  • Deductive verification
  • Process-oriented languages
  • Reflex language
  • SMT solver
  • Z3

Fingerprint

Dive into the research topics of 'Two-Step Deductive Verification of Control Software Using Reflex'. Together they form a unique fingerprint.

Cite this