乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:20:40Z","timestamp":1742941240411,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452339"},{"type":"electronic","value":"9783030452346"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45234-6_12","type":"book-chapter","created":{"date-parts":[[2020,4,20]],"date-time":"2020-04-20T14:04:23Z","timestamp":1587391463000},"page":"245-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Family-Based SPL Model Checking Using Parity Games with Variability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"given":"Sjef","family":"van Loo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9514-2260","authenticated-orcid":false,"given":"Erik P.","family":"de Vink","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3049-7962","authenticated-orcid":false,"given":"Tim A. C.","family":"Willemse","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"A. Classen, P. Heymans, and P.-Y. Schobbens. What\u2019s in a Feature: A Requirements Engineering Perspective. In J.L. Fiadeiro and P. Inverardi, editors, FASE\u201908, volume 4961 of LNCS, pages 16\u201330. Springer, 2008.","DOI":"10.1007\/978-3-540-78743-3_2"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"S.\u00a0Apel, D.\u00a0Batory, C.\u00a0K\u00e4stner, and G.\u00a0Saake. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, 2013.","DOI":"10.1007\/978-3-642-37521-7"},{"key":"12_CR3","unstructured":"A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model Checking $$\\underline{\\text{Lots}}$$ of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In Proc. ICSE\u201910, pages 335\u2013344. ACM, 2010."},{"key":"12_CR4","unstructured":"A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and their Application to LTL Model Checking. IEEE Trans. Softw. Eng., 39(8):1069\u20131089, 2013."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"M. Cordy, X. Devroey, A. Legay, G. Perrouin, A. Classen, P. Heymans, P.-Y. Schobbens, and J.-F. Raskin. A Decade of Featured Transition Systems. In M.H. ter Beek, A. Fantechi, and L. Semini, editors, From Software Engineering to Formal Methods and Tools, and Back, volume 11865 of LNCS, pages 285\u2013312. Springer, 2019.","DOI":"10.1007\/978-3-030-30985-5_18"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"T. Th\u00fcm, S. Apel, C. K\u00e4stner, I. Schaefer, and G. Saake. A Classification and Survey of Analysis Strategies for Software Product Lines. ACM Comput. Surv., 47(1):6:1\u20136:45, 2014.","DOI":"10.1145\/2580950"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf., 14(5):589\u2013612, 2012.","DOI":"10.1007\/s10009-012-0234-1"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. ProVeLines: a product line of verifiers for software product lines. In Proc. SPLC\u201913, volume 2, pages 141\u2013146. ACM, 2013.","DOI":"10.1145\/2499777.2499781"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"M.H. ter Beek, F. Mazzanti, and A. Sulova. VMC: A Tool for Product Variability Analysis. In D. Giannakopoulou and D. M\u00e9ry, editors, Proc. FM\u201912, volume 7436 of LNCS, pages 450\u2013454. Springer, 2012.","DOI":"10.1007\/978-3-642-32759-9_36"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"P. Chrszon, C. Dubslaff, S. Kl\u00fcppelholz, and C. Baier. Family-Based Modeling and Analysis for Probabilistic Systems \u2013 Featuring ProFeat. In P. Stevens and A. W\u0105sowski, editors, Proc. FASE\u201916, volume 9633 of LNCS, pages 287\u2013304, 2016.","DOI":"10.1007\/978-3-662-49665-7_17"},{"key":"12_CR11","unstructured":"P. Chrszon, C. Dubslaff, S. Kl\u00fcppelholz, and C. Baier. ProFeat: feature-oriented engineering for family-based probabilistic model checking. Form. Asp. Comp., 30(1):45\u201375, 2018."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"M.H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin. A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Trans. Softw. Eng., 2018.","DOI":"10.1007\/978-3-030-34968-4_35"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"A. Vandin, M.H. ter Beek, A. Legay, and A. Lluch Lafuente. QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems. In K. Havelund, J. Peleska, B. Roscoe, and E. de Vink, editors, Proc. FM\u201918, volume 10951 of LNCS, pages 329\u2013337. Springer, 2018.","DOI":"10.29007\/1mjd"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic Model Checking of Software Product Lines. In Proc. ICSE\u201911, pages 321\u2013330. ACM, 2011.","DOI":"10.1145\/1985793.1985838"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program., 80(B):416\u2013439, 2014.","DOI":"10.1016\/j.scico.2013.09.019"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski, A.S. Al-Sibahi, C. Brabrand, and A. W\u0105sowski. Family-Based Model Checking Without a Family-Based Model Checker. In B. Fischer and J. Geldenhuys, editors, Proc. SPIN\u201915, volume 9232 of LNCS, pages 282\u2013299. Springer, 2015.","DOI":"10.1007\/978-3-319-23404-5_18"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"M. Lochau, S. Mennicke, H. Baller, and L. Ribbeck. Incremental model checking of delta-oriented software product lines. J. Log. Algebr. Meth. Program., 85(1):245\u2013267, 2016.","DOI":"10.1016\/j.jlamp.2015.09.004"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"M.H. ter Beek and E.P. de Vink. Using mCRL2 for the Analysis of Software Product Lines. In Proc. FormaliSE\u201914, pages 31\u201337. IEEE, 2014.","DOI":"10.1145\/2593489.2593493"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. Family-Based Model Checking with mCRL2. In M. Huisman and J. Rubin, editors, Proc. FASE\u201917, volume 10202 of LNCS, pages 387\u2013405. Springer, 2017.","DOI":"10.1007\/978-3-662-54494-5_23"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, W. Wesselink, and T.A.C. Willemse. An Overview of the mCRL2 Toolset and Its Recent Advances. In N. Piterman and S.A. Smolka, editors, Proc. TACAS\u201913, volume 7795 of LNCS, pages 199\u2013213. Springer, 2013.","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"O. Bunte, J.F. Groote, J.J.A. Keiren, M. Laveaux, T. Neele, E.P. de Vink, W. Wesselink, A. Wijs, and T.A.C. Willemse. The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability. In T. Vojnar and L. Zhang, editors, Proc. TACAS\u201919, volume 11428 of LNCS, pages 21\u201339. Springer, 2019.","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. Towards a Feature mu-Calculus Targeting SPL Verification. Electr. Proc. Theor. Comput. Sci., 206:61\u201375, 2016.","DOI":"10.4204\/EPTCS.206.6"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski. Symbolic Game Semantics for Model Checking Program Families. In D. Bo\u0161na\u010dki and A. Wijs, editors, Proc. SPIN\u201916, volume 9641 of LNCS, pages 19\u201337. Springer, 2016.","DOI":"10.1007\/978-3-319-32582-8_2"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski and A. W\u0105sowski. Variability-Specific Abstraction Refinement for Family-Based Model Checking. In M. Huisman and J. Rubin, editors, Proc. FASE\u201917, volume 10202 of LNCS, pages 406\u2013423. Springer, 2017.","DOI":"10.1007\/978-3-662-54494-5_24"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski. Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL$$^*$$. In A. Russo and A. Sch\u00fcrr, editors, Proc. FASE\u201918, volume 10802 of LNCS, pages 301\u2013318. Springer, 2018.","DOI":"10.1007\/978-3-319-89363-1_17"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski, A. Legay, and A. W\u0105sowski. Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL. In R. H\u00e4hnle and W. van der Aalst, editors, Proc. FASE\u201919, volume 11424 of LNCS, pages 192\u2013209. Springer, 2019.","DOI":"10.1016\/j.tcs.2020.06.011"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135\u2013183, 1998.","DOI":"10.1016\/S0304-3975(98)00009-7"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"O. Friedmann and M. Lange. Solving Parity Games in Practice. In Z. Liu and A.P. Ravn, editors, Proc. ATVA\u201909, volume 5799 of LNCS, pages 182\u2013196. Springer, 2009.","DOI":"10.1007\/978-3-642-04761-9_15"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"T. van Dijk. Oink: An Implementation and Evaluation of Modern Parity Game Solvers. In D. Beyer and M. Huisman, editors, Proc. TACAS\u201918, volume 10805 of LNCS, pages 291\u2013308. Springer, 2018.","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"J.C. Bradfield and I. Walukiewicz. The mu-calculus and model checking. In E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, editors, Handbook of Model Checking, chapter 26, pages 871\u2013919. Springer, 2018.","DOI":"10.1007\/978-3-319-10575-8_26"},{"key":"12_CR31","unstructured":"J. Lind-Nielsen. BuDDy: A Binary Decision Diagram package. Technical Report IT-TR 1999\u2013028, IT University of Copenhagen, 1999."},{"key":"12_CR32","unstructured":"H. Cohen, J. Whaley, J. Wildt, and N. Gorogiannis. BuDDy: A Binary Decision Diagram library. http:\/\/sourceforge.net\/p\/buddy\/ . Last visited October 18, 2019."},{"key":"12_CR33","unstructured":"J. Kramer, J. Magee, M. Sloman, and A. Lister. CONIC: an integrated approach to distributed computer control systems. IEE Proc. E, 130(1):1\u201310, 1983."},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"X. Devroey, G. Perrouin, M. Papadakis, A. Legay, P.-Y. Schobbens, and P. Heymans. Featured Model-based Mutation Analysis. In Proc. ICSE\u201916, pages 655\u2013666. ACM, 2016.","DOI":"10.1145\/2884781.2884821"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski, A.S. Al-Sibahi, C. Brabrand, and A. W\u0105sowski. Efficient family-based model checking via variability abstractions. Int. J. Softw. Tools Technol. Transf., 19(5):585\u2013603, 2017.","DOI":"10.1007\/s10009-016-0425-2"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"M.H. ter Beek, F. Damiani, M. Lienhardt, F. Mazzanti, and L. Paolini. Static Analysis of Featured Transition Systems. In Proc. SPLC\u201919, pages 39\u201351. ACM, 2019.","DOI":"10.1145\/3336294.3336295"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"M. Plath and M. Ryan. Feature integration using a feature construct. Sci. Comput. Program., 41(1):53\u201384, 2001.","DOI":"10.1016\/S0167-6423(00)00018-6"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"A.S. Dimovski. CTL$$^*$$ family-based model checking using variability abstractions and modal transition systems. Int. J. Softw. Tools Technol. Transf., 22(1):35\u201355, 2020.","DOI":"10.1007\/s10009-019-00528-0"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45234-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,9]],"date-time":"2021-03-09T20:37:42Z","timestamp":1615322262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45234-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452339","9783030452346"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45234-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"81","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}