2026-07-23T16:48:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2281 2024-03-06T10:28:34Z ddc:004 open_access

Comparison of Implicit Path Enumeration and Model Checking Based WCET Analysis Huber, Benedikt Schoeberl, Martin WCET analysis model checking IPET Java JOP UPPAAL In this paper, we present our new worst-case execution time (WCET) analysis tool for Java processors, supporting both implicit path enumeration (IPET) and model checking based execution time estimation. Even though model checking is significantly more expensive than IPET, it simplifies accurate modeling of pipelines and caches. Experimental results using the UPPAAL model checker indicate that model checking is fast enough for typical tasks in embedded applications, though large loop bounds may lead to long analysis times. To obtain a tool which is able to cope with larger applications, we recommend to use model checking for more important code fragments, and combine it with the IPET approach. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Huber and Martin Schoeberl 2009 Is Part Of OASIcs, Volume 10, 9th International Workshop on Worst-Case Execution Time Analysis (WCET'09) (2009) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WCET.2009.2281 urn:nbn:de:0030-drops-22810 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2009.2281 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode