SpideyBC: Static Resource Analysis of Safety-Critical Java Applications
Authors
Todberg, Mikkel ; Andersen, Jeppe Lund
Term
4. term
Education
Publication year
2013
Submitted on
2013-05-31
Pages
91
Abstract
I sikkerhedskritiske og indlejrede systemer skal udviklere ofte på forhånd angive, hvor meget hukommelse deres program kan bruge. Vores tidligere arbejde med et SCJ-specifikationsudkast fra 2012 og en niveau 1-kompatibel use-case-bibliotek for CubeSat Space Protocol viste, at det er svært – især for nye SCJ-brugere – at vælge de rigtige lagerparametre. I denne rapport præsenterer vi SpideyBC, et statisk analyseværktøj, der uden at køre programmet estimerer maksimal dynamisk hukommelsesallokering og værst tænkeligt JVM-stakforbrug for udvalgte Java-metoder, fx handleAsyncEvent. Værktøjet bygger på veletablerede principper fra statisk programanalyse og tilpasser teknikker kendt fra WCET (Worst-Case Execution Time), herunder Implicit Path Enumeration Technique (IPET), til at gennemgå mulige eksekveringsforløb og afgrænse ressourceforbrug. SpideyBC genererer en rapport med overskuelige visualiseringer af værst mulige forløb, kaldgrafer, kontrolflowgrafer og stakoplysninger. Derudover opgør værktøjet allokeringer i SCJ’s hukommelsesområder – private, mission og immortal – for at indikere den værst tænkelige størrelse, hvert område kan kræve. Samlet hjælper SpideyBC udviklere med at vælge passende lagerparametre for en SCJ-applikation.
In safety-critical and embedded systems, developers often have to declare memory limits up front. In our earlier work on a 2012 draft of the Safety-Critical Java (SCJ) specification and a level 1 compliant CubeSat Space Protocol use-case library, we found that choosing correct storage parameters is difficult, especially for newcomers. This report introduces SpideyBC, a static analysis tool that estimates, without executing the program, the maximum dynamic memory allocation and worst-case Java Virtual Machine (JVM) stack usage for selected Java methods, such as handleAsyncEvent. The tool relies on established ideas from static program analysis and adapts techniques from worst-case execution time (WCET) analysis, including the Implicit Path Enumeration Technique (IPET), to reason about possible execution paths and bound resource use. SpideyBC produces a report with clear visualizations of worst-case paths, call graphs, control-flow graphs, and stack information. It also accounts for allocations in SCJ’s memory areas—private, mission, and immortal—to indicate the worst-case size each region may need. Together, these results help developers choose appropriate storage parameters for an SCJ application.
[This abstract was generated with the help of AI]
Keywords
Documents