Querying parametric temporal logic properties on embedded systems

Hengyi Yang, Bardh Hoxha, Georgios Fainekos

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

33 Scopus citations

Abstract

In Model Based Development (MBD) of embedded systems, it is often desirable to not only verify/falsify certain formal system specifications, but also to automatically explore the properties that the system satisfies. Namely, given a parametric specification, we would like to automatically infer the ranges of parameters for which the property holds/does not hold on the system. In this paper, we consider parametric specifications in Metric Temporal Logic (MTL). Using robust semantics for MTL, the parameter estimation problem can be converted into an optimization problem which can be solved by utilizing stochastic optimization methods. The framework is demonstrated on some examples from the literature.

Original languageEnglish (US)
Title of host publicationTesting Software and Systems - 24th IFIP WG 6.1 International Conference, ICTSS 2012, Proceedings
Pages136-151
Number of pages16
DOIs
StatePublished - 2012
Event24th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2012 - Aalborg, Denmark
Duration: Nov 19 2012Nov 21 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7641 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other24th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2012
Country/TerritoryDenmark
CityAalborg
Period11/19/1211/21/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Querying parametric temporal logic properties on embedded systems'. Together they form a unique fingerprint.

Cite this