国防科技大学学报
國防科技大學學報
국방과기대학학보
JOURNAL OF NATIONAL UNIVERSITY OF DEFENSE TECHNOLOGY
2010年
1期
95-100
,共6页
屈婉霞%庞征斌%郭阳%李暾%杨晓东
屈婉霞%龐徵斌%郭暘%李暾%楊曉東
굴완하%방정빈%곽양%리돈%양효동
参数化系统%模型检验%抽象%多处理机系统%Cache一致性协议
參數化繫統%模型檢驗%抽象%多處理機繫統%Cache一緻性協議
삼수화계통%모형검험%추상%다처리궤계통%Cache일치성협의
parameterized system%model checking%abstraction%multiprocessor%Cache coherence protocol
针对参数化系统状态空间爆炸问题提出了一个通用的参数化系统二维抽象框架TDA.对所有进程单独进行抽象,利用参数化系统的设计思想,隐藏系统参数构建全系统的抽象模型,最大限度地剔除了原始系统中的冗余信息.建立的具有真并发语义的参数化系统的形式化模型,更适合描述一般意义上的并发系统,较好地解决了验证大规模同构和异构系统的空间激增问题.理论推导和实例均证实了TDA的正确性和合理性.
針對參數化繫統狀態空間爆炸問題提齣瞭一箇通用的參數化繫統二維抽象框架TDA.對所有進程單獨進行抽象,利用參數化繫統的設計思想,隱藏繫統參數構建全繫統的抽象模型,最大限度地剔除瞭原始繫統中的冗餘信息.建立的具有真併髮語義的參數化繫統的形式化模型,更適閤描述一般意義上的併髮繫統,較好地解決瞭驗證大規模同構和異構繫統的空間激增問題.理論推導和實例均證實瞭TDA的正確性和閤理性.
침대삼수화계통상태공간폭작문제제출료일개통용적삼수화계통이유추상광가TDA.대소유진정단독진행추상,이용삼수화계통적설계사상,은장계통삼수구건전계통적추상모형,최대한도지척제료원시계통중적용여신식.건립적구유진병발어의적삼수화계통적형식화모형,경괄합묘술일반의의상적병발계통,교호지해결료험증대규모동구화이구계통적공간격증문제.이론추도화실례균증실료TDA적정학성화합이성.
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 semantics for parameterized systems, more suitable for describing general concurrency systems, is introduced, which effectively solves the problem of verifying both homogeneous and heterogeneous systems. Results from the theoretical reasoning and the example given demonstrate that TDA is correct and feasible.