{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:19:20Z","timestamp":1760141960974,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032071316","type":"print"},{"value":"9783032071323","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:00:00Z","timestamp":1760140800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:00:00Z","timestamp":1760140800000},"content-version":"vor","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":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Formal verification tools like model checkers have long demonstrated their capability to ensure mission-critical properties are satisfied, yet their adoption in the aerospace and defense industries remains limited. Among the various reasons for slow uptake, difficulty in understanding analysis results (i.e., counterexamples) tops\u00a0the list of multiple surveys. In previous work, our team developed AGREE, an assume-guarantee compositional reasoning tool\u00a0for architecture models. Like many other model checkers, AGREE generates potentially large counterexamples in a tabular format containing variable values at each time step of program execution up to the property violation, which can be difficult to interpret, especially for novice formal methods users. In this paper,\u00a0we present our approach for achieving explainable compositional reasoning using AGREE in combination with generative AI and we introduce AGREE-Dog, an open-source generative AI copilot integrated into the OSATE IDE. AGREE-Dog automates 16 DevOps and ProofOps steps, utilizing a novel context-selection and memory management system to efficiently manage evolving artifacts and historical interactions. We introduce structural and temporal metrics to evaluate the typically overlooked human contributions in generative AI-supported workflows. Evaluations using 13 UV fault-injection scenarios demonstrate a significant reduction in manual effort (less than 0.1\u00a0% of tokens authored by users), rapid convergence of counterexample repairs (84.6\u00a0% resolved in a single iteration, accuracy increasing to about 92\u00a0% after two iterations, and reaching 100\u00a0% within three iterations), and low LLM latency (average LLM response under 22\u00a0s, with negligible AGREE-Dog computational overhead). We also discuss limitations and future work. These promising results motivate further exploration into explainable model-based systems engineering (MBSE).<\/jats:p>","DOI":"10.1007\/978-3-032-07132-3_8","type":"book-chapter","created":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T05:27:44Z","timestamp":1760074064000},"page":"117-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["AGREE-Dog Copilot: A Neuro-Symbolic Approach to\u00a0Enhanced Model-Based Systems Engineering"],"prefix":"10.1007","author":[{"given":"Amer","family":"Tahat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Isaac","family":"Amundson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Hardin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Darren","family":"Cofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,11]]},"reference":[{"key":"8_CR1","unstructured":"AWS News Blog: Prevent factual errors from llm hallucinations with mathematically sound automated reasoning checks (preview). AWS Blog Post(2024), Accessed 11 May 2025"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-41010-9_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"JA Davis","year":"2013","unstructured":"Davis, J.A., et al.: Study on the barriers to the industrial adoption of formal methods. In: Pecheur, C., Dierkes, M. (eds.) Formal Methods for Industrial Critical Systems, pp. 63\u201377. Springer, Berlin Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41010-9_5"},{"key":"8_CR4","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language. Addison-Wesley Professional, 1st edn. (2012)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: Whole-proof generation and repair with large language models. arXiv preprint arXiv:2303.04910 (2023)","DOI":"10.1145\/3611643.3616243"},{"key":"8_CR6","unstructured":"INSPECTA Project: Inspecta. https:\/\/loonwerks.com\/projects\/inspecta.html, Accessed: 19 May 2025"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Kaleeswaran, A.P., Nordmann, A., Vogel, T., Grunske, L.: A systematic literature review on counterexample explanation. Inform. Softw. Technol. 145 (2022)","DOI":"10.1016\/j.infsof.2021.106800"},{"key":"8_CR8","unstructured":"Megill, N., Wheeler, D.A.: Metamath: A computer language for mathematical proofs (2019)"},{"key":"8_CR9","unstructured":"Mirzadeh, S.I., Alizadeh, K., Shahrokhi, H., Tuzel, O., Bengio, S., Farajtabar, M.: GSM-symbolic: understanding the limitations of mathematical reasoning in large language models. In: The Thirteenth International Conference on Learning Representations (2025). https:\/\/openreview.net\/forum?id=AjXkRZIvjB"},{"key":"8_CR10","unstructured":"Object Management Group (OMG): Systems modeling language (sysml) v2 specification. (2024), Accessed 19 May 2025"},{"key":"8_CR11","unstructured":"Pei, K., Bieber, D., Shi, K., et\u00a0al.: Can large language models reason about program invariants? Proceedings of the 40th International Conference on Machine Learning (July 2023)"},{"key":"8_CR12","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 (2020)"},{"key":"8_CR13","unstructured":"RTCA: DO-333: Formal Methods Supplement to DO-178C and DO-278A (December 2011)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Closed-loop verifiable code generation. arXiv preprint arXiv:2310.17807 (2024)","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"8_CR15","unstructured":"Tahat, A., Hardin, D., Petz, A., Alexander, P.: Metrics for large language model generated proofs in a high-assurance application domain. In: High Confidence Software and Systems Conference (HCSS 2024) (2024)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Tahat, A., Hardin, D., Petz, A., Alexander, P.: Proof repair utilizing large language models: A case study on the copland remote attestation proofbase. In: Proceedings of International Symposium On Leveraging Applications of Formal Methods Verification and Validation (AISolA) (2024)","DOI":"10.1007\/978-3-031-75434-0_10"},{"key":"8_CR17","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating large language models in automated program verification. arXiv preprint arXiv:2310.04870 (2023)"},{"key":"8_CR18","unstructured":"Zhang, S., First, E., Ringer, T.: Getting more out of large language models for proofs. arXiv preprint arXiv:2305.04369 (2023)"}],"container-title":["Lecture Notes in Computer Science","Bridging the Gap Between AI and Reality"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07132-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T05:27:51Z","timestamp":1760074071000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07132-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,11]]},"ISBN":["9783032071316","9783032071323"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07132-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,11]]},"assertion":[{"value":"11 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Bridging the Gap between AI and Reality","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aisola2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2025-aisola.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}