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

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

Researchers

Research units

  • St. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)
  • Luleå University of Technology

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.

Details

Original languageEnglish
Title of host publicationProceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018
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

    Research areas

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

ID: 30294700