论文部分内容阅读
针对参数化系统状态空间爆炸问题提出了一个通用的参数化系统二维抽象框架TDA。对所有进程单独进行抽象，利用参数化系统的设计思想，隐藏系统参数构建全系统的抽象模型，最大限度地剔除了原始系统中的冗余信息。建立的具有真并发语义的参数化系统的形式化模型，更适合描述一般意义上的并发系统，较好地解决了验证大规模同构和异构系统的空间激增问题。理论推导和实例均证实了TDA的正确性和合理性。