Optimizing the Symbolic Execution of Communicating and Evolving State Machines.
Amal Khalil · 2015
This paper describes research investigating two complementary optimization techniques that leverage the similarities between state machines versions to reduce the cost of symbolic execution of the evolved version. I. RESEARCH PROBLEM AND MOTIVATION Model Driven Engineering (MDE) is a model-centric software engineering approach that aims at improving the productivity and the quality of software artifacts by focusing on models as first-class artifacts in place of code. MDE has been widely used for over a decade in many domains such as automotive and telecommunication industries. Iterativeincremental development and model-based analysis are central to MDE in which artifacts typically undergo several iterations and refinements during their lifetime that may require changes to their initial design versions. As these models evolve, it is necessary to assess their quality by repeating the analysis and the verification of these models after every iteration or refinement. This process, if not optimized, can be very tedious and time consuming. The IBM Rational Rhapsody framework [1] is one of the MDE commercial tools that is heavily used in practice (e.g., in the automotive industry). Rhapsody Statecharts (also known as Harel’s Statecharts [2]) are a visual state-based formalism implemented in the IBM Rational Rhapsody framework to describe the behavior of reactive systems. They extend Mealy Machines a type of Finite State Machines (FSMs) that perform their action only on firing transitions with state entry and exit actions and hierarchical composite states with orthogonal regions. Symbolic execution is a well-known analysis technique that systematically explores all possible execution paths of behavioral software artifacts (e.g., programs [3] and statebased models [4, 5]) using symbolic inputs such that we can derive precise characterizations of the circumstances in which a specific path is taken. The output of the analysis is a symbolic execution tree (SET) which provides the basis for various types of analysis and verification, including reachability analysis, guard analysis, invariant checking and instant test case generation. One of the key challenges of symbolic execution is scalability, especially when applied to big, complex artifacts where the size of the output SET becomes very large. Repeating the entire analysis even after small changes is not the best solution. This research introduces two complementary optimization techniques that leverage the similarities between two successive state machine versions to reduce the cost of symbolic execution of the evolved version. This research is motivated by a number of facts. First, symbolic execution has been shown to be a very powerful method for the analysis of programs and there are already several commercial code analysis tools built based on it (e.g., CodeSonar [6]). Similarly, the technique has been adopted and applied in the context of state-based models (e.g., the IAR visualSTATE Verificator [7]). Second, there is an interest from our industrial partner to improve the model-level analysis capabilities of the IBM Rhapsody tool. Third, research on optimizing the symbolic execution of evolving programs has been recently addressed [8, 9], however to the best of knowledge we are the first to consider such optimizations for the symbolic execution of evolving state machines.