Research On Consistency Checking Between Model Refinements

Model refinement is one of the key issues in model-based software engineering, it is widely used in model-driven development methodology. System development and testing would be difficult to manage if bring in too much details in initial model, it is difficult to do in one step for those large and complex systems modeling. Model refinement technology is often used in the actual development of the modeling process. The model refinement is added more details on the basis of the original model, and gradually refined model from the beginning step by step, then the model become more concrete rather than the abstract beginning models. But how to ensure the consistency between model refine has been get high attention of academia and industry.Maintaining the consistency between the system models during refinement process is crucial to a successful software development.In order to ensure the consistency between pre- and after- refinement, it need to checking consistency between them. Identifying the inconsistencies between software models early in software lifecycle would undoubtedly reduce the overall cost, especially when the inconsistencies are carried over to the implementation phase, which would then be very costly to change it. However, during model refinement process, traditional consistency checking techniques tend to focus on the syntax and semantics of the models, their structural correctness, as well as deadlock and invariants retention, while ignoring behavior consistency. However, we believe that inconsistencies between models is often present in all aspects of system behavior. To the best of our knowledge, there has no work specifically targeting on checking the behavior consistency.We assume that the pre-refinement models trustfully represents the stakeholder requirements, while it is sometimes lost or violated during refinement process. Thus this paper captures the system behaviors via the form of system property and utilizing model checking techniques to check the consistencies among system models. Firstly, the pre-refinement model is analyzed and abstract test cases are generated from it, important system behaviors are then extracted as system properties and expressed as linear temporal logic (LTL); Secondly, these system properties are updated based on the refinement relationships, which are extracted between pre-and post-refinement models. Thirdly, the extracted system properties are checked over the post-refinement model. The possible inconsistency positions could be found through the counter-example path. Then iteration to verify the model after modify the inconsistent until post-refinement model meet these system properties.Finally, in order to analyze the effectiveness of the proposed method, we choose three common systems:Celebrity, Kettle, VOBC to consistency checking by artificial injection inconsistent to simulate the inconsistent. Our early experimental results show that most of the inconsistency could be found between pre- and post-refinement models using this approach. So consistency checking between models through system behavior properties is enabling, and this method improves the effectiveness of consistency checking between models.