Computer Science ›› 2016, Vol. 43 ›› Issue (4): 167-172.doi: 10.11896/j.issn.1002-137X.2016.04.034

Previous Articles     Next Articles

Model Checking Software Product Line Based on Feature Slicing

LIU Yu-mei, WEI Ou and HUANG Ming-yu   

  • Online:2018-12-01 Published:2018-12-01

Abstract: Feature models are a popular formalism for describing the commonality and variability of software product line in terms of features.Feature models symbolize a representation of the possible application configuration space,and can be customized based on specific domain requirements and stakeholder goals.As feature models are becoming increa-singly complex,it is desired to provide automatic support for customized analysis and verification based on the strategic goals and requirements of stakeholders.This paper firstly presented feature model slicing based on the requirements of the users.It then introduced three-valued abstraction of behavior models based on the slicing unit.Finally,based on multi-valued model checker,a case study was conducted to illustrate the effectiveness of our approach.

Key words: Software product line,Feature slicing,Three-valued model,Model checking

[1] Pohl K,Bockle G,Linden V D.Software Product Line Engineering:Foundations,Principles and Techniques[M].Berlin Heidelberg:Springer-Verlag,2005
[2] Classen A,Heymans P,Schobbens P Y.What’s in a feature:A requirements engineering perspective[C]∥ Proceedings of the 11th International Conference on Fundamental Approaches to Software Engineering (FASE 08) in Conjuncation with ETAPS’08.2008:16-30
[3] Nie K M,Zhang L,Fan Z Q.Systematic literarture review ofsoftware product line variability modeling techniques[J].Journal of Software,2013,24(9):2001-2019(in Chinese) 聂坤明,张莉,樊志强.软件产品线可变性建模技术系统综述[J].软件学报,2013,24(9):2001-2019
[4] Schobbens P Y,Heymans P,Trigaux J C,et al.Generic semantics of feature diagrams[J].Computer Networks,2007,51(2):456-479
[5] Classen A,Heymans P,Schobbens P Y,et al.Symbolic model checking of software product lines[C]∥Proceeding of the 33rd International Conference on Software Engineering.New York:ACM,2011:321-330
[6] Baier C,Katoen J P.Principles of model checking[M].Cam-bridge:MIT press,2008
[7] Acher M,Collet P,Lahire P,et al.Slicing feature models[C]∥Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering.Washington:IEEE,2011:424-427
[8] Hartmann H,Trew T.Using feature diagrams with context vari-ability to model multiple product lines for software supply chains[C]∥Proceedings of the 12th International Software Product Line Conference.Washington:IEEE,2008:12-21
[9] Hartmann H,Trew T,Matsinger A.Supplier independent fea-ture modeling[C]∥Proceedings of the 13th International Software Product Line Conference.Pittsburgh:Carnegie Mellon University,2009:191-200
[10] Easterbrook S,Chechik M,Devereux B,et al.χChek:A model checker for multi-valued reasoning[C]∥Proceedings of the 25th International Conference on Software Engineering.Washington:IEEE Computer Society,2003:804-805
[11] Benavides D,Segura S,Ruiz-Cortés A.Automated analysis offeature models 20 years later:A literature review[J].Information Systems,2010,35(6):615-636
[12] Schobbens P,Heymans P,Trigaux J.Feature Diagrams:A Survey and A Formal Semantics[M]∥Proceedings of 14th IEEE International Conference on Requirements Engineering.Washington:IEEE Computer Society,2006:139-148
[13] Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[M]∥Logic of Programs:Workshop,Yorktown Heights,New York,May 1981.London:Springer-Verlag,1981:52-71
[14] Pnueli A.The temporal logic of programs[C]∥Proceedings of the 18th Annual Symposium on Foundations of Computer Scien-ce.Washington:IEEE,1977:46-57
[15] Nicola R D,Vaandrager F.Action versus state based logics for transition systems[J]∥Lecture Notes in Computer Science,1990,9:407-419
[16] Glenn B,Patrice G.Model Checking Partial State Spaces with 3-Valued Temporal Logics[J].11th International Conference on Computer Aided Verification(CAV’99).1999:274-287
[17] Classen A,Cordy M,Heymans P,et al.Model checking software product lines with SNIP[J].International Journal on Software Tools for Technology Transfer,2012,4(5):589-612
[18] Chen J J,Wei O.Approximation of multi-valued models via reduction[J].Computer Science,2014,1(6):125-130(in Chinese) 陈娟娟,魏欧.基于分解的多值模型的逼近关系[J].计算机科学,2014,41(6):125-130
[19] Shi Y F,Wei O,Zhou Y.Model checking of software product line based on bilattices[J].Computer Science,2015,2(2):167-172(in Chinese) 石玉峰,魏欧,周宇.基于双格的软件产品线模型检测[J].计算机科学,2015,2(2):167-172
[20] Classen A,Boucher Q,Heymans P.A text-based approach to feature modelling:Syntax and semantics of TVL[J].Science of Computer Programming,2011,76(12):1130-1143

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!