automatically generated formal specification based on the problem decomposition tree

ISCAS OpenIR

	automatically generated formal specification based on the problem decomposition tree
	Wang Changjing
	2012
发表期刊	Qinghua Daxue Xuebao/Journal of Tsinghua University
ISSN	1000-0054
卷号	52 期号:SUPPL.1 页码:88-92
摘要	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
关键词	Forestry Knowledge Based Systems
部门归属	(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
语种	中文
内容类型	期刊论文
URI标识	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.