| 参数化系统二维抽象框架 |
| |
| 引用本文： | 屈婉霞,庞征斌,郭阳,李暾,杨晓东.参数化系统二维抽象框架[J].国防科技大学学报,2010,32(1):95-100. |
| |
| 作者姓名： | 屈婉霞 庞征斌 郭阳 李暾 杨晓东 |
| |
| 作者单位： | 国防科技大学,计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金资助项目(60573173,60773025);;新世纪优秀人才支持计划资助项目 |
| |
| 摘 要： | 针对参数化系统状态空间爆炸问题提出了一个通用的参数化系统二维抽象框架TDA。对所有进程单独进行抽象,利用参数化系统的设计思想,隐藏系统参数构建全系统的抽象模型,最大限度地剔除了原始系统中的冗余信息。建立的具有真并发语义的参数化系统的形式化模型,更适合描述一般意义上的并发系统,较好地解决了验证大规模同构和异构系统的空间激增问题。理论推导和实例均证实了TDA的正确性和合理性。
|
| 关 键 词： | 参数化系统 模型检验 抽象 多处理机系统 Cache一致性协议 |
| 收稿时间： | 2009/5/18 0:00:00 |
A Generic Framework of Two-dimension Abstraction for Parameterized Systems |
| |
| QU Wanxi,PANG Zhengbin,GUO Yang,LI Tun and YANG Xiaodong.A Generic Framework of Two-dimension Abstraction for Parameterized Systems[J].Journal of National University of Defense Technology,2010,32(1):95-100. |
| |
| Authors: | QU Wanxi PANG Zhengbin GUO Yang LI Tun and YANG Xiaodong |
| |
| Affiliation: | College of Computer;National Univ.of Defense Technology;Changsha 410073;China |
| |
| Abstract: | To address the state explosion problem in model checking parameterized systems,this paper proposes a generic framework of two-dimension abstraction(TDA),in which the size of the state transition graph for individual process is reduced independently at first,and the whole system composed of reduced processes is then abstracted based on the design method of parameterized systems,thus avoiding the construction of the unreduced model that might be too big to fit into memory.Formal model with true concurrency se... |
| |
| Keywords: | parameterized system model checking abstraction multiprocessor Cache coherence protocol |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载全文 |
|
