Counterexample-guided inference of controller logic from execution traces and temporal formulas

Daniil Chivilikhin, Igor Buzhinskv, Vladimir Ulvantsev, Andrey Stankevich, Anatoly Shalyto, Valeriy Vyatkin

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

1 Citation (Scopus)

Abstract

We developed an algorithm for inferring controller logic for cyber-physical systems (CPS) in the form of a state machine from given execution traces and linear temporal logic formulas. The algorithm implements an iterative counterexample-guided strategy: constraint programming is employed for constructing a minimal state machine from positive and negative traces (counterexamples) while formal verification is used for discovering new counterexamples. The proposed approach extends previous work by (1) considering a more intrinsic model of a state machine making the algorithm applicable to synthesizing CPS controller logic, and (2) using closed-loop verification which allows considering more expressive temporal properties.

Original languageEnglish
Title of host publicationProceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018
PublisherIEEE
Pages91-98
Number of pages8
Volume2018-September
ISBN (Electronic)9781538671085
DOIs
Publication statusPublished - 22 Oct 2018
MoE publication typeA4 Article in a conference publication
EventIEEE International Conference on Emerging Technologies and Factory Automation - Torino, Italy
Duration: 4 Sep 20187 Sep 2018
Conference number: 23

Publication series

NameProceedings IEEE International Conference on Emerging Technologies and Factory Automation
PublisherIEEE
ISSN (Print)1946-0740
ISSN (Electronic)2379-9560

Conference

ConferenceIEEE International Conference on Emerging Technologies and Factory Automation
Abbreviated titleETFA
CountryItaly
CityTorino
Period04/09/201807/09/2018

Keywords

  • input variables
  • programming
  • adaptation models
  • inference algorithms
  • data models
  • iterative algorithms
  • testing

Fingerprint Dive into the research topics of 'Counterexample-guided inference of controller logic from execution traces and temporal formulas'. Together they form a unique fingerprint.

Cite this