License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2015.95
URN: urn:nbn:de:0030-drops-52604
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5260/
Go to the corresponding OASIcs Volume Portal

Ruiz, Jordy ; Cassé, Hugues

Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs

pdf-format:
11.pdf (0.5 MB)

Abstract

Worst-Case Execution Time (WCET) is a key component to check temporal constraints of realtime systems. WCET by static analysis provides a safe upper bound. While hardware modelling is now efficient, loss of precision stems mainly in the inclusion of infeasible execution paths in the WCET calculation. This paper proposes a new method to detect such paths based on static analysis of machine code and the feasibility test of conditions using Satisfiability Modulo Theory (SMT) solvers. The experimentation shows promising results although the expected precision was slightly lowered due to clamping operations needed to cope with complexity explosion. An important point is that the implementation has been performed in the OTAWA framework and is independent of any instruction set thanks to its semantic instructions.

BibTeX - Entry

@InProceedings{ruiz_et_al:OASIcs:2015:5260,
  author =	{Jordy Ruiz and Hugues Cass{\'e}},
  title =	{{Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs}},
  booktitle =	{15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
  pages =	{95--104},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-95-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{47},
  editor =	{Francisco J. Cazorla},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5260},
  URN =		{urn:nbn:de:0030-drops-52604},
  doi =		{10.4230/OASIcs.WCET.2015.95},
  annote =	{Keywords: WCET, infeasible paths, SMT, machine code}
}

Keywords: WCET, infeasible paths, SMT, machine code
Collection: 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)
Issue Date: 2015
Date of publication: 06.07.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI