Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Computing WCET using symbolic execution

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

    Leeds, UK, 2 - 3 July 2008


    Bilel Benhamamouch, Bruno Monsuez and Franck Védrine


    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.


    PDF filePDF Version of this Paper (134 kb)