Computing WCET using symbolic execution

We propose a novel formal method to compute an upper estimation of the WCET that contains the loss of precision and also can be easily parametrized by the hardware architecture. Assuming that there exists an executable timed model of the hardware, we first use symbolic execution [5] to precisely infer the execution time for a given instruction flow. We secondly identify execution states that can be merged with no loss of precision. Depending on the loss of precisionwe are ready to accept, we finally merge execution paths that have similar execution times.

Content

Author and article information

Contributors

Bilel Benhamamouch

Bruno Monsuez

Franck Védrine

Conference

Publication date: July 2008

Publication date (Print): July 2008

Pages: 1-12

Affiliations

[0001]UEI, ENSTA, 32 Bd Victor, 75739 Paris cedex 15, France

[0002]CEA, LIST, Boîte 65, Gif-sur-Yvette, F-91191 France

Article

DOI: 10.14236/ewic/VECOS2008.12

SO-VID: 2b4f41b0-a2c7-4182-a09d-9400fad83b63

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)

Conference acronym: VECoS

Conference number:

Conference location: Leeds, UK

Conference date: 2 - 3 July 2008

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Verification and Evaluation of Computer and Communication Systems

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VECOS2008.12

Self URI (journal page): https://ewic.bcs.org/

Studying business & IT? Drive your professional career forwards with BCS books - for a 20% discount click here: shop.bcs.org

Computing WCET using symbolic execution

Abstract