Counterexample-guided inference of controller logic from execution traces and temporal formulas Show others and affiliations
2018 (English) In: 2018 IEEE 23RD INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), Piscataway, NJ: IEEE, 2018, p. 91-98Conference paper, Published paper (Refereed)
Abstract [en]
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.
Place, publisher, year, edition, pages Piscataway, NJ: IEEE, 2018. p. 91-98
Series
IEEE International Conference on Emerging Technologies and Factory Automation-ETFA, ISSN 1946-0740
National Category
Computer Sciences
Research subject Dependable Communication and Computation Systems
Identifiers URN: urn:nbn:se:ltu:diva-72534 DOI: 10.1109/ETFA.2018.8502463 ISI: 000449334500010 Scopus ID: 2-s2.0-85057249596 ISBN: 978-1-5386-7108-5 (print) OAI: oai:DiVA.org:ltu-72534 DiVA, id: diva2:1278300
Conference 23rd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2018) Politecnico Torino,Italy , Sep 04-07, 2018
2019-01-142019-01-142019-01-14 Bibliographically approved