Computer Science ›› 2015, Vol. 42 ›› Issue (2): 167-172.doi: 10.11896/j.issn.1002-137X.2015.02.036

Previous Articles     Next Articles

Model Checking of Software Product Line Based on Bilattices

SHI Yu-feng, WEI Ou and ZHOU Yu   

  • Online:2018-11-14 Published:2018-11-14

Abstract: Software product line (SPL) maximizes the commonality between similar software products to reduce production costs and improve productivity.Recently,state transition systems based on features have been widely used in behavioral modeling and verification of SPLs.However,they can’t nicely support uncertain and inconsistent information.Therefore,firstly a formalism,bilattice-based featured transition systems (BFTS),was proposed for model chec-king of SPLs with uncertain and inconsistent information,where product was defined via projection.Furthermore,action computation tree logic (ACTL) was used to describe temporal properties;its semantics on BFTS was defined for model checking.Finally,based on multi-valued model checker χ chek,a case study was conducted to illustrate the effectiveness of our approach.

Key words: Model checking,Software product line,Multi-valued logic

[1] Clements P,Northrop L.Software Product Lines:Practices and Patterns [M].Addision-Wesley Professional,2001
[2] Baier C,Katoen J P.Principles of model checking[M].Cam-bridge:MIT press,2008
[3] Kang K C,Cohen S G,Hess J A,et al.Feature-oriented domain analysis (FODA) feasibility study[R].Carnegie-Mellon Univ Pittsburgh Pa Software Engineering Inst,1990
[4] Huth M,Jagadeesan R,Schmidt D.Modal transition systems:Afoundation for three-valued program analysis[M]∥Programming Languages and Systems.Springer Berlin Heidelberg,2001:155-169
[5] Classen A,Heymans P,Schobbens P Y,et al.Model checking lots of systems:efficient verification of temporal properties in software product lines[C]∥Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1.ACM,2010:335-344
[6] De Nicola R,Vaandrager F.Action versus state based logics for transition systems[M]∥Semantics of Systems of Concurrent Processes.Springer Berlin Heidelberg,1990:407-419
[7] 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.IEEE Computer Society,2003:804-805
[8] 聂坤明,张莉,樊志强.软件产品线可变性建模技术系统综述[J].软件学报,2013,24(9):2002-2018
[9] Apel S,Batory D,Kstner C,et al.Feature-Oriented Software Product Lines[M].Springer,2013
[10] Fantechi A,Gnesi S.Formal modeling for product families engineering[C]∥12th International Software Product Line Confe-rence,2008(SPLC’08).IEEE,2008:193-202
[11] Ginsberg M L.Multivalued logics:A uniform approach to reasoning in artificial intelligence[J].Computational intelligence,1988,4(3):265-316
[12] Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[M].Springer Berlin Heidelberg,1982
[13] Pnueli A.The temporal logic of programs[C]∥18th AnnualSymposium on Foundations of Computer Science,1977.IEEE,1977:46-57
[14] 魏欧,袁泳,蔡昕烨,等.循环对称化简及在三值模型上的扩展[J].软件学报,2011,22(6):1169-1184
[15] Shoham S,Grumberg O.Multi-valued model checking games[M]∥Automated Technology for Verification and Analysis.Springer Berlin Heidelberg,2005:354-369
[16] Chechik M,Devereux B,Easterbrook S,et al.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology (TOSEM),2003,12(4):371-408
[17] Leucker M,Thoma D.A formal approach to software productfamilies[M]∥Leveraging Applications of Formal Methods,Veri-fication and Validation.Technologies for Mastering Change.Springer Berlin Heidelberg,2012:131-145
[18] Schobbens P,Heymans P,Trigaux J C.Feature diagrams:A survey and a formal semantics[C]∥ 14th IEEE International Requirements Engineering Conference.IEEE,2006:139-148
[19] Niu N,Savolainen J,Yu Y.Variability modeling for product line viewpoints integration[C]∥2010 IEEE 34th Annual Computer Software and Applications Conference (COMPSAC).IEEE.2010:337-346
[20] 邹盛享,张伟,赵海燕,等.面向软件产品家族的变化性建模方法[J].软件学报,2005,16(1):37-49
[21] Ziadi T,Hélout L,Jézéquel J M.Towards a UML profile for software product lines[M]∥Software Product-Family Enginee-ring.Springer Berlin Heidelberg,2004:129-139
[22] Czarnecki K,Antkiewicz M.Mapping features to models:A template approach based on superimposed variants[C]∥Generative Programming and Component Engineering.Springer Berlin Heidelberg,2005:422-437
[23] 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,14(5):589-612
[24] Cordy M,Classen A,Heymans P,et al.ProVeLines:a product line of verifiers for software product lines[C]∥Proceedings of the 17th International Software Product Line Conference co-located workshops.ACM,2013:141-146
[25] 陈娟娟,魏欧,黄志球,等.基于双格的多值模型的精化关系与对称化简[J].计算机工程与应用,2013,49(22):40-45

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!