Integration of Symbolic Execution into a Formal Abstract State Machines based Language

Hard real-time systems are embedded systems with a strong emphasis on the guaranty of safety-critical properties. In order to provide the necessary confidence level, with regard to the respect of functional and non-functional properties, a system analysis that accounts for all possible execution paths must be performed. Symbolic execution has been successfully used to explore and analyze reachable system states. In this paper, we formally define a symbolic execution semantics for an abstract state machine based model. The unification of the update semantics redefined in terms of symbolic moves, enable us to achieve reacher methods for path condition resolution and ultimately better scalability of the execution. The goal of this paper is to provide a formal ground for the integration of symbolic execution in existing timing analysis frameworks based on abstract state machines that will facilitate the computability of the analysis tools.