摘要： 为对电信服务系统的特征交互问题进行精确、简洁的形式化描述,提出将Z语言应用于该问题的研究。对3种主要特征交互类型进行形式化描述,包括完整性破坏、相同触发条件和坏循环类型。针对特征交互的具体案例,通过Z语言得到精确、无歧义的形式化规格,分别描述各业务之间的交互过程,并在Z规格的基础上对其进行分析及形式化验证。研究人员可根据特征交互的形式化规格及验证结果掌握系统内部的冲突和缺陷,从而有效预防和解决电信系统特征交互问题,保障基础系统和新增功能模块的稳定性。

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

Abstract: 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.

Key words: feature interaction, Z specification, telecommunication system, formal description, formal verification

中图分类号: 

• TP311