Name
Abstract | ||
|---|---|---|
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 behaviormodels. 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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1109/SNPD.2007.406 | SNPD (3) |
Keywords | DocType | ISBN |
formal method,operation sequence,architecture model,stepwise refinement,automatic theorem proving,refinement result,automatic refinement tool,operation refinement approach,critical domain,automatic operation refinement approach,concrete data structure,data structure,refinement calculus,formal specification,uml,formal methods,unified modeling language,data structures,behavior modeling,theorem proving | Conference | 0-7695-2909-7 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shuaiqiang Wang | 1 | 254 | 22.72 |
| Jiancheng Wan | 2 | 23 | 5.23 |
| Jinkui Hou | 3 | 7 | 4.94 |