电信服务系统特征交互的Z规格及验证  

Z Specification and Verification of Feature Interaction in Telecommunication Service System

作　　者：彭展[1] 梁根[2] 周炳[3] 

机构地区：[1]广东石油化工学院实验教学部,广东深圳518129 [2]广东石油化工学院理学院,广东茂名525000 [3]华为技术有限公司,广东深圳518129

出　　处：《计算机工程》2016年第8期19-23,共5页Computer Engineering

基　　金：广东石油化工学院青年自然科学基金资助项目(513023)

摘　　要：为对电信服务系统的特征交互问题进行精确、简洁的形式化描述,提出将Z语言应用于该问题的研究。对3种主要特征交互类型进行形式化描述,包括完整性破坏、相同触发条件和坏循环类型。针对特征交互的具体案例,通过Z语言得到精确、无歧义的形式化规格,分别描述各业务之间的交互过程,并在Z规格的基础上对其进行分析及形式化验证。研究人员可根据特征交互的形式化规格及验证结果掌握系统内部的冲突和缺陷,从而有效预防和解决电信系统特征交互问题,保障基础系统和新增功能模块的稳定性。For formally describing feature interaction problems in telecommunication system accurately and compactly, this paper applies Z language into the research on these feature interaction problems. It does the formal description for three main types of feature interaction, which contains integrality violation, same trigger condition and bad loop. It uses Z language to develop precise and unambiguous formal specification for the specific cases of the three types of feature interaction, describing the feature interaction between businesses. It analyzes and formally verifies the feature interactions based on Z specification. Researchers can grasp the collisions and faults in the system through formal specifications and verification results. The proposed method can prevent and solve the problems of feature interaction in telecommunication systems, and safeguard the stability of the base system and the new function module.

关 键 词：特征交互 Z规格 电信系统 形式化描述 形式化验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]