基于完备抽象解释的性质强保留抽象研究
在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全抽象.然后基于抽象解释框架及完备抽象解释和性质强保留之间的关系,构造使得Lμ性质强保留的最小抽象模型精化,并转换为抽象解释中抽象域的最小完备精化.依据此完备抽象域求得性质强保留的最优抽象状态划分,从而构造出性质强保留且最优的抽象状态转换系统.
抽象解释、模型检验、性质强保留、完备性、精化
37
TP311(计算技术、计算机技术)
国家自然科学基金61063002,61100186,61262008;中国博士后基金20090450211;广西自然科学基金2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220;武汉大学软件工程国家重点实验室开放基金SKLSE2010-08-06;广西壮族自治区教育厅重点项目基金资助.This work is supported by the National Natural Science Foundation of China under Grant Nos.61063002,61100186,61262008,China Postdoctoral Science Foundation No.20090450211,Guangxi Natural Science Foundation of China Nos.2011GXNSFA018164,2011GXNSFA018166,2012GXNSFA;Guangxi Key Laboratory of Trusted Software Focus Fund,and the Guangxi Department of Education Focus Fund
2014-09-15（万方平台首次上网日期，不代表论文的发表时间）
共14页
1754-1767
