计算机工程

• 体系结构与软件技术 • 上一篇    下一篇

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

彭展1a,梁根1b,周炳2   

  1. (1.广东石油化工学院 a.实验教学部; b.理学院,广东 茂名 525000; 2.华为技术有限公司,广东 深圳 518129)
  • 收稿日期:2015-10-09 出版日期:2016-08-15 发布日期:2016-08-15
  • 作者简介:彭展(1985-),男,硕士,主研方向为软件开发形式化方法;梁根,副教授;周炳,博士。
  • 基金项目:
    广东石油化工学院青年自然科学基金资助项目(513023)。

Z Specification and Verification of Feature Interaction in Telecommunication Service System

PENG Zhan 1a,LIANG Gen 1b,ZHOU Bing 2   

  1. (1a.Department of Experimental Teaching; 1b.College of Science,Guangdong University of Petrochemical Technology,Maoming,Guangdong 525000,China; 2.Huawei Technologies Co.,Ltd.,Shenzhen,Guangdong 518129,China)
  • Received:2015-10-09 Online:2016-08-15 Published:2016-08-15

摘要: 为对电信服务系统的特征交互问题进行精确、简洁的形式化描述,提出将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

中图分类号: