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

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

doi:10.1109/ETFA.2018.8502463

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

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

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

2 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Englanti
Otsikko	Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018
Kustantaja	IEEE
Sivut	91-98
Sivumäärä	8
Vuosikerta	2018-September
ISBN (elektroninen)	9781538671085
DOI - pysyväislinkit	https://doi.org/10.1109/ETFA.2018.8502463
Tila	Julkaistu - 22 lokak. 2018
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisussa
Tapahtuma	IEEE International Conference on Emerging Technologies and Factory Automation - Torino, Italia Kesto: 4 syysk. 2018 → 7 syysk. 2018 Konferenssinumero: 23

Julkaisusarja

Nimi	Proceedings IEEE International Conference on Emerging Technologies and Factory Automation
Kustantaja	IEEE
ISSN (painettu)	1946-0740
ISSN (elektroninen)	2379-9560

Conference

Conference	IEEE International Conference on Emerging Technologies and Factory Automation
Lyhennettä	ETFA
Maa/Alue	Italia
Kaupunki	Torino
Ajanjakso	04/09/2018 → 07/09/2018

Pääsy asiakirjaan

10.1109/ETFA.2018.8502463

Muut tiedostot ja linkit

Link to publication in Scopus

Siteeraa tätä

Chivilikhin, D., Buzhinskv, I., Ulvantsev, V., Stankevich, A., Shalyto, A., & Vyatkin, V. (2018). Counterexample-guided inference of controller logic from execution traces and temporal formulas. teoksessa Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018 (Vuosikerta 2018-September, Sivut 91-98). Artikkeli 8502463 (Proceedings IEEE International Conference on Emerging Technologies and Factory Automation). IEEE. https://doi.org/10.1109/ETFA.2018.8502463

Chivilikhin, Daniil ; Buzhinskv, Igor ; Ulvantsev, Vladimir et al. / Counterexample-guided inference of controller logic from execution traces and temporal formulas. Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018. Vuosikerta 2018-September IEEE, 2018. Sivut 91-98 (Proceedings IEEE International Conference on Emerging Technologies and Factory Automation).

@inproceedings{3b35f0d734d24cd1835522f3a6c57657,

title = "Counterexample-guided inference of controller logic from execution traces and temporal formulas",

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.",

keywords = "input variables, programming, adaptation models, inference algorithms, data models, iterative algorithms, testing",

author = "Daniil Chivilikhin and Igor Buzhinskv and Vladimir Ulvantsev and Andrey Stankevich and Anatoly Shalyto and Valeriy Vyatkin",

year = "2018",

month = oct,

day = "22",

doi = "10.1109/ETFA.2018.8502463",

language = "English",

volume = "2018-September",

series = "Proceedings IEEE International Conference on Emerging Technologies and Factory Automation",

publisher = "IEEE",

pages = "91--98",

booktitle = "Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018",

address = "United States",

note = "IEEE International Conference on Emerging Technologies and Factory Automation, ETFA ; Conference date: 04-09-2018 Through 07-09-2018",

}

Chivilikhin, D, Buzhinskv, I, Ulvantsev, V, Stankevich, A, Shalyto, A & Vyatkin, V 2018, Counterexample-guided inference of controller logic from execution traces and temporal formulas. julkaisussa Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018. Vuosikerta 2018-September, 8502463, Proceedings IEEE International Conference on Emerging Technologies and Factory Automation, IEEE, Sivut 91-98, IEEE International Conference on Emerging Technologies and Factory Automation, Torino, Italia, 04/09/2018. https://doi.org/10.1109/ETFA.2018.8502463

Counterexample-guided inference of controller logic from execution traces and temporal formulas. / Chivilikhin, Daniil; Buzhinskv, Igor; Ulvantsev, Vladimir et al.
Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018. Vuosikerta 2018-September IEEE, 2018. s. 91-98 8502463 (Proceedings IEEE International Conference on Emerging Technologies and Factory Automation).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

TY - GEN

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

AU - Chivilikhin, Daniil

AU - Buzhinskv, Igor

AU - Ulvantsev, Vladimir

AU - Stankevich, Andrey

AU - Shalyto, Anatoly

AU - Vyatkin, Valeriy

N1 - Conference code: 23

PY - 2018/10/22

Y1 - 2018/10/22

N2 - 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.

AB - 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.

KW - input variables

KW - programming

KW - adaptation models

KW - inference algorithms

KW - data models

KW - iterative algorithms

KW - testing

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

U2 - 10.1109/ETFA.2018.8502463

DO - 10.1109/ETFA.2018.8502463

M3 - Conference article in proceedings

AN - SCOPUS:85057249596

VL - 2018-September

T3 - Proceedings IEEE International Conference on Emerging Technologies and Factory Automation

SP - 91

EP - 98

BT - Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018

PB - IEEE

T2 - IEEE International Conference on Emerging Technologies and Factory Automation

Y2 - 4 September 2018 through 7 September 2018

ER -

Chivilikhin D, Buzhinskv I, Ulvantsev V, Stankevich A, Shalyto A, Vyatkin V. Counterexample-guided inference of controller logic from execution traces and temporal formulas. julkaisussa Proceedings or the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation, ETFA 2018. Vuosikerta 2018-September. IEEE. 2018. s. 91-98. 8502463. (Proceedings IEEE International Conference on Emerging Technologies and Factory Automation). doi: 10.1109/ETFA.2018.8502463

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

Abstrakti

Julkaisusarja

Conference

Pääsy asiakirjaan

Muut tiedostot ja linkit

Sormenjälki

Siteeraa tätä