Symbolic execution and timed automata model checking for timing analysis of Java real-time systems

摘要

This paper presents SymRT , a tool based on a combination of symbolic execution and real-time model checking for timing analysis of Java systems. Symbolic execution is used for the generation of a safe and tight timing model of the analyzed system capturing the feasible execution paths. The model is combined with suitable execution environment models capturing the timing behavior of the target host platform including the Java virtual machine and complex hardware features such as caching. The complete timing model is a network of timed automata which directly facilitates safe estimates of worst and best case execution time to be determined using the Uppaal model checker. Furthermore, the integration of the proposed techniques into the TetaSARTS tool facilitates reasoning about additional timing properties such as the schedulability of periodically and sporadically released Java real-time tasks (under specific scheduling policies), worst case response time, and more. Keywords WCET analysis Timing analysis Symbolic execution Timed automata Model checking