Show simple item record

dc.contributor.authorBen-David, Shoham
dc.contributor.authorSterin, Baruch
dc.contributor.authorAtlee, Joanne M.
dc.contributor.authorBeidu, Sandy 17:15:53 (GMT) 17:15:53 (GMT)
dc.description.abstractProduct line (PL) engineering promotes the de- velopment of families of related products, where individual products are differentiated by which optional features they include. Modelling and analyzing requirements models of PLs allows for early detection and correction of requirements errors – including unintended feature interactions, which are a serious problem in feature-rich systems. A key challenge in analyzing PL requirements is the efficient verification of the product family, given that the number of products is too large to be verified one at a time. Recently, it has been shown how the high-level design of an entire PL, that includes all possible products, can be compactly represented as a single model in the SMV language, and model checked using the NuSMV tool. The implementation in NuSMV uses BDDs, a method that has been outperformed by SAT-based algorithms. In this paper we develop PL model checking using two leading SAT-based symbolic model checking algorithms: IMC and IC3. We describe the algorithms, prove their correctness, and report on our implementation. Evaluating our methods on three PL models from the literature, we demonstrate an improvement of up to 3 orders of magnitude over the existing BDD-based method.en
dc.description.sponsorshipNSERC Discovery Grant, 155243-12 || NSERC / Automotive Partnership Canada, APCPJ 386797 - 09 || Ontario Research Fund, RE05-044en
dc.titleSymbolic Model Checking of Product-Line Requirements Using SAT-Based Methodsen
dc.typeConference Paperen
dcterms.bibliographicCitationS. Ben-David, B. Sterin, J. M. Atlee and S. Beidu, "Symbolic Model Checking of Product-Line Requirements Using SAT-Based Methods," 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, Florence, 2015, pp. 189-199.en
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages