{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T05:43:10Z","timestamp":1770010990710,"version":"3.49.0"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,5,1]],"date-time":"2006-05-01T00:00:00Z","timestamp":1146441600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,5]]},"DOI":"10.1007\/s10703-006-0002-5","type":"journal-article","created":{"date-parts":[[2006,6,8]],"date-time":"2006-06-08T15:48:21Z","timestamp":1149781701000},"page":"213-261","source":"Crossref","is-referenced-by-count":30,"title":["Feature interaction detection by pairwise analysis of LTL properties\u2014A case study"],"prefix":"10.1007","volume":"28","author":[{"given":"Muffy","family":"Calder","sequence":"first","affiliation":[]},{"given":"Alice","family":"Miller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,9]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D.C. Kozen, \u201cLimits for automatic verification of finite-state concurrent systems,\u201d Inform. Proc. Lett., Vol. 22, pp. 307\u2013309, 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"M. Browne, E. Clarke, and O. Grumberg, \u201cCharacterizing finite Kripke structures in propositional temporal logic,\u201d Theor Comp Sci, Vol. 59, pp. 115\u2013131, 1988.","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"2_CR3","unstructured":"M. Calder and E. Magill (Eds.), Feature Interactions in Telecommunications and Software Systems VI. Amsterdam, IOS Press, 2000."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"M. Calder and A. Miller, \u201cUsing SPIN for feature interaction analysis\u2014A case study,\u201d in M.B. Dwyer (Ed.), Proceedings of the 8th International SPIN Workshop (SPIN 2001), volume 2057 of Lecture Notes in Computer Science, Springer-Verlag, Toronto, Canada, May 2001, pp. 143\u2013162.","DOI":"10.1007\/3-540-45139-0_9"},{"key":"2_CR5","unstructured":"M. Calder and A. Miller, \u201cAnalysing a basic call protocol using Promela\/XSPIN,\u201d in G. Holzmann, E. Najm, and A. Serhrouchni (Eds.), Proceedings of the 4th Workshop on Automata Theoretic Verification with the SPIN Model Checker (SPIN '98), Paris, France, November 1998, pp. 169\u2013181."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"M. Calder and A. Miller, \u201cAutomatic verification of any number of concurrent, communicating processes,\u201d in Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE 2002) IEEE Computer Society Press, Edinburgh, UK: September 2002, pp. 227\u2013230.","DOI":"10.1109\/ASE.2002.1115017"},{"key":"2_CR7","unstructured":"E.J. Cameron, N. Griffeth, Y.-J. Lin, M.E. Nilson, and W.K. Schnure,\u201c A feature interaction benchmark for IN and beyond,\u201d in L.G. Bouma and H. Velthuijsen (Eds.), Feature Interactions in Telecommunications Systems, Amsterdam IOS Press, May 1994, pp. 1\u201323."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"A. Cimatti, F. Giunchiglia, G. Mingardi, D. Romano, F. Torielli, and P. Traverso. \u201cModel checking safety critical software with SPIN: an application to a railway interlocking system,\u201d in Proceedings of the Third SPIN Workshop, Twente University, Enschede, The Netherlands, April 1997, pp. 5\u201317.","DOI":"10.1007\/3-540-49646-7_22"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and S. Jha, \u201cVerifying parameterized networks using abstraction and regular languages,\u201d in I. Lee and S.A. Smolka (Eds.), Proceedings of the 6th International Conference on Concurrency Theory (CONCUR '95), volume 962 of Lecture Notes in Computer Science, Philadelphia, PA., Springer-Verlag, August 1995, pp. 395\u2013407.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"2_CR10","unstructured":"E. Clarke, O. Grumberg, and D. Long, \u201cModel checking and abstraction,\u201d ACM Transactions on Programming Languages and Systems, Vol. 16, No. 5, pp. 1512\u20131542, 1994."},{"key":"2_CR11","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. Cambridge, Masachusetts, The MIT Press, 1999."},{"key":"2_CR12","unstructured":"S.J. Creese and A.W. Roscoe, \u201cData independent induction over structured networks,\u201d in Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'00), volume II, Las Vegas, Nevada, USA, CSREA Press, June 2000."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"D. Dill, A. Drexler, A. Hu, and C.H. Yang,\u201cProtocol verification as a hardware design aid,\u201d in Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer Processors (ICCD'92), IEEE Computer Society, Cambridge, Massachusetts, USA, October 1992, pp. 522\u2013525.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, \u201cProperty specification patterns for finite-state verification,\u201d in Proceedings of the Second International Workshop on Formal Methods in Software Practice (FMSP '98), ACM Press, March 1998, pp. 7\u201315.","DOI":"10.1145\/298595.298598"},{"key":"2_CR15","unstructured":"M.B. Dwyer and J. Hatcliff, \u201cSlicing software for model construction\u201d, in O. Danvy (Ed.), Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'99), San Antonio, Texas, January 1999, pp. 105\u2013118, University of Aarhus. Technical report BRICS-NS-99-1."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"E. Emerson, \u201cTemporal and modal logic,\u201d in J.V. Leeuwen (Ed.), Handbook of Theoretical Computer Science, MIT Press, Cambridge, MA, USA, 1990, pp. 995\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"E. Emerson and J. Halpern, \u201csometimes\u201d and \u201cnot never\u201d revisited: On branching time versus linear time. J. ACM, Vol. 33, pp. 151\u2013178, 1986.","DOI":"10.1145\/4904.4999"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"E. Emerson and V. Kahlon, \u201cReducing model checking of the many to the few,\u201d in D. A. McAllester (Ed.), Automated Deduction\u2014Proceedings of the 17th International Conference on Automated Deduction (CADE 2000), volume 1831 of Lecture Notes in Computer Science, Springer-Verlag, Pittsburgh, PA, USA, June 2000, pp. 236\u2013254.","DOI":"10.1007\/10721959_19"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"E. Emerson and K. Namjoshi, \u201cReasoning about rings,\u201d in Conference Record of the 22nd Annual ACM Symposium on Principles of Programming Languages (POPL '95), ACM Press, San Francisco, California, January 1995, pp. 85\u201394.","DOI":"10.1145\/199448.199468"},{"key":"2_CR20","unstructured":"A. Felty and K. Namjoshi, \u201cFeature specification and automatic conflict detection,\u201d in Calder and Magill [3], pp. 179\u2013192."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"S.M. German and A.P. Sistla, \u201cReasoning about systems with many processes,\u201d J. ACM, Vol. 39, No. 3, pp. 675\u2013735, 1992.","DOI":"10.1145\/146637.146681"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Vardi, and P. Wolper, \u201cSimple on-the-fly automatic verification of linear temporal logic,\u201d in Proceedings of the 15th international Conference on Protocol Specification Testing and Verification (PSTV '95), Chapman & Hall, Warsaw, Poland, 1995, pp. 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long, \u201cModel checking and modular verification,\u201d in J. C.M. Baeten and J. F. Groote (Eds.), Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR '91), volume 527 of Lecture Notes in Computer Science, Springer-Verlag, Amsterdam, The Netherlands, August 1991, pp. 250\u2013265.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"2_CR24","unstructured":"R.J. Hall, \u201cFeature combination and interaction detection via foreground\/background models,\u201d in Kimbler and Bouma [37], pp. 232\u2013246."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"C.L. Heitmeyer, J. Jr. Kirby, B. Labaw, M. Archer, and R. Bharadwaj, \u201cUsing abstraction and model checking to detect safety violations in requirements specifications,\u201d IEEE Transactions on Software Engineering, Vol. 24, No. 11, pp. 927\u2013948, Nov. 1998.","DOI":"10.1109\/32.730543"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"G. Holzmann, \u201cDesign and validation of protocols: A tutorial,\u201d Computer Networks and ISDN Systems, Vol. 25, pp. 981\u20131017, 1993.","DOI":"10.1016\/0169-7552(93)90095-L"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"G. Holzmann, \u201cThe model checker SPIN,\u201d IEEE Trans. Soft. Engin., Vol. 23, No. 5, pp. 279\u2013295, 1997.","DOI":"10.1109\/32.588521"},{"key":"2_CR28","unstructured":"G. Holzmann, \u201cState compression in spin: Recursive indexing and compression training runs,\u201d in Langerak [42]."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"G. Holzmann, \u201cThe engineering of a model checker: The Gnu i-protocol case study revisited,\u201d in D. Dams, R. Gerth, S. Leue, and M. Massink (Eds.), Proceedings of the 5th and 6th International Spin Workshops, volume 1680 of Lecture Notes in Computer Science, Springer-Verlag, Trento, Italy and Toulouse, France, 1999, pp. 232\u2013244.","DOI":"10.1007\/3-540-48234-2_18"},{"key":"2_CR30","unstructured":"G. Holzmann The SPIN Model Checker: Primer and Reference Manual, Addison Wesley, Boston, 2003."},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"G. Holzmann and D. Peled, \u201cAn improvement in formal verification,\u201d in D. Hogrefe and S. Leue (Eds.), Proceedings of the 7th WG6.1 International Conference on Formal Description Techniqus (FORTE '94), Volume 6 of Internationl Federation For Information Processing, Berne, Switzerland, Chapman and Hall, October 1994, pp. 197\u2013211.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"G. Holzmann and M. Smith, \u201cA practical method for the verification of event-driven software,\u201d in Proceedings of the 21st international conference on on Software engineering (ICSE'99), Los Angeles, California, USA, ACM Press, May 1999, pp. 597\u2013607.","DOI":"10.1145\/302405.302710"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"G. Holzmann and M. Smith, \u201cSoftware model checking\u2014extracting verification models from source code,\u201d in J. Wu, S. Chanson, and Q. Gao (Eds.), Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communiction Protocols and Protocol Specification, Testing and Verification (FORTE\/PSTV '99), volume 156 of International Federtion. For Information Processing, Beijing, China, Kluwer, October 1999, pp. 481\u2013497.","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"2_CR34","unstructured":"IN Distributed Functional Plane Architecture, recommmendation q. 1204, ITU-T edition, March 1992."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"C. Norris Ip and D.L. Dill, \u201cVerifying systems with replicated components in Mur\u03c6,\u201d Formal Methods in System Design Vol. 14, pp. 273\u2013310, 1999.","DOI":"10.1023\/A:1008723125149"},{"key":"2_CR36","unstructured":"B. Jonsson, T. Margaria, G. Naeser, J. Nystroem, and B. Steffen, \u201cIncremental requirement specification for evoling systems,\u201d in Calder and Magill [3], pp. 145\u2013162."},{"key":"2_CR37","unstructured":"K. Kimbler and L.G. Bouma (Eds.), Feature Interactions in Telecommunications and Software Systems V. IOS Press, Amsterdam, September 1998."},{"key":"2_CR38","unstructured":"M. Kolberg, E.H. Magill, D. Marples, and S. Reiff, \u201cResults of the second feature interaction contest,\u201d in Calder and Magill [3], pp. 311\u2013325."},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K.L. McMillan, \u201cA structural induction theorem for processes,\u201d in Proceedings of the eighth Annual ACM Symposium on Principles of Distrubuted Computing, ACM Press, 1989, pp. 239\u2013247.","DOI":"10.1145\/72981.72998"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, M. Merritt, A. Orda, and S.R. Sachs, \u201cA structural linearization principle for processes,\u201d Formal Methods in System Design, Vol. 5, No. 3, pp. 227\u2013244, December 1994.","DOI":"10.1007\/BF01383832"},{"key":"2_CR41","unstructured":"L. Lamport, \u201cWhat good is temporal logic?\u201d Information Processing, Vol. 83, pp. 657\u2013668, 1983."},{"key":"2_CR42","unstructured":"R. Langerak (Ed.), Proceedings of the 3rd SPIN Workshop (SPIN'97), Twente University, The Netherlands, April 1997."},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"S. Leue and P. Ladkin, \u201cImplementing and verifying msc specifications using promela\/XSPIN,\u201d in J.-Ch. Gregoire, G.J. Holzmann, and D. Peled (Eds.), Proceedings of the 2nd Workshop on the SPIN verification System, volume 32 of DIMACS Series in Discrete Mathematics and Theoreticl computer Science, Rutgers University, New Jersey, USA, August 1996. American Mathematical Society, pp. 65\u201389.","DOI":"10.1090\/dimacs\/032\/06"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, \u201cTools and rules for the practicing verifier,\u201d Technical Report STAN-CS-90-1321, Stanford University, June 1990.","DOI":"10.21236\/ADA227320"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking, Kluwer Academic Publishers, Boston, Massachusetts, USA, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"D. Peled, \u201cCombining partial order reductions with on-the-fly model checking,\u201d Form Meth Syst Des, Vol. 8, pp. 39\u201364, 1996.","DOI":"10.1007\/BF00121262"},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"D. Peled, \u201cPartial order reduction: Linear and branching temporal logics and process algebras,\u201d in D. Peled, V. Pratt, and G. Holzmann (Eds.), in Proceedings of the DIMACS Workshop on Partial-Order Methods in Verification (POMIV '96), volume 29 of DIMACS Series in Series in Districte Mathmatices and Theoretical Computer Science, pp. 233\u2013257, Princeton, New Jersey, USA, 1996. American Mathematical Society.","DOI":"10.1090\/dimacs\/029\/13"},{"key":"2_CR48","unstructured":"M. Plath and M. Ryan, \u201cPlug-and-play features,\u201d in Kimbler and Bouma [37], pp. 150\u2013164."},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"A. Pnuelli, \u201cThe temporal semantics of concurrent programs,\u201d Theore Compu Sci, Vol. 13, PP. 45\u201360, 1981.","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"2_CR50","unstructured":"A.W. Roscoe, \u201cModel-checking CSP,\u201d in A.W. Roscoe (Ed.), A Classical Mind: Essays in Honour of C.A.R. Hoare, Prentice-Hall International, Englewood Cliffs, NJ, 1994, chapter 21, pp. 353\u2013378."},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury and I.V. Ramakrishnan, \u201cAutomated inductive verification of parameterized protocols,\u201d in G. Berry, H. Comon, and A. Finkel (Eds.), Proceedings of the 13th International Conference on Computer-aided Verification (CAV 2001), volume 2102 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, July 2001, pp. 25\u201337.","DOI":"10.1007\/3-540-44585-4_4"},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"T.C. Ruys, \u201cLow-fat recipes for SPIN,\u201d in K. Havelund, J. Penix, and W. Visser (Eds.), Proceedings of the 7th SPIN Workshop (SPIN 2000), volume 1885 of Lecture Notes in Computer Science, Springer-Verlag Stanford, California, USA, September 2000, pp. 287\u2013321.","DOI":"10.1007\/10722468_17"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"M. Smith, G. Holzmann, and K. Etessami,\u201c Events and constraints: A graphical editor for capturing logic requirements of programs,\u201d in Proceedings of the 5th IEEE International symposium on Requirements Engineering, Toronto, Canada, IEEE Computer Society, August 2001, pp. 14\u201322.","DOI":"10.1109\/ISRE.2001.948539"},{"key":"2_CR54","unstructured":"M. Thomas, \u201cModelling and analysing user views of telecommunications services,\u201d in P. Dini, R. Boutaba, and L. Logrippo (Eds.), Feature Interactions in Telecommunication Networks IV, IOS Press, Amsterdam, June 1997, pp. 168\u2013182."},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat, and S. Park, \u201cModel checking programs,\u201d in P. Alexander and P. Flener (Eds.), Proceedings of the 15th IEEE Conference on Automated Software Engineering (ASE-2000), IEEE Computer Society Press, Grenoble, France, September 2000, pp. 3\u201312.","DOI":"10.1109\/ASE.2000.873645"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"P. Wolper and V. Lovinfosse, \u201cProperties of large sets of processes with network invariants (extended abstract),\u201d in J. Sifakis (Ed.), Proceedings of the International Workshop in Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, Springer-Verlag. Grenoble, France, June 1989, pp. 68\u201380.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0002-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0002-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0002-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T08:06:40Z","timestamp":1736410000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0002-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":56,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["2"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0002-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,5]]}}}