OR-ATP: An Operation Refinement Approach As a Process of Automatic Theorem Proving

Since it is too difficult to develop a feasible tool to execute the stepwise refinement automatically, the applications of formal methods have mainly been limited to safety critical domains. With the development of the theory and practice of modeling by the integration of UML and formal methods, formal methods usually play a role of representing the behavior models. Thanks to the information provided by the architecture models, such as the concrete data structure, limit conditions, invariants and so on, the automatic refinement tools become possible. This paper presents an automatic operation refinement approach of formal methods, which bases on the theorem of automatic theorem proving (ATP). Plenty of rules and patterns have been already defined or can be defined by the users, which relate to the concrete data structure and context. Driven by these rules and patterns, and even the users´ manual direction, the refinement results can be finally obtained in the form of an operation sequence.