基于χChek的软件产品线多值模型检测方法-论文.pdf

《基于χChek的软件产品线多值模型检测方法-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、计算机与现代化2014年第8期JISUANJIYUXIANDAIHUA总第228期文章编号：1006-2475(2014)08-0087-04基于~Chek的软件产品线多值模型检测方法黄鸣宇，石玉峰(南京航空航天大学计算机科学与技术学院，江苏南京210016)摘要：软件产品线保持产品个性化的同时提高了公共部分的复用。但软件产品线中包含的不确定信息，给产品带来了潜在风险。形式化验证技术逐步应用于软件产品线验证。但是传统的布尔逻辑模型不能很好地描述软件产品线的不确定性和不一致性。本文结合多值模型检测器XChek，通过基于动作的模型描述方法，对软件产品线进行描述，然后转换成为XChek规

2、定的模型格式，同时提供多值逻辑描述。最后采用计算树逻辑描述产品线属性，使用~Chek进行验证。关键词：软件产品线；模型检测；XChek；多值逻辑中图分类号：TP31l文献标识码：Adoi：10．3969／j．issn．1006-2475．2014．08．019Multi-valuedModelCheckingofSoftwareProductLinewithXChekHUANGMing-yu，SHIYu—feng(CollegeofComputerScienceandTechnology，NanjingUniversityofAeronauticsandAstronautics，N

3、anjing210016，China)Abstract：SoftwareProductLine(SPL)keepstheflexibilityofproductsandimprovesthereuseofthecommonbaseatthesametime．ButSPLincludesmuchuncertainandinconsistentinformation．thustherewillbesomepotentialrisksforsoftwareproduct．FormalvalidationtechnologyhasbeenusedforvalidatingtheSPL．Bu

4、tthetraditionalmodelbasedonbooleanlogiccan’twelldescribethenondeterminacyandinconsistencyofSPL．Thereforecombinedwithamuti。valuedlogicmodelchecker．anaction。basedforspecifyingSPLwasproposed．Thenthenewmodelwasconvertedintothemodelwhichcanbecheckedby~Chekandalatticeofmulti—valuedlogicwasgenerated．

5、Atlast，ComputationTreeLogic(CTL)wasusedtodescribetemporalpropertiesoftheSPLandXChekcanvalidatethoseproperties．Keywords：SPL；modelchecking；XChek；multi—valuedlogic模型检测4。是一种基于状态搜索的形式化验证0引言方法。该方法最早由E．M．Clarke和E．A．Emerson人们对于个性化产品的需求越来越强烈。这一于1981年提出，在工业领域中早期被应用于电子电点不仅仅体现在传统的工业产品中，在软件领域中人路和通信协议的验证，随后

6、逐步应用到软件领域。模们对于个性化的需求也同样亟待解决。在实际的软型检测的基本思想是用状态迁移系统(S)表示系统件生产中往往会根据不同的用户需求设计和开发一的行为，用模态逻辑公式(F)描述系统的性质。这样系列的软件产品，这些软件产品具有一定的共性，同“系统是否具有所期望的性质”就转化为数学问题时又表现出不同的应用特征，从而构成软件产品线“状态迁移系统S是否是公式F的一个模型”，用公(SoftwareProductLine)。目前在软件领域中软件式表示为sF。对有限状态系统，这个问题是可判产品线还没有一个统一的定义。本文采用SEI对软定的，即可以用计算机程序在有限时间内自动确件产品线

7、的定义：“软件产品线是一组在公共核心资定j。模型检测拥有完全自动化的特性而且验证速源的基础上，按照规定的方式开发的软件密集系统的度较快，尤其是当系统没有满足某条性质时，模型检集合。这些系统共享一组公共的、可管理的、能够满测器可以给出相应的反例，这对于分析软件设计中的足特定的市场或者任务需求的特征的集合”J。错误，尽早在软件产品线早期解决潜在的问题有着重收稿日期：2014-04．28基金项目：国家自然科学基金资助项目(61170043)作者简介：黄鸣宇(1994一)，男