【摘要】 介绍了Hierarchy CPN的相关定义,然后对OpenFlow协议进行了基于时间着色CPN建模.在建模过程中,详细考虑了Token Colour的选取与相关变量的定义,并考虑了时间属性,针对建模的性能进行了分析.执行上述模型并进行验证分析,得出变迁发生次数与所需时间基本符合稳态分布这一事实,满足预期的要求.对所构建模型进行自定义查询分析,依据模型活性、死锁、可达性等特性构建相应的抽象路径,用于指导抽象测试例的生成.更多还原

【Abstract】 The definition of Hierarchy CPN(coloured Petri net)was introduced firstly,and then a formal model about OpenFlow protocol was made.In the modelling process,the choice of token color and the definition of relevant variables detailed was considered.The time factor was also considered,and made analysis about performance.By executing these model,making verification and analysis,the fact that the frequency of the transition and the time match normal distribution had got.This met the expected requirements.The user defined query analyse on this model was made,such as live lock,dead lock and reachabilities.The abstract paths was also constructed which can be used to generate abstract testcases.更多还原