automatically generated formal specification based on the problem decomposition tree
文献类型：期刊论文
| 作者 | Wang Changjing |
| 刊名 | Qinghua Daxue Xuebao/Journal of Tsinghua University
 |
| 出版日期 | 2012 |
| 卷号 | 52期号:SUPPL.1页码:88-92 |
| 关键词 | Forestry Knowledge based systems |
| ISSN号 | 1000-0054 |
| 中文摘要 | 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. |
| 收录类别 | EI |
| 语种 | 中文 |
| 公开日期 | 2013-09-17 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/15661]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 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. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。