基于完备抽象解释的性质强保留抽象研究
发布时间：2019-05-16 13:29
【摘要】：在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ-演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全抽象.然后基于抽象解释框架及完备抽象解释和性质强保留之间的关系,构造使得Lμ性质强保留的最小抽象模型精化,并转换为抽象解释中抽象域的最小完备精化.依据此完备抽象域求得性质强保留的最优抽象状态划分,从而构造出性质强保留且最优的抽象状态转换系统.
[Abstract]:Abstraction is an important method to solve the state space explosion problem in model checking. The usual abstraction is not strongly reserved, that is, there may be temporal properties that are not satisfied in the abstract model but satisfied in the concrete model. In this paper, the security abstraction of 渭-calculus L 渭 semantic model is constructed systematically, and on this basis, it is transformed into security abstraction under general Kripke structure. Then, based on the abstract interpretation framework and the relationship between complete abstract interpretation and strong retention of properties, the minimum abstract model with strong retention of L 渭 property is constructed and transformed into the minimum complete refinement of extraction domain in abstract interpretation. According to this complete abstract domain, the optimal abstract state partition with strong property retention is obtained, and the abstract state transition system with strong property retention and optimal property is constructed.
【作者单位】： 武汉大学软件工程国家重点实验室;桂林电子科技大学广西可信软件重点实验室;
【基金】：国家自然科学基金(61063002,61100186,61262008) 中国博士后基金(20090450211) 广西自然科学基金(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220) 武汉大学软件工程国家重点实验室开放基金(SKLSE2010-08-06) 广西壮族自治区教育厅重点项目基金资助~~
【分类号】：TP306
本文编号：2478312
[Abstract]:Abstraction is an important method to solve the state space explosion problem in model checking. The usual abstraction is not strongly reserved, that is, there may be temporal properties that are not satisfied in the abstract model but satisfied in the concrete model. In this paper, the security abstraction of 渭-calculus L 渭 semantic model is constructed systematically, and on this basis, it is transformed into security abstraction under general Kripke structure. Then, based on the abstract interpretation framework and the relationship between complete abstract interpretation and strong retention of properties, the minimum abstract model with strong retention of L 渭 property is constructed and transformed into the minimum complete refinement of extraction domain in abstract interpretation. According to this complete abstract domain, the optimal abstract state partition with strong property retention is obtained, and the abstract state transition system with strong property retention and optimal property is constructed.
【作者单位】： 武汉大学软件工程国家重点实验室;桂林电子科技大学广西可信软件重点实验室;
【基金】：国家自然科学基金(61063002,61100186,61262008) 中国博士后基金(20090450211) 广西自然科学基金(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220) 武汉大学软件工程国家重点实验室开放基金(SKLSE2010-08-06) 广西壮族自治区教育厅重点项目基金资助~~
【分类号】：TP306
【相似文献】
相关硕士学位论文 前1条
1 国莹;基于共享总线的多核实时系统WCET分析[D];东北大学;2010年
，本文编号：2478312
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/2478312.html
