基于χChek的软件产品线多值模型检测方法

doi:10.3969/j.issn.1006-2475.2014.08.019

计算机与现代化

基于χChek的软件产品线多值模型检测方法

(南京航空航天大学计算机科学与技术学院，江苏南京210016)

收稿日期:2014-04-28 出版日期:2014-08-15 发布日期:2014-08-19
作者简介:黄鸣宇(1994-),男，河南息县人，南京航空航天大学计算机科学与技术学院本科生，研究方向：形式化方法，模型检测；石玉峰(1990-),女，研究生，研究方向：模型检测器，软件产品线。
基金资助:
国家自然科学基金资助项目(61170043)

#br# Multi-valued Model Checking of Software Product Line with χChek

（College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016,

China）

Received:2014-04-28 Online:2014-08-15 Published:2014-08-19

摘要/Abstract

摘要：

软件产品线保持产品个性化的同时提高了公共部分的复用。但软件产品线中包含的不确定信息，给产品带来了潜在风险。形式化

验证技术逐步应用于软件产品线验证。但是传统的布尔逻辑模型不能很好地描述软件产品线的不确定性和不一致性。本文结合多值模型

检测器χChek，通过基于动作的模型描述方法，对软件产品线进行描述，然后转换成为χChek规定的模型格式，同时提供多值逻辑描述

。最后采用计算树逻辑描述产品线属性，使用χChek进行验证。

关键词: 软件产品线, 模型检测, &chi, Chek, 多值逻辑

Abstract:

Software Product Line (SPL) keeps the flexibility of products and improves the reuse of the common base

at the same time. But SPL includes much uncertain and inconsistent information, thus there will be some potential

risks for software product. Formal validation technology has been used for validating the SPL. But the traditional

model based on boolean logic can’t well describe the nondeterminacy and inconsistency of SPL. Therefore combined

with a muti-valued logic model checker, an action-based for specifying SPL was proposed. Then the new model was

converted into the model which can be checked by χChek and a lattice of multi-valued logic was

generated. At last, Computation Tree Logic (CTL) was used to describe temporal properties of the SPL and

χChek can validate those properties.

Key words: SPL, model checking, χChek, multi-valued logic

中图分类号:

TP311

黄鸣宇,石玉峰. 基于χChek的软件产品线多值模型检测方法[J]. 计算机与现代化, doi: 10.3969/j.issn.1006-2475.2014.08.019.

HUANG Ming-yu, SHI Yu-feng. #br# Multi-valued Model Checking of Software Product Line with χChek[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2014.08.019.

参考文献［17］

［1］	Klaus Pohl，Günter Bckle, Frank Van Der Linden. Software Product Line Engineering［M］. Berlin: Springer, 2005.
	
［2］	Clements P, Northrop L. Software Product Lines: Practices and Patterns［M］. Boston: Addison Wesley, 2002.
	
［3］	Baier C, Katoen J P. Principles of Model Checking［M］. Cambridge：MIT Press, 2008.
［4］	Clarke E M, Grumberg O, Peled D. Model Checking［M］. 4th ed. Cambridge: MIT Press, 1999.
［5］	王敏飞. 模型检测在安全协议验证中的研究与应用［D］. 南京:南京航空航天大学, 2009.
［6］	聂坤明,张莉,樊志强. 软件产品线可变性建模技术系统综述［J］. 软件学报, 2013,24(9):2001-2019.
［7］	赵鄂，杨博文，杨贯中. 一种适用于软件产品线的特征模型［J］. 计算机系统应用, 2013,22(10):114-118.
［8］	Shoham S, Grumberg O. Multi-valued Model Checking Games［M］. Berlin:Springer, 2005:354-369.
［9］	Gruler A, Leucker M, Scheidemann K D. Modeling and model checking software product lines: Formal methods
	for open object-based distributed systems［C］// Proceedings of the 10th IFIP WG 6.1 International Conference.
	Oslo:Springer-Verlag, 2008:113-131.
［10］	Ginsberg M L． Multi-valued logics［C］// Proceedings of the 5th National Conference on Artificial
	Intelligence. 1986,1.
［11］	陈娟娟，魏欧，黄志球，等. 基于双格的多值模型的精化关系与对称化简［J］. 计算机工程与应用, 2013,49(22),40-44.
［12］	Steve Easterbrook, Marsha Chechik, et a1. 〖JX-5〗χ〖JX5〗Chek: A model checker for multi-valued
	reasoning［C］// Proceedings of the 25th International Conference on Software Engineering. 2003:804-805.
［13］	Chechik M, Devereux B,Easterbrook S, et a1． Multi-valued symbolic model-checking［J］． ACM Transactions
	on Software Engineering and Methodology， 2003,12(4)：371-408．
［14］	Jocelyn Simmonds, Arie Gurfinkel. 〖JX-5〗χ〖JX5〗Chek RC2 User Manual［R］. University of Toronto,
20	07.
［15］	Steve Easterbrook, Marsha Chechik. A framework for multi-valued reasoning over inconsistent viewpoints ［C
］	// Proceedings of the 23rd ICSE. 2001:411-420.
［16］	Clarke E M, Emerson E A. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal
	Logic［M］. Berlin:Springer, 1982:52-71.
［17］	Michael Huth, Mark Ryan. Logic in Computer Science Modelling and Reasoning about Systems［M］. New York:
	Cambridge University Press, 2004:217-221.

[1]	管金平, 杨晋吉, 杨成龙. 基于概率模型的Raft协议形式化验证[J]. 计算机与现代化, 2023, 0(09): 77-81.
[2]	郑晓娟,刘洋,陈祥科. 基于特征可变性建模教学服务管理系统的研究与实现[J]. 计算机与现代化, 2018, 0(08): 120-.
[3]	刘林武，张弛. 模型检测中虚假反例检测方法[J]. 计算机与现代化, 2017, 0(9): 29-32,44.
[4]	刘维维，庄毅，李蜜. 一种嵌入式软件可靠性建模与评估方法[J]. 计算机与现代化, 2017, 0(8): 78-.
[5]	毛良文1，徐亮2,3. 基于SMT的PTACTL限界模型检测方法[J]. 计算机与现代化, 2016, 0(3): 41-45.
[6]	罗敏1,2，方琳3，施炜利1,2. 基于小系统理论的简化SET协议[J]. 计算机与现代化, 2014, 0(12): 97-102.
[7]	徐小丽. 基于SPIN的系统建模研究[J]. 计算机与现代化, 2012, 1(9): 209-214.
[8]	陈志辉. 基于时间自动机的信息物理融合系统建模与验证[J]. 计算机与现代化, 2012, 1(10): 125-130,.
[9]	温炽亮. 小额交易中SET协议的优化及SPIN验证的研究[J]. 计算机与现代化, 2011, 7(7): 201-206.
[10]	罗清胜. 一种基于Büchi自动机的LTL程序模型检测方法[J]. 计算机与现代化, 2010, 1(8): 58-61.

基于χChek的软件产品线多值模型检测方法

#br# Multi-valued Model Checking of Software Product Line with χChek

可视化

摘要/Abstract

引用本文

使用本文

参考文献［17］

相关文章 10

编辑推荐

Metrics

本文评价

基于χChek的软件产品线多值模型检测方法

#br# Multi-valued Model Checking of Software Product Line with χChek

可视化

摘要/Abstract

引用本文

使用本文

参考文献 ［17］

相关文章 10

编辑推荐

Metrics

本文评价

参考文献［17］