Interfaces for Modular Feature Verification Export

@article{citeulike:4325511, abstract = {Feature-oriented programming organizes programs around features rather than objects, thus better supporting extensible, product-line architectures. Programming languages increasingly support this style of programming, but programmers get little support from verification tools. Ideally, programmers should be able to verify features independently of each other and use automated compositional reasoning techniques to infer properties of a system from properties of its features. Achieving this requires carefully designed interfaces: they must hold sufficient information to enable compositional verification, yet tools should be able to generate this information automatically because experience indicates programmers cannot or will not provide it manually. We present a model of interfaces that supports automated, compositional, feature-oriented model checking. To demonstrate their utility, we automatically detect the feature-interaction problems originally found manually by Robert Hall in an email suite case study.}, address = {Los Alamitos, CA, USA}, author = {Li, Harry C. and Krishnamurthi, Shriram and Fisler, Kathi}, booktitle = {Automated Software Engineering, 2002. Proceedings. ASE 2002. 17th IEEE International Conference on}, citeulike-article-id = {4325511}, citeulike-linkout-0 = {http://doi.ieeecomputersociety.org/10.1109/ASE.2002.1115013}, citeulike-linkout-1 = {http://dx.doi.org/10.1109/ASE.2002.1115013}, citeulike-linkout-2 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1115013}, doi = {10.1109/ASE.2002.1115013}, issn = {1527-1366}, journal = {Automated Software Engineering, International Conference on}, keywords = {formal-method, model-check, swd}, pages = {195--204}, posted-at = {2009-08-27 16:43:43}, priority = {2}, publisher = {IEEE Computer Society}, title = {Interfaces for Modular Feature Verification}, url = {http://dx.doi.org/10.1109/ASE.2002.1115013}, volume = {0}, year = {2002} }

TY - JOUR ID - citeulike:4325511 L3 - citeulike-article-id:4325511 N2 - Feature-oriented programming organizes programs around features rather than objects, thus better supporting extensible, product-line architectures. Programming languages increasingly support this style of programming, but programmers get little support from verification tools. Ideally, programmers should be able to verify features independently of each other and use automated compositional reasoning techniques to infer properties of a system from properties of its features. Achieving this requires carefully designed interfaces: they must hold sufficient information to enable compositional verification, yet tools should be able to generate this information automatically because experience indicates programmers cannot or will not provide it manually. We present a model of interfaces that supports automated, compositional, feature-oriented model checking. To demonstrate their utility, we automatically detect the feature-interaction problems originally found manually by Robert Hall in an email suite case study. JF - Automated Software Engineering, International Conference on SN - 1527-1366 AD - Los Alamitos, CA, USA EP - 204 TI - Interfaces for Modular Feature Verification PB - IEEE Computer Society VL - 0 T2 - Automated Software Engineering, 2002. Proceedings. ASE 2002. 17th IEEE International Conference on SP - 195 KW - formal-method KW - model-check KW - swd AU - Li, Harry AU - Krishnamurthi, Shriram AU - Fisler, Kathi PY - 2002/// UR - http://dx.doi.org/10.1109/ASE.2002.1115013 ER -