摘要
将描述端业务的LESS脚本转换为着色Petri网模型,可以为实现形式化方法检测端业务间的冲突提供基础。本文根据业务逻辑树节点的特性和LESS的定义,提出了通用的转化规则,实现了端业务的形式化建模,从而方便了业务的集成及业务间的离线检测。通过CPNTools对建立的业务模型进行仿真并分析模型状态空间,检测出端业务之间是否存在冲突。最后,用典型的业务实例验证了所提方法在Internet电话端系统环境中的可行性和有效性。
Using the transformation from the LESS scripts of end system services to the models of colored Petri nets, feature interaction in Internet telephony end systems is detected by formal methods. Based on the characters of decision-tree nodes and the definition of LESS, the universal rules of transformation are proposed. Then the formal models of end system services are obtained, and the feature integration and the off-line detection are realized easily. After simulating the models and analyzing the state space by CPN Tools, the feature interaction in Internet telephony end systems is detected. As a case study, some practical applications are introduced to show that the proposed approach works well in Internet telephony end systems.
出处
《计算机科学》
CSCD
北大核心
2007年第12期41-45,共5页
Computer Science
