Institutional Repository
| automatically generated formal specification based on the problem decomposition tree | |
| Wang Changjing | |
| 2012 | |
| Source | Qinghua Daxue Xuebao/Journal of Tsinghua University
 |
| ISSN | 1000-0054 |
| Volume | 52Issue:SUPPL.1Pages:88-92 |
| English Abstract | Difficulties in transforming informal requirements into formal specifications in requirement analyses greatly restrict the application scope of formal methods, with requirement validation that depends on informal requirement also not being reliable. A method was developed based on the problem decomposition tree (PDT) to automatically generate a formal specification, Radl. A user first needs to write the requirement using structure natural language (SNL), and chooses a suitable PDT and its corresponding abstract Radl specification from the knowledge base according to requirement characters, with the PDT then decomposed to a number of sub-problems until the base problem. The abstract Radl specification of every sub-problem is instantiated with combination and optimization being realized to obtain the final Radl specification. The method is able to generate Radl specifications of combinational optimization problems, as well as sort and search problems, which provides a new way to explore formal specifications in specific domains.; Difficulties in transforming informal requirements into formal specifications in requirement analyses greatly restrict the application scope of formal methods, with requirement validation that depends on informal requirement also not being reliable. A method was developed based on the problem decomposition tree (PDT) to automatically generate a formal specification, Radl. A user first needs to write the requirement using structure natural language (SNL), and chooses a suitable PDT and its corresponding abstract Radl specification from the knowledge base according to requirement characters, with the PDT then decomposed to a number of sub-problems until the base problem. The abstract Radl specification of every sub-problem is instantiated with combination and optimization being realized to obtain the final Radl specification. The method is able to generate Radl specifications of combinational optimization problems, as well as sort and search problems, which provides a new way to explore formal specifications in specific domains. |
| Indexed Type | EI |
| Keyword | Forestry Knowledge Based Systems |
| Department | (1) College of Computer and Information Engineering Jiangxi Normal University Nanchang 330022 China; (2) Institute of Software Chinese Academy of Sciences Beijing 100080 China; (3) Graduate University of Chinese Academy of Sciences Beijing 100049 China |
| Language | 中文 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15661 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Wang Changjing. automatically generated formal specification based on the problem decomposition tree[J]. Qinghua Daxue Xuebao/Journal of Tsinghua University,2012,52(SUPPL.1):88-92. |
| APA | Wang Changjing.(2012).automatically generated formal specification based on the problem decomposition tree.Qinghua Daxue Xuebao/Journal of Tsinghua University,52(SUPPL.1),88-92. |
| MLA | Wang Changjing."automatically generated formal specification based on the problem decomposition tree".Qinghua Daxue Xuebao/Journal of Tsinghua University 52.SUPPL.1(2012):88-92. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment