使用实例驱动的软交换业务生成时序着色Petri网模型

软交换被认为是下一代网络（NGN）的核心技术之一。目前关于软交换的研究，大部分集中在体系结构和协议选取上，对业务生成和检测的建模研究滞后，而由于网络的变迁是个渐变的过程，当前软交换的生成环境和操作十分复杂，远远没有实现软交换体系业务开放的基本特征，因此对软交换业务生成的有效描述是十分必要的。本项目采用着色Petri网的分层结构，利用UML成熟的设计和分析方法，用变迁不变量表示使用实例，用不变量守恒变换实现软交换业务的增量式建模，并用时序逻辑公式表示业务的功能，从使用实例导出测试实例，通过检测时序逻辑公式进行校验。本项目研究系统的典型行为，避开复杂性，有效反映网络的全局特征，并体现网络分布式和并行运行的特点，可望建立软交换业务生成的统一的形式模型。本项目成果可融入电信厂商的解决方案中，具有学术和应用的双重意义。