Verification of automotive control applications using S-TaLiRo

Georgios Fainekos, Sriram Sankaranarayanan, Koichi Ueda, Hakan Yazarel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

46 Scopus citations

Abstract

S-TALIRO is a software toolbox that performs stochastic search for system trajectories that falsify realtime temporal logic specifications. S-TaLiRo is founded on the notion of robustness of temporal logic specifications. In this paper, we present a dynamic programming algorithm for computing the robustness of temporal logic specifications with respect to system trajectories. We also demonstrate that typical automotive functional requirements can be captured and falsified using temporal logics and S-TALIRO.

Original languageEnglish (US)
Title of host publication2012 American Control Conference, ACC 2012
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages3567-3572
Number of pages6
ISBN (Print)9781457710957
DOIs
StatePublished - 2012
Event2012 American Control Conference, ACC 2012 - Montreal, QC, Canada
Duration: Jun 27 2012Jun 29 2012

Publication series

NameProceedings of the American Control Conference
ISSN (Print)0743-1619

Other

Other2012 American Control Conference, ACC 2012
CountryCanada
CityMontreal, QC
Period6/27/126/29/12

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Verification of automotive control applications using S-TaLiRo'. Together they form a unique fingerprint.

  • Cite this

    Fainekos, G., Sankaranarayanan, S., Ueda, K., & Yazarel, H. (2012). Verification of automotive control applications using S-TaLiRo. In 2012 American Control Conference, ACC 2012 (pp. 3567-3572). [6315384] (Proceedings of the American Control Conference). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/acc.2012.6315384