Compositional equivalence checking for models and code of control systems

We present CSEC (Compositional Symbolic Equivalence Checker), a tool to perform automatic and compositional equivalence checking of C code against Simulink models. Such equivalence checking is important in model-based development of safety-critical control software in industrial settings, where either the Simulink models are hand-generated to correspond to existing legacy code bases, or the C code is generated from Simulink models using code generators. In the former case, manual translations may not preserve behavior; in the latter case, equivalence checking is necessary to ensure that the code generator has not introduced bugs. CSEC constructs proofs of equivalence of two call graphs compositionally, by constructing a formula that is valid iff two functions are equivalent, when all called functions are assumed equivalent. The validity of the formula is checked using an SMT solver. We have applied CSEC to a module of powertrain controller C code base and the corresponding semi-automatically translated Simulink model at Toyota, and have automatically uncovered several dissimilar behaviors between models and code. We have also applied CSEC to prove equivalence of a Clutch Lockup Model and the automatically generated C code from the model.