基于双格的软件产品线模型检测

doi:10.11896/j.issn.1002-137X.2015.02.036

计算机科学 ›› 2015, Vol. 42 ›› Issue (2): 167-172.doi: 10.11896/j.issn.1002-137X.2015.02.036

基于双格的软件产品线模型检测

石玉峰,魏欧,周宇

南京航空航天大学计算机科学与技术学院南京210016,南京航空航天大学计算机科学与技术学院南京210016,南京航空航天大学计算机科学与技术学院南京210016

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受国家自然科学基金项目(61170043,2),国家重点基础研究发展计划(973)项目(2014CB744904)资助

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

摘要： 软件产品线在保留每个产品的可变性前提下通过最大化产品间的共性实现资源的再利用,从而提高生产效率和节约生产成本。近年来,基于特征的状态迁移系统应用于软件产品线的建模和验证中。然而现有的方法不能很好地支持软件产品线中存在的信息不确定和不一致的情况。为此,首先提出一种基于双格的特征迁移系统,用于软件产品线的行为建模,采用投影的方法定义产品的行为模型；然后采用动作计算树逻辑描述系统的时序属性,并且给出它在新系统上的语义,用于支持基于双格的模型检测；最后,采用多值模型检测工具χchek对方法的有效性进行实验分析。

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

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

石玉峰,魏欧,周宇. 基于双格的软件产品线模型检测[J]. 计算机科学, 2015, 42(2): 167-172. https://doi.org/10.11896/j.issn.1002-137X.2015.02.036

SHI Yu-feng, WEI Ou and ZHOU Yu. Model Checking of Software Product Line Based on Bilattices[J]. Computer Science, 2015, 42(2): 167-172. https://doi.org/10.11896/j.issn.1002-137X.2015.02.036

参考文献

[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

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于双格的软件产品线模型检测

Model Checking of Software Product Line Based on Bilattices

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0