A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams

Abstract

A model transformation method based on state refinement and semantic mapping is proposed to address the challenges of high modeling complexity and resource consumption in symbolic validation of industrial software requirements. First, a rule-based semantic mapping system is constructed through the explicit definition of element correspondence between statechart components and verification models, coupled with a composite state-level refinement strategy to structurally optimize model hierarchy. Second, an automated transformation algorithm is developed to bridge graphical modeling tools with formal verification environments, supported by quantitative evaluation metrics for mapping validity. To demonstrate its practical applicability, the methodology is systematically applied to railway infrastructure safety—specifically the railroad turnout control system—as a critical case study. The experimental implementation converts operational statecharts of turnout control logic into optimized NuSMV models. Not only did the models remain intact, but the state space was also effectively reduced through the optimization of the hierarchical structure. In the validation phase, the converted model is tested for robustness using the fault injection method, and boundary condition anomalies that are not explicitly stated in the requirement specification are successfully detected. The experimental results show that the validation model generated by this method has improved validation efficiency in the NuSMV tool, which is significantly better than the traditional conversion method.