caa a22 4500 445835389 CHVBK 20180317145329.0 cr unu---uuuuu 170323e20110301xx s 000 0 eng 10.1007/s10515-010-0075-7 doi (NATIONALLICENCE)springer-10.1007/s10515-010-0075-7 Compositional model checking of software product lines using variation point obligations [Elektronische Daten] [Jing Liu, Samik Basu, Robyn Lutz] This paper introduces a technique for incremental and compositional model checking that allows efficient reuse of model-checking results associated with the features in a product line. As the use of product lines has increased, so has the need to verify the models used to construct the products in the product line. However, this effort is currently hampered by the difficulty of composing model-checking results for the features in a way that allows reuse for subsequent products. The contributions of this paper are to remove restrictions on how the features can be sequentially composed, to describe how to generate obligations such that all sequentially composed systems can be verified, and to show how to compositionally model check the product in the product line by reusing the variation-point obligations. The paper develops the technique and its implementation in the context of a medical-device product line. Springer Science+Business Media, LLC, 2010 Software product lines nationallicence Compositional model checking nationallicence Variation point nationallicence Feature nationallicence Liu Jing Rockwell Collins, Inc., Cedar Rapids, IA, USA aut Basu Samik Department of Computer Science, Iowa State University, Ames, IA, USA aut Lutz Robyn Department of Computer Science, Iowa State University, Ames, IA, USA aut Automated Software Engineering Springer US; http://www.springer-ny.com 18/1(2011-03-01), 39-76 0928-8910 18:1<39 2011 18 10515 https://doi.org/10.1007/s10515-010-0075-7 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10515-010-0075-7 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Liu Jing Rockwell Collins, Inc., Cedar Rapids, IA, USA aut NATIONALLICENCE 700 1- Basu Samik Department of Computer Science, Iowa State University, Ames, IA, USA aut NATIONALLICENCE 700 1- Lutz Robyn Department of Computer Science, Iowa State University, Ames, IA, USA aut NATIONALLICENCE 773 0- Automated Software Engineering Springer US; http://www.springer-ny.com 18/1(2011-03-01), 39-76 0928-8910 18:1<39 2011 18 10515 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer