{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:29Z","timestamp":1775790809028,"version":"3.50.1"},"reference-count":87,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"name":"European Union\u2019s Horizon 2020 Framework Programme through the MSCA network REMARO","award":["956200"],"award-info":[{"award-number":["956200"]}]},{"name":"Italian project NODES","award":["ECS00000036"],"award-info":[{"award-number":["ECS00000036"]}]},{"name":"German DFG","award":["EXC 2050\/1"],"award-info":[{"award-number":["EXC 2050\/1"]}]},{"name":"Dutch NWO","award":["VI.Veni.222.431"],"award-info":[{"award-number":["VI.Veni.222.431"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>\n                    Improved autonomy in robotic systems is needed for innovation in, e.g., the marine sector. Autonomous robots that are let loose in hazardous environments, such as underwater, need to handle uncertainties that stem from both their environment and internal state. While self-adaptation is crucial to cope with these uncertainties, bad decisions may cause the robot to get lost or even to cause severe environmental damage. Autonomous, self-adaptive robots that operate in uncontrolled environments full of uncertainties need to be reliable! Since these uncertainties are hard to replicate in test deployments, we need methods to formally analyse self-adaptive robots operating in uncontrolled environments. In this article, we show how feature-oriented techniques can be used to formally model and analyse self-adaptive robotic systems in the presence of such uncertainties. Self-adaptive systems can be organised as two-layered systems with a\n                    <jats:italic toggle=\"yes\">managed<\/jats:italic>\n                    subsystem handling the domain concerns and a\n                    <jats:italic toggle=\"yes\">managing<\/jats:italic>\n                    subsystem implementing the adaptation logic. We consider a case study of an Autonomous Underwater Vehicle (AUV) for pipeline inspection, in which the managed subsystem of the AUV is modelled as a family of systems, where each family member corresponds to a valid configuration of the AUV which can be seen as an operating mode of the AUV\u2019s behaviour. The managing subsystem of the AUV is modelled as a control layer that is capable of dynamically switching between such valid configurations, depending on both environmental and internal uncertainties. These uncertainties are captured in a probabilistic and highly configurable model. Our modelling approach allows us to exploit powerful formal methods for feature-oriented systems, which we illustrate by analysing safety properties, energy consumption, and multi-objective properties, as well as performing parameter synthesis to analyse to what extent environmental conditions affect the AUV. The case study is realised in the probabilistic feature-oriented modelling language and verification tool ProFeat, and in particular exploits family-based probabilistic and parametric model checking.\n                  <\/jats:p>","DOI":"10.1145\/3709159","type":"journal-article","created":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T06:27:34Z","timestamp":1736144854000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Feature-Oriented Modelling and Analysis of a Self-Adaptive Robotic System"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8515-1809","authenticated-orcid":false,"given":"Juliane","family":"P\u00e4\u00dfler","sequence":"first","affiliation":[{"name":"Department of Informatics, University of Oslo","place":["Oslo, Norway"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"additional","affiliation":[{"name":"CNR-ISTI","place":["Pisa, Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8109-1706","authenticated-orcid":false,"given":"Ferruccio","family":"Damiani","sequence":"additional","affiliation":[{"name":"University of Turin","place":["Torino, Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5718-8276","authenticated-orcid":false,"given":"Clemens","family":"Dubslaff","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology","place":["Eindhoven, Netherlands"]},{"name":"Dresden University of Technology","place":["Eindhoven, Netherlands"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5382-3949","authenticated-orcid":false,"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo","place":["Oslo, Norway"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9948-2748","authenticated-orcid":false,"given":"Silvia Lizeth","family":"Tapia Tarifa","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo","place":["Oslo, Norway"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3542945"},{"key":"e_1_3_3_4_2","series-title":"LNCS","first-page":"269","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification (CAV 1996)","volume":"1102","author":"Aziz Adnan","year":"1996","unstructured":"Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. 1996. Verifying continuous time Markov chains. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV 1996), Rajeev Alur and Thomas A. Henzinger (Eds.). LNCS, Vol. 1102, Springer, Germany, 269\u2013276. DOI:DOI:10.1007\/3-540-61474-5_75"},{"key":"e_1_3_3_5_2","article-title":"On Algorithmic Verification Methods for Probabilistic Systems","author":"Baier Christel","year":"1998","unstructured":"Christel Baier. 1998. On Algorithmic Verification Methods for Probabilistic Systems. Universit\u00e4t Mannheim.","journal-title":"Universit\u00e4t Mannheim"},{"key":"e_1_3_3_6_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, USA."},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1183236.1183264"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","unstructured":"Maurice H. Beekter Beek Rod Chapman Rance Cleaveland Hubert Garavel Rong Gu Ivo ter Horst Jeroen J. A. Keiren Thierry Lecomte Michael Leuschel Kristin Yvonne Rozier Augusto Sampaio Cristina Seceleanu Martyn Thomas Tim A. C. Willemse and Lijun Zhang. 2024. Formal methods in industry. Formal Aspects of Computing 37 1 (2025) 7:1\u20137:38. DOI:DOI:10.1145\/3689374","DOI":"10.1145\/3689374"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09930-8"},{"key":"e_1_3_3_10_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-3-662-54494-5_23","volume-title":"Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017)","volume":"10202","author":"Beek Maurice H. Beekter","year":"2017","unstructured":"Maurice H. Beekter Beek, Erik P. de Vink, and Tim A. C. Willemse. 2017. Family-based model checking with mCRL2. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017). Marieke Huisman and Julia Rubin (Eds.), LNCS, Vol. 10202, Springer, Germany, 387\u2013405. DOI:DOI:10.1007\/978-3-662-54494-5_23"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.11.006"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2853726"},{"key":"e_1_3_3_13_2","first-page":"82:1\u201382:7","volume-title":"Proceedings of the 23rd International Systems and Software Product Line Conference (SPLC 2019)","author":"Beek Maurice H. Beekter","year":"2019","unstructured":"Maurice H. Beekter Beek, Klaus Schmid, and Holger Eichelberger. 2019. Textual variability modeling languages: An overview and considerations. In Proceedings of the 23rd International Systems and Software Product Line Conference (SPLC 2019). ACM, USA, 82:1\u201382:7. DOI:DOI:10.1145\/3307630.3342398"},{"key":"e_1_3_3_14_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/978-3-030-45234-6_12","volume-title":"Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020)","volume":"12076","author":"Beek Maurice H. Beekter","year":"2020","unstructured":"Maurice H. Beekter Beek, Sjef van Loo, Erik P. de Vink, and Tim A.C. Willemse. 2020. Family-based SPL model checking using parity games with variability. In Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020). Heike Wehrheim and Jordi Cabot (Eds.), LNCS, Vol. 12076, Springer, Germany, 245\u2013265. DOI:DOI:10.1007\/978-3-030-45234-6_12"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.292"},{"key":"e_1_3_3_16_2","first-page":"23","volume-title":"Proceedings of the 12th International Conference on Software Product Lines (SPLC 2008)","volume":"2","author":"Bencomo Nelly","year":"2008","unstructured":"Nelly Bencomo, Peter Sawyer, Gordon S. Blair, and Paul Grace. 2008. Dynamically adaptive systems are product lines too: Using model-driven techniques to capture dynamic variability of adaptive systems. In Proceedings of the 12th International Conference on Software Product Lines (SPLC 2008). Steffen Thiel and Klaus Pohl (Eds.), Vol. 2, Lero, University of Limerick, Ireland, 23\u201332."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.06.005"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1080\/01691864.2022.2039761"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-66494-7_1"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2015.354"},{"key":"e_1_3_3_21_2","first-page":"277","volume-title":"Proceedings of the 1st International Conference on Robotic Computing (IRC 2017)","author":"Brugali Davide","year":"2017","unstructured":"Davide Brugali and Nico Hochgeschwender. 2017. Managing the functional variability of robotic perception systems. In Proceedings of the 1st International Conference on Robotic Computing (IRC 2017). IEEE, USA, 277\u2013283. DOI:DOI:10.1109\/IRC.2017.20"},{"key":"e_1_3_3_22_2","first-page":"19:1\u201319:11","volume-title":"Proceedings of the 24th International Systems and Software Product Line Conference (SPLC 2020)","author":"Chrszon Philipp","year":"2020","unstructured":"Philipp Chrszon, Christel Baier, Clemens Dubslaff, and Sascha Kl\u00fcppelholz. 2020. From features to roles. In Proceedings of the 24th International Systems and Software Product Line Conference (SPLC 2020). ACM, USA, 19:1\u201319:11. DOI:DOI:10.1145\/3382025.3414962"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2022.111556"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0432-4"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0234-1"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.09.019"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.86"},{"key":"e_1_3_3_28_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-540-78743-3_2","volume-title":"Proceedings of the 11th International Conference on Fundamental Approaches to Software Engineering (FASE 2008)","volume":"4961","author":"Classen Andreas","year":"2008","unstructured":"Andreas Classen, Patrick Heymans, and Pierre-Yves Schobbens. 2008. What\u2019s in a feature: A requirements engineering perspective. In Proceedings of the 11th International Conference on Fundamental Approaches to Software Engineering (FASE 2008). Jos\u00e9 Luiz Fiadeiro and Paola Inverardi (Eds.), LNCS, Vol. 4961, Springer, Germany, 16\u201330. DOI:DOI:10.1007\/978-3-540-78743-3_2"},{"key":"e_1_3_3_29_2","first-page":"335","volume-title":"Proceedings of the 32nd International Conference on Software Engineering (ICSE 2010)","author":"Classen Andreas","year":"2010","unstructured":"Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, and Jean-Fran\u00e7ois Raskin. 2010. Model checking lots of systems: Efficient verification of temporal properties in software product lines. In Proceedings of the 32nd International Conference on Software Engineering (ICSE 2010). ACM, USA, 335\u2013344. DOI:DOI:10.1145\/1806799.1806850"},{"key":"e_1_3_3_30_2","volume-title":"Software Product Lines: Practices and Patterns","author":"Clements Paul","year":"2001","unstructured":"Paul Clements and Linda Northrop. 2001. Software Product Lines: Practices and Patterns. Addison-Wesley, USA."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36249-1_1"},{"key":"e_1_3_3_32_2","first-page":"141","volume-title":"Proceedings of the 17th International Software Product Line Conference (SPLC 2013)","author":"Cordy Maxime","year":"2013","unstructured":"Maxime Cordy, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, and Axel Legay. 2013. ProVeLines: A product line of verifiers for software product lines. In Proceedings of the 17th International Software Product Line Conference (SPLC 2013). ACM, USA, 141\u2013146. DOI:DOI:10.1145\/2499777.2499781"},{"key":"e_1_3_3_33_2","volume-title":"Generative Programming: Methods, Tools, and Applications","author":"Czarnecki Krzysztof","year":"2000","unstructured":"Krzysztof Czarnecki and Ulrich W. Eisenecker. 2000. Generative Programming: Methods, Tools, and Applications. Addison-Wesley, USA."},{"key":"e_1_3_3_34_2","first-page":"34:1\u201334:8","volume-title":"Proceedings of the 15th Software Product Line Conference (SPLC 2011)","author":"Damiani Ferruccio","year":"2011","unstructured":"Ferruccio Damiani and Ina Schaefer. 2011. Dynamic delta-oriented programming. In Proceedings of the 15th Software Product Line Conference (SPLC 2011). ACM, USA, 34:1\u201334:8. DOI:DOI:10.1145\/2019136.2019175"},{"key":"e_1_3_3_35_2","series-title":"LNCS","first-page":"280","volume-title":"Proceedings of the Revised Selected Papers of the 1st International Colloquium on Theoretical Aspects of Computing (ICTAC 2004)","volume":"3407","author":"Daws Conrado","year":"2004","unstructured":"Conrado Daws. 2004. Symbolic and parametric model checking of discrete-time Markov chains. In Proceedings of the Revised Selected Papers of the 1st International Colloquium on Theoretical Aspects of Computing (ICTAC 2004). Zhiming Liu and Keijiro Araki (Eds.), LNCS, Vol. 3407, Springer, Germany, 280\u2013294. DOI:DOI:10.1007\/978-3-540-31862-0_21"},{"key":"e_1_3_3_36_2","series-title":"LNCS","first-page":"214","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015)","volume":"9206","author":"Dehnert Christian","year":"2015","unstructured":"Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, and Erika \u00c1brah\u00e1m. 2015. PROPhESY: A PRObabilistic ParamEter SYnthesis tool. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015). Daniel Kroening and Corina S. Pasareanu (Eds.), LNCS, Vol. 9206, Springer, Germany, 214\u2013231. DOI:DOI:10.1007\/978-3-319-21690-4_13"},{"key":"e_1_3_3_37_2","series-title":"IFIP","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/978-0-387-73947-2_19","volume-title":"Proceedings of the IFIP WG 8.1 Working Conference on Situational Method Engineering: Fundamentals and Experiences (ME 2007)","volume":"244","author":"Dhungana Deepak","year":"2007","unstructured":"Deepak Dhungana, Paul Gr\u00fcnbacher, and Rick Rabiser. 2007. Domain-specific adaptations of product line variability modeling. In Proceedings of the IFIP WG 8.1 Working Conference on Situational Method Engineering: Fundamentals and Experiences (ME 2007). Jolita Ralyt\u00e9, Sjaak Brinkkemper, and Brian Henderson-Sellers (Eds.), IFIP, Vol. 244, Springer, Germany, 238\u2013251. DOI:DOI:10.1007\/978-0-387-73947-2_19"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00528-0"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0425-2"},{"key":"e_1_3_3_40_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/978-3-662-54494-5_24","volume-title":"Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017)","volume":"10202","author":"Dimovski Aleksandar S.","year":"2017","unstructured":"Aleksandar S. Dimovski and Andrzej W\u0105sowski. 2017. Variability-specific abstraction refinement for family-based model checking. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017). Marieke Huisman and Julia Rubin (Eds.), LNCS, Vol. 10202, Springer, Germany, 406\u2013423. DOI:DOI:10.1007\/978-3-662-54494-5_24"},{"key":"e_1_3_3_41_2","series-title":"LNCS","first-page":"162","volume-title":"Proceedings of the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019)","volume":"11724","author":"Dubslaff Clemens","year":"2019","unstructured":"Clemens Dubslaff. 2019. Compositional feature-oriented systems. In Proceedings of the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019). Peter Csaba \u00d6lveczky and Gwen Sala\u00fcn (Eds.), LNCS, Vol. 11724, Springer, Germany, 162\u2013180. DOI:DOI:10.1007\/978-3-030-30446-1_9"},{"key":"e_1_3_3_42_2","volume-title":"Quantitative Analysis of Configurable and Reconfigurable Systems","author":"Dubslaff Clemens","year":"2021","unstructured":"Clemens Dubslaff. 2021. Quantitative Analysis of Configurable and Reconfigurable Systems. Ph.D. Dissertation. TU Dresden. Retrieved from https:\/\/tud.qucosa.de\/id\/qucosa:78543"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46734-3_5"},{"key":"e_1_3_3_44_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012)","volume":"7561","author":"Forejt Vojtech","year":"2012","unstructured":"Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. 2012. Pareto curves for probabilistic model checking. In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012). Supratik Chakraborty and Madhavan Mukund (Eds.), LNCS, Vol. 7561, Springer, Germany, 317\u2013332. DOI:DOI:10.1007\/978-3-642-33386-6_25"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2018.10.001"},{"key":"e_1_3_3_46_2","first-page":"83","volume-title":"Proceedings of the 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2017)","author":"Gerasimou Simos","year":"2017","unstructured":"Simos Gerasimou, Radu Calinescu, Stepan Shevtsov, and Danny Weyns. 2017. UNDERSEA: An exemplar for engineering self-adaptive unmanned underwater vehicles. In Proceedings of the 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2017). IEEE, USA, 83\u201389. DOI:DOI:10.1109\/SEAMS.2017.19"},{"key":"e_1_3_3_47_2","doi-asserted-by":"crossref","first-page":"6414","DOI":"10.1109\/ICRA.2014.6907806","volume-title":"Proceedings of the International Conference on Robotics and Automation (ICRA 2014)","author":"Gherardi Luca","year":"2014","unstructured":"Luca Gherardi and Davide Brugali. 2014. Modeling and reusing robotic software architectures: the HyperFlex toolchain. In Proceedings of the International Conference on Robotics and Automation (ICRA 2014). IEEE, USA, 6414\u20136420. DOI:DOI:10.1109\/ICRA.2014.6907806"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35813-5_8"},{"key":"e_1_3_3_49_2","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/SPLC.2011.33","volume-title":"Proceedings of the 15th International Software Product Lines Conference (SPLC 2011)","author":"Ghezzi Carlo","year":"2011","unstructured":"Carlo Ghezzi and Amir Molzam Sharifloo. 2011. Verifying non-functional properties of software product lines: Towards an efficient approach using parametric model checking. In Proceedings of the 15th International Software Product Lines Conference (SPLC 2011). IEEE, USA, 170\u2013174. DOI:DOI:10.1109\/SPLC.2011.33"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24667-1_33"},{"key":"e_1_3_3_51_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010)","volume":"6174","author":"Hahn Ernst Moritz","year":"2010","unstructured":"Ernst Moritz Hahn, Holger Hermanns, Bj\u00f6rn Wachter, and Lijun Zhang. 2010. PARAM: A model checker for parametric Markov models. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010). Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.), LNCS, Vol. 6174, Springer, Germany, 660\u2013664. DOI:DOI:10.1007\/978-3-642-14295-6_56"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36583-6_16"},{"key":"e_1_3_3_53_2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1109\/SPLINE.2006.1691586","volume-title":"Proceedings of the 10th International Software Product Line Conference (SPLC 2006)","author":"Hallsteinsen Svein","year":"2006","unstructured":"Svein Hallsteinsen, Erlend Stav, Arnor Solberg, and Jacqueline Floch. 2006. Using product line techniques to build adaptive systems. In Proceedings of the 10th International Software Product Line Conference (SPLC 2006). IEEE, USA, 141\u2013150. DOI:DOI:10.1109\/SPLINE.2006.1691586"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-021-00633-Z"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.20868\/UPM.thesis.23178"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3487921"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.332"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00442-x"},{"key":"e_1_3_3_60_2","doi-asserted-by":"crossref","DOI":"10.21236\/ADA235785","volume-title":"Feature-Oriented Domain Analysis (FODA) Feasibility Study","author":"Kang Kyo C.","year":"1990","unstructured":"Kyo C. Kang, Sholom G. Cohen, James A. Hess, William E. Novak, and A. Spencer Peterson. 1990. Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical Report CMU\/SEI-90-TR-21. Carnegie Mellon University."},{"key":"e_1_3_3_61_2","first-page":"35","volume-title":"Proceedings of the Workshop on Modularization, Composition and Generative Techniques for Product Line Engineering (McGPLE 2008)","author":"K\u00e4stner Christian","year":"2008","unstructured":"Christian K\u00e4stner and Sven Apel. 2008. Integrating compositional and annotative approaches for product line engineering. In Proceedings of the Workshop on Modularization, Composition and Generative Techniques for Product Line Engineering (McGPLE 2008). Neil Loughran, Iris Groher, Roberto Lopez-Herrejon, Sven Apel, and Christa Schwanninger (Eds.), University of Passau, Germany, 35\u201340."},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1160055"},{"key":"e_1_3_3_63_2","series-title":"LNCS","first-page":"585","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011)","volume":"6806","author":"Kwiatkowska Marta","year":"2011","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011). Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), LNCS, Vol. 6806, Springer, Germany, 585\u2013591. DOI:DOI:10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_3_64_2","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1109\/ICAS.2009.24","volume-title":"Proceedings of the 5th International Conference on Autonomic and Autonomous Systems (ICAS 2009)","author":"Liu Yu","year":"2009","unstructured":"Yu Liu and Ren\u00e9 Meier. 2009. Resource-aware contracts for addressing feature interaction in dynamic adaptive systems. In Proceedings of the 5th International Conference on Autonomic and Autonomous Systems (ICAS 2009). IEEE, USA, 346\u2013350. DOI:DOI:10.1109\/ICAS.2009.24"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.09.004"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3342355"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1126\/SCIROBOTICS.ABM6074"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14228090"},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2024.103221"},{"key":"e_1_3_3_70_2","series-title":"LNCS","first-page":"343","volume-title":"Proceedings of the 18th International Conference on integrated Formal Methods (iFM 2023)","volume":"14300","author":"P\u00e4\u00dfler Juliane","year":"2023","unstructured":"Juliane P\u00e4\u00dfler, Maurice H. ter Beek, Ferruccio Damiani, S. Lizeth Tapia Tarifa, and Einar Broch Johnsen. 2023. Formal modelling and analysis of a self-adaptive robotic system. In Proceedings of the 18th International Conference on integrated Formal Methods (iFM 2023). Paula Herber and Anton Wijs (Eds.), LNCS, Vol. 14300, Springer, Germany, 343\u2013363. DOI:DOI:10.1007\/978-3-031-47705-8_18"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","unstructured":"Juliane P\u00e4\u00dfler Maurice H. ter Beek Ferruccio Damiani S. Lizeth Tapia Tarifa and Einar Broch Johnsen. 2023. Formal Modelling and Analysis of a Self-Adaptive Robotic System (Artifact). Zenodo. DOI:DOI:10.5281\/zenodo.8275533","DOI":"10.5281\/zenodo.8275533"},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1"},{"key":"e_1_3_3_73_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016)","volume":"9938","author":"Quatmann Tim","year":"2016","unstructured":"Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. 2016. Parameter synthesis for y models: Faster than ever. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016). Cyrille Artho, Axel Legay, and Doron Peled (Eds.), LNCS, Vol. 9938, Springer, Germany, 50\u201367. DOI:DOI:10.1007\/978-3-319-46520-3_4"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-021-00364-6"},{"key":"e_1_3_3_75_2","volume-title":"Proceedings of the Open-Source Software Workshop of the International Conference on Robotics and Automation (ICRA 2009)","author":"Quigley Morgan","year":"2009","unstructured":"Morgan Quigley, Brian Gerkey, Ken Conley, Josh Faust, Tully Foote, Jeremy Leibs, Eric Berger, Rob Wheeler, and Andrew Ng. 2009. ROS: An open-source Robot Operating System. In Proceedings of the Open-Source Software Workshop of the International Conference on Robotics and Automation (ICRA 2009). IEEE, USA, 6."},{"key":"e_1_3_3_76_2","first-page":"63","volume-title":"Proceedings of the 17th International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2024)","author":"Quijano Sergio","year":"2024","unstructured":"Sergio Quijano, Mahsa Varshosaz, and Andrzej W\u0105sowski. 2024. Modeling and safety analysis of autonomous underwater vehicles behaviors. In Proceedings of the 17th International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2024). IEEE, USA, 63\u201367. DOI:DOI:10.1109\/ICSTW60967.2024.00022"},{"key":"e_1_3_3_77_2","first-page":"181","volume-title":"Proceedings of the 18th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2023)","author":"Silva Gustavo Rezende","year":"2023","unstructured":"Gustavo Rezende Silva, Juliane P\u00e4\u00dfler, Jeroen Zwanepol, Elvin Alberts, S. Lizeth Tapia Tarifa, Ilias Gerostathopoulos, Einar Broch Johnsen, and Carlos Hern\u00e1ndez Corbato. 2023. SUAVE: An exemplar for self-adaptive underwater vehicles. In Proceedings of the 18th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2023). IEEE, USA, 181\u2013187. DOI:DOI:10.1109\/SEAMS59076.2023.00031"},{"key":"e_1_3_3_78_2","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1109\/HASE.2015.34","volume-title":"Proceedings of the 16th International Symposium on High-Assurance Systems Engineering (HASE 2015)","author":"Rodrigues Gena\u00edna N.","year":"2015","unstructured":"Gena\u00edna N. Rodrigues, Vander Alves, Vinicius Nunes, Andr\u00e9 Lanna, Maxime Cordy, Pierre-Yves Schobbens, Amir Molzam Sharifloo, and Axel Legay. 2015. Modeling and verification for probabilistic properties in software product lines. In Proceedings of the 16th International Symposium on High-Assurance Systems Engineering (HASE 2015). IEEE, USA, 173\u2013180. DOI:DOI:10.1109\/HASE.2015.34"},{"key":"e_1_3_3_79_2","first-page":"106","volume-title":"Proceedings of the 17th International Software Product Line Conference (SPLC 2013)","author":"Saller Karsten","year":"2013","unstructured":"Karsten Saller, Malte Lochau, and Ingo Reimund. 2013. Context-aware DSPLs: Model-based runtime adaptation for resource-constrained systems. In Proceedings of the 17th International Software Product Line Conference (SPLC 2013). ACM, USA, 106\u2013113. DOI:DOI:10.1145\/2499777.2500716"},{"key":"e_1_3_3_80_2","series-title":"LNCS","first-page":"77","volume-title":"Proceedings of the 14th Software Product Lines Conference (SPLC 2010)","volume":"6287","author":"Schaefer Ina","year":"2010","unstructured":"Ina Schaefer, Lorenzo Bettini, Viviana Bono, Ferruccio Damiani, and Nico Tanzarella. 2010. Delta-oriented programming of software product lines. In Proceedings of the 14th Software Product Lines Conference (SPLC 2010). Jan Bosch and Jaejoon Lee (Eds.), LNCS, Vol. 6287, Springer, Germany, 77\u201391. DOI:DOI:10.1007\/978-3-642-15579-6_6"},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2008.123"},{"key":"e_1_3_3_82_2","first-page":"136","volume-title":"Proceedings of the 14th International Conference on Requirements Engineering (RE 2006)","author":"Schobbens Pierre-Yves","year":"2006","unstructured":"Pierre-Yves Schobbens, Patrick Heymans, Jean-Christophe Trigaux, and Yves Bontemps. 2006. Feature diagrams: A survey and a formal semantics. In Proceedings of the 14th International Conference on Requirements Engineering (RE 2006). IEEE, USA, 136\u2013145. DOI:DOI:10.1109\/RE.2006.23"},{"key":"e_1_3_3_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/2580950"},{"key":"e_1_3_3_84_2","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/2371401.2371404","volume-title":"Proceedings of the 11th International Conference on Generative Programming and Component Engineering (GPCE 2012)","author":"Th\u00fcm Thomas","year":"2012","unstructured":"Thomas Th\u00fcm, Ina Schaefer, Sven Apel, and Martin Hentschel. 2012. Family-based deductive verification of software product lines. In Proceedings of the 11th International Conference on Generative Programming and Component Engineering (GPCE 2012). ACM, USA, 11\u201320. DOI:DOI:10.1145\/2371401.2371404"},{"key":"e_1_3_3_85_2","series-title":"LNCS","first-page":"329","volume-title":"Proceedings of the 22nd International Symposium on Formal Methods (FM 2018)","volume":"10951","author":"Vandin Andrea","year":"2018","unstructured":"Andrea Vandin, Maurice H. Beekter Beek, Axel Legay, and Alberto Lluch Lafuente. 2018. QFLan: A tool for the quantitative analysis of highly reconfigurable systems. In Proceedings of the 22nd International Symposium on Formal Methods (FM 2018). Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik de Vink (Eds.), LNCS, Vol. 10951, Springer, Germany, 329\u2013337. DOI:DOI:10.1007\/978-3-319-95582-7_19"},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2018.09.001"},{"key":"e_1_3_3_87_2","volume-title":"An Introduction to Self-Adaptive Systems: A Contemporary Software Engineering Perspective","author":"Weyns Danny","year":"2020","unstructured":"Danny Weyns. 2020. An Introduction to Self-Adaptive Systems: A Contemporary Software Engineering Perspective. John Wiley and Sons, UK."},{"key":"e_1_3_3_88_2","first-page":"67","volume-title":"Proceedings of the 5th International C \\(^*\\)  Conference on Computer Science and Software Engineering (C3S2E 2012)","author":"Weyns Danny","year":"2012","unstructured":"Danny Weyns, M. Usman Iftikhar, Didac Gil de la Iglesia, and Tanvir Ahmad. 2012. A survey of formal methods in self-adaptive systems. In Proceedings of the 5th International C \\(^*\\) Conference on Computer Science and Software Engineering (C3S2E 2012). ACM, USA, 67\u201379. DOI:DOI:10.1145\/2347583.2347592"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3709159","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:07:08Z","timestamp":1761919628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3709159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"references-count":87,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3709159"],"URL":"https:\/\/doi.org\/10.1145\/3709159","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"2024-08-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-16","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}