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.
参考文献
相似文献
引证文献
引用本文
屈婉霞,庞征斌,郭阳,等.参数化系统二维抽象框架[J].国防科技大学学报,2010,32(1):95-100. QU Wanxia, PANG Zhengbin, GUO Yang, et al. A Generic Framework of Two-dimension Abstraction forParameterized Systems[J]. Journal of National University of Defense Technology,2010,32(1):95-100.