Automatic pattern-based consistency checking in model refactoring: introducing a formal behavioral preserving method

Evolution is one of the most important parts of the software development process. One of the negative consequences of software development is design erosion. Refactoring is a technique that aims to prevent this issue. Therefore, refactoring is an important software development process to promote software quality without changing its external behavior. Refactoring at the model level is the same as refactoring at the code level and has similar advantages, and the only difference is that refactoring at the model level, due to its formation over the initial steps of software development process, has a greater impact on cost reduction and efficiency improvement. Timely and consistent utilization of this procedure in a software project has extremely positive long-term impacts, especially when this is done by its technical tools. Then, refactoring will be a rapid, easy, and safe way to promote software system quality. The main idea of this study is the automatic checking of consistency in model refactoring in order to retain model behavior using Alloy modeling language. Thus, by employing structural and behavioral patterns as a reusable and well-defined component, as well as consistency rules, this objective can be achieved.