Verifying Automotive Systems in EAST-ADL/Stateflow Using UPPAAL

EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design. We have previously developed a translator, called A-BeTA, transforming timed behavioral constraints in EAST-ADL into the analyzable UPPAAL models. In this paper, we extend the previous work by including support for Stateflow, which is used to design event-driven systems via hierarchical state machines and flow charts. However, Stateflow provides limited support for formal analysis and often suffers from incomplete coverage issues since it was originally designed for the simulation of designs and as such does not provide a model amenable to formal verification. We tackle that shortcoming by transforming Stateflow models into verifiable UPPAAL models and integrating the translation with formal analysis techniques: a flattening strategy is proposed to facilitate the guarantee of translation. Furthermore, a set of mapping rules is presented to ensure the translation is correct, efficient, and applicable to real case studies. The analysis techniques, including the flattening and mapping strategy, are validated and demonstrated on two automotive case studies.