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

doi:10.3969/j.issn.1006-2475.2014.08.019

Abstract

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

CLC Number:

TP311

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.

References ［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]	GUAN Jin-ping, YANG Jin-ji, YANG Cheng-long. Formal Verification of Raft Protocol Based on Probabilistic Model [J]. Computer and Modernization, 2023, 0(09): 77-81.
[2]	WANG Yu-li, YANG Chang-song, QIU Jing, WEI Jun, WU Hong-jie, . Prediction Method of Foundation Pit Displacement Based on Spatiotemporal Attention Mechanism#br# [J]. Computer and Modernization, 2023, 0(05): 39-45.
[3]	ZHU Zhuo-yue, HUANG Huan, SONG Qing-ling, HOU Ju-pan. Atrioventricular Plane Displacement Detection and Reconstruction Based on CMR Images [J]. Computer and Modernization, 2023, 0(04): 78-82.
[4]	CUI Chen-lu, CUI Lin, . Lightweight Speech Emotion Recognition for Data Enhancement [J]. Computer and Modernization, 2023, 0(04): 83-89.
[5]	SHENG Jiang-an, CHEN Shu-rong. Mask-wearing Face Recognition Method Fused with Dual Attention Mechanism [J]. Computer and Modernization, 2023, 0(02): 72-77.
[6]	MENG Xiao-long, . DNeStCount: A Data-dependent Encoder-decoder Architecture with Split-attention for Crowd Counting#br# [J]. Computer and Modernization, 2022, 0(09): 68-77.
[7]	WANG Zhe, WANG Long-da, LIU GANG, WANG Xing-cheng, WANG Zhong-jun, BAO Lu-jie. Improved Immune Particle Swarm Optimization Algorithm for Automatic Parallel Parking Based on Cubic Spline Interpolation#br# [J]. Computer and Modernization, 2022, 0(02): 7-12.
[8]	ZHOU Kun-yang, ZHAO Meng-ting, ZHANG Hai-chao, SHAO Ye-qin. Human Pose Estimation Algorithm Based on Channel Splitting [J]. Computer and Modernization, 2021, 0(12): 27-36.
[9]	YANG Xin-yi, HOU Ling-yan, YANG Da-li, CUI Li-yan. Prediction of Renal Transplantation Rejection Based on SMOTE and RNN [J]. Computer and Modernization, 2021, 0(11): 7-11.
[10]	LIANG Chao, HUANG Hong-quan. Lightweight Image Super-Resolution Based on Convolutional Neural Network [J]. Computer and Modernization, 2020, 0(11): 23-27.
[11]	WEI Qing-zheng， YANG Yun， LI Ling-yan， WEI Hai-zhou. Predict Model for Foreign Exchange Based on Grey-Markov [J]. Computer and Modernization, 2020, 0(02): 12-.
[12]	WANG Zhi-le1, DONG Jun-yu2. GL Studio Chinese Technology Based on GB2312 Standard [J]. Computer and Modernization, 2020, 0(01): 85-.
[13]	SUN Yu-nan, NIE Ying, REN Fei. #br# 3D Symbol Generation for Communication Situation [J]. Computer and Modernization, 2019, 0(01): 120-.
[14]	GENG Juncheng1, ZHANG Xiaofei1, SUN Yubao2, WU Bo1, ZHOU Qiang2. Power Failure Sensitivity Prediction Algorithm Using Ksupport Sparse Logistic Regression [J]. Computer and Modernization, 2018, 0(04): 68-.
[15]	LIU Lin-wu， ZHANG Chi. ethod of False Counterexamples Detection in Model Checking [J]. Computer and Modernization, 2017, 0(9): 29-32,44.

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

Knowledge

Abstract

Cite this article

share this article

References ［17］

Related Articles 15

Recommended Articles

Metrics

Comments