WCET Analysis of Java Bytecode Featuring Common Execution Environments
Authors
Frost, Christian ; Jensen, Casper Svenning ; Luckow, Kasper Søe
Term
4. term
Education
Publication year
2011
Submitted on
2011-06-07
Pages
158
Abstract
Vi præsenterer TetaJ, et værktøj til statisk at bestemme Worst Case Execution Time (WCET) for Java-bytecodeprogrammer. WCET er en sikker øvre grænse for, hvor lang tid et program kan bruge i værste fald, og er afgørende i hard realtidssystemer, hvor deadlines ikke må overskrides. Tidligere løsninger enten måler kørselstider (hvilket kan være usikkert) eller kræver hardware, der kan køre Java-bytecode direkte. TetaJ adskiller sig ved at bygge på en softwarebaseret Java Virtual Machine (JVM), så analysen kan udføres på almindelige indlejrede processorer. Kernen i TetaJ er at se WCET-bestemmelse som et modelkontrolproblem (model-checking). TetaJ genskaber kontrolflowgrafer (CFG) for både JVM-eksekveringen og Java-bytecoden—et kort over alle mulige forløb i koden. Disse grafer omdannes derefter til et netværk af tidsautomater, matematiske modeller med ure, som kan analyseres af UPPAAL, et førende verifikationsværktøj. UPPAAL udforsker alle relevante stier for at beregne den værste kørselstid. For at vurdere anvendeligheden gennemfører vi et casestudie på det klassiske minepumpe-realtidssystem i et miljø med Hardware near Virtual Machine (HVM), en konkret JVM-implementering, der kører på en Atmel AVR ATmega2560-processor. Vi konkluderer, at TetaJ kan estimere sikre WCET’er med rimelig præcision. Selvom vi kun viser ét casestudie, understreges det, at tilgangen gælder for vilkårlig hardware og fortolkende JVM’er.
We introduce TetaJ, a tool for statically determining the Worst Case Execution Time (WCET) of Java bytecode programs. WCET is a safe upper bound on how long code can take in the worst case, which is essential for hard real-time systems that must never miss deadlines. Previous approaches either rely on measurement (which can be unsafe) or require hardware that executes Java bytecode natively. TetaJ instead uses a software implementation of the Java Virtual Machine (JVM), enabling analysis on common embedded processors. The key idea is to treat WCET analysis as a model-checking problem. TetaJ reconstructs control flow graphs (CFGs) for both the JVM execution and the Java bytecode—a map of all possible paths the code can take. It then transforms these graphs into a network of timed automata, mathematical models with clocks, which can be analyzed by UPPAAL, a state-of-the-art verification tool. UPPAAL explores all relevant paths to compute the worst-case time. To evaluate TetaJ, we conduct a case study on the classic mine pump real-time system using Hardware near Virtual Machine (HVM), a concrete JVM implementation, running on an Atmel AVR ATmega2560 processor. From this study we conclude that TetaJ can estimate safe WCETs with reasonable precision. Although demonstrated on a single case, the approach applies to arbitrary hardware and interpretation-based JVMs.
[This abstract was generated with the help of AI]
Documents