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

文档介绍：计 算 机 与 现 代 化
年第 期 总第 期
文章编 号 ：
基 于 的软件产 品线多值模 型检测方法
黄 鸣宇 ，石玉 峰
南京航 空航 天大学计算机科 学与技术 学院，江 苏 南京
摘要 ：软件 产品线保持产品个性化 的同时提 高 了公 共部分的复用。但软件产品线 中包含的不确 定信 息 ，给 产品带来 了潜
在风 险。形式化验证技 术逐 步应用于软件产品线验证 。但是传统 的布 尔逻辑模 型不能很好 地描 述软件 产品线的不 确定
性和 不一 致性 。本 文结合 多值模 型检测器 ，通过基 于动作 的模 型描 述 方法 ，对软件 产品 线进行描 述 ，然后 转换 成
为 规定的模型格 式 ，同时提供 多值逻辑描 述。最后 采用计算树逻辑描 述产品线属性 ，使 用 进行验证。
关键词 ：软件产品线 ；模 型检 测 ；；多值逻辑
中图分类 号 ： 文献标识码 ： ：．／．．．．．

，—
，，，
：
．．．
． ’
． 。．。
．
—．，
．
：；；；—
模 型检 测。是 一种 基 于状态搜 索 的形式 化验 证
引 言 方法 。该方法最早