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

61 Scopus citations


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.
Number of pages6
ISBN (Print)9781457710957
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


Other2012 American Control Conference, ACC 2012
CityMontreal, QC

ASJC Scopus subject areas

  • Electrical and Electronic Engineering


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

Cite this