{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T13:16:27Z","timestamp":1775913387219,"version":"3.50.1"},"publisher-location":"Cham","reference-count":117,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with <jats:italic>formal executable specifications<\/jats:italic> and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of <jats:italic>formal patterns<\/jats:italic>. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_1","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:43:47Z","timestamp":1745988227000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Capturing System Designs with Formal Executable Specifications"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100501"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: A parallel statistical model-checking and quantitative analysis tool (2011), in Proc. CALCO 2011, Springer LNCS 6859, 386\u2013392","DOI":"10.1007\/978-3-642-22944-2_28"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Meseguer, J., Gunter, C.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. Electr. Notes Theor. Comput. Sci. 234, 3\u201318 (2009)","DOI":"10.1016\/j.entcs.2009.02.069"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Aoumeur, N., Saake, G.: Integrating and rapid-prototyping UML structural and behavioural diagrams using rewriting logic. In: Pidduck, A.B., Mylopoulos, J., Woo, C.C., \u00d6zsu, M.T. (eds.) Advanced Information Systems Engineering, 14th International Conference, CAiSE 2002, Toronto, Canada, May 27-31, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02348, pp. 296\u2013310. Springer (2002), http:\/\/dx.doi.org\/10.1007\/3-540-47961-9","DOI":"10.1007\/3-540-47961-9"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Ardekani, M.S., Sutra, P., Shapiro, M.: Non-monotonic snapshot isolation: Scalable and strong consistency for geo-replicated transactional systems. In: IEEE 32nd Symposium on Reliable Distributed Systems, SRDS 2013, Braga, Portugal, 1-3 October 2013. pp. 163\u2013172. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/SRDS.2013.25, https:\/\/doi.org\/10.1109\/SRDS.2013.25","DOI":"10.1109\/SRDS.2013.25"},{"key":"1_CR7","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In: Rewriting Techniques and Applications (RTA\u201913). LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2013)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems using multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13\u201350 (2015)","DOI":"10.1016\/j.scico.2014.09.011"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","DOI":"10.1016\/j.scico.2014.02.006"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Bae, K., Meseguer, J., \u00d6lveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3\u201344 (2014)","DOI":"10.1016\/j.scico.2013.09.010"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C.: Extending the Real-Time Maude semantics of Ptolemy to hierarchical DE models. In: \u00d6lveczky [92], pp. 46\u201366, http:\/\/dx.doi.org\/10.4204\/EPTCS.36.3","DOI":"10.4204\/EPTCS.36.3"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C.: Formal model engineering of distributed CPSs using AADL: From behavioral AADL models to Multirate Hybrid Synchronous AADL. In: FACS\u201923. Lecture Notes in Computer Science, vol. 14485, pp. 127\u2013152. Springer (2023)","DOI":"10.1007\/978-3-031-52183-6_7"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Qin, S., Qiu, Z. (eds.) ICFEM. Lecture Notes in Computer Science, vol.\u00a06991, pp. 651\u2013667. Springer (2011)","DOI":"10.1007\/978-3-642-24559-6_43"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Sci. Comput. Program. 77(12), 1235\u20131271 (2012)","DOI":"10.1016\/j.scico.2010.10.002"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: FM. Lecture Notes in Computer Science, vol.\u00a08442, pp. 94\u2013109. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: FM\u201914. Lecture Notes in Computer Science, vol.\u00a08442, pp. 94\u2013109. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Bobba, R., Grov, J., Gupta, I., Liu, S., Meseguer, J., \u00d6lveczky, P.C., Skeirik, S.: Survivability: Design, formal modeling, and validation of cloud storage systems using Maude. In: Campbell, R.H., Kamhoua, C.A., Kwiat, K.A. (eds.) Assured Cloud Computing, chap.\u00a02, pp. 10\u201348. Wiley-IEEE Computer Society Press (2018)","DOI":"10.1002\/9781119428497.ch2"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Boronat, A., Meseguer, J.: An algebraic semantics for MOF. Formal Asp. Comput. 22(3-4), 269\u2013296 (2010)","DOI":"10.1007\/s00165-009-0140-9"},{"key":"1_CR19","unstructured":"Boronat, A.: MOMENT: A Formal Framework for MOdel ManageMENT. Ph.D. thesis, Universitat Polit\u00e8cnica de Val\u00e8ncia, Spain (2007)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Boronat, A., Cars\u00ed, J.A., Ramos, I.: Automatic reengineering in MDA using rewriting logic as transformation engine. In: Gold, N., Syst\u00e4, T. (eds.) Proceedings of the 9th European Conference on Software Maintenance and Reengineering, CSMR 2005, Manchester, UK, March 21-23, 2005, Proceedings. pp. 228\u2013231. IEEE Computer Society (2005)","DOI":"10.1109\/CSMR.2005.14"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: Chechik, M., Wirsing, M. (eds.) Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05503, pp. 18\u201333. Springer (2009), http:\/\/dx.doi.org\/10.1007\/978-3-642-00593-0","DOI":"10.1007\/978-3-642-00593-0"},{"key":"1_CR22","unstructured":"Boronat, A., Meseguer, J.: MOMENT2: EMF model transformations in Maude. In: Vallecillo, A., Sagardui, G. (eds.) Actas de las XIV Jornadas de Ingenier\u00eda del Software y Bases de Datos, JISBD 2009, San Sebasti\u00e1n, Espa\u00f1a, Septiembre 8-11, 2009. pp. 178\u2013179 (2009)"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Brewer, E.A.: Towards robust distributed systems (abstract). In: Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing. p.\u00a07. ACM (2000)","DOI":"10.1145\/343477.343502"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1-3), 386\u2013414 (2006)","DOI":"10.1016\/j.tcs.2006.04.012"},{"key":"1_CR25","unstructured":"Cerone, A., Bernardi, G., Gotsman, A.: A framework for transactional consistency models with atomic visibility. In: Proc. 26th International Conference on Concurrency Theory, CONCUR 2015. LIPIcs, vol.\u00a042, pp. 58\u201371. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Chadha, R., Gunter, C.A., Meseguer, J., Shankesi, R., Viswanathan, M.: Modular preservation of safety properties by cookie-based DoS-protection wrappers. In: Proc. FMOODS 2008. LNCS, vol.\u00a05051, pp. 39\u201358. Springer (2008)","DOI":"10.1007\/978-3-540-68863-1_4"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Chen, S., Meseguer, J., Sasse, R., Wang, H.J., Wang, Y.M.: A systematic approach to uncover security flaws in GUI logic. In: IEEE Symposium on Security and Privacy. pp. 71\u201385. IEEE (2007)","DOI":"10.1109\/SP.2007.6"},{"key":"1_CR28","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude \u2013 A High-Performance Logical Framework. Springer LNCS Vol. 4350 (2007)"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Clavel, M., Egea, M.: ITP\/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04019, pp. 368\u2013373. Springer (2006), http:\/\/dx.doi.org\/10.1007\/11784180","DOI":"10.1007\/11784180_28"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. vol.\u00a071. ENTCS, Elsevier (2002)","DOI":"10.1016\/S1571-0661(05)82531-9"},{"key":"1_CR31","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Theoretical Computer Science 12, 1618\u20131650 (2006)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J., Volk, M.: A Storm is coming: A modern probabilistic model checker. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 592\u2013600. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming open distributed systems in Maude. In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J. (eds.) Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, September 9-11, 2024. pp. 7:1\u20137:12. ACM (2024), https:\/\/doi.org\/10.1145\/3678232.3678237","DOI":"10.1145\/3678232.3678237"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: MTT: The Maude Termination Tool (system description). In: IJCAR 2008. Lecture Notes in Computer Science, vol.\u00a05195, pp. 313\u2013319. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_27"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05749, pp. 246\u2013262. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_15"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s module algebra. Sci. Comput. Program. 66(2), 125\u2013153 (2007)","DOI":"10.1016\/j.scico.2006.07.002"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic and Logic Programming 81, 816\u2013850 (2012)","DOI":"10.1016\/j.jlap.2011.12.004"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F.J., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: Nuitp: An inductive theorem prover for equational program verification. In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J. (eds.) Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, September 9-11, 2024. pp. 6:1\u20136:11. ACM (2024), https:\/\/doi.org\/10.1145\/3678232.3678236","DOI":"10.1145\/3678232.3678236"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Eckhardt, J., M\u00fchlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de\u00a0Lara, Zisman (eds.) FASE. LNCS, vol.\u00a07212, pp. 78\u201393. Springer (2012)","DOI":"10.1007\/978-3-642-28872-2_6"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Egea, M., Rusu, V.: Formal executable semantics for conformance in the MDE framework. Innovations in Systems and Software Engineering 6(1-2), 73\u201381 (2009)","DOI":"10.1007\/s11334-009-0108-1"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Eker, J., Janneck, J.W., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity\u2014the Ptolemy approach. Proceedings of the IEEE 91(2), 127\u2013144 (2003)","DOI":"10.1109\/JPROC.2002.805829"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway logic: Symbolic analysis of biological signaling. In: Proceedings of the Pacific Symposium on Biocomputing. pp. 400\u2013412 (January 2002)","DOI":"10.1142\/9789812799623_0038"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Field, J., Hicks, M. (eds.) POPL. pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Foundations of Security Analysis and Design V, FOSAD 2007\/2008\/2009 Tutorial Lectures, LNCS, vol.\u00a05705, pp. 1\u201350. Springer (2009)","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Fern\u00e1ndez Alem\u00e1n, J.L., Toval \u00c1lvarez, J.A.: Can intuition become rigorous? Foundations for UML model verification tools. In: Titsworth, F.M. (ed.) Proceedings of the 11th International Symposium on Software Reliability Engineering, ISSRE 2000, San Jose, CA, USA, October 8-11, 2000. pp. 344\u2013355. IEEE Computer Society (2000), http:\/\/dx.doi.org\/10.1109\/ISSRE.2000.885885","DOI":"10.1109\/ISSRE.2000.885885"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Gal\u00e1n, D., Garc\u00eda, V., Escobar, S., Meadows, C.A., Meseguer, J.: Protocol dialects as formal patterns. In: Tsudik, G., Conti, M., Liang, K., Smaragdakis, G. (eds.) Computer Security - ESORICS 2023 - 28th European Symposium on Research in Computer Security, The Hague, The Netherlands, September 25-29, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14345, pp. 42\u201361. Springer (2023)","DOI":"10.1007\/978-3-031-51476-0_3"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Garavel, H., ter Beek, M.H., van\u00a0de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12327, pp. 3\u201369. Springer (2020)","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95\u2013146 (1992)","DOI":"10.1145\/147508.147524"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Grov, J., \u00d6lveczky, P.C.: Increasing consistency in multi-site data stores: Megastore-CGC and its formal analysis. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) Software Engineering and Formal Methods - 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08702, pp. 159\u2013174. Springer (2014)","DOI":"10.1007\/978-3-319-10431-7_12"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. Sci. Comput. Program. 99, 235\u2013261 (2015)","DOI":"10.1016\/j.scico.2014.07.003"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Automated Reasoning, Third International Joint Conference, IJCAR 2006. pp. 151\u2013155 (2006)","DOI":"10.1007\/11814771_14"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van\u00a0de Pol, J., Blom, S., van Dijk, T.: LTSmin: High-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a09035, pp. 692\u2013707. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Knapp, A.: Generating rewrite theories from UML collaborations. In: Futatsugi, K., Nakagawa, A.T., Tamai, T. (eds.) Cafe: An Industrial-Strength Algebraic Formal Method, pp. 97\u2013120. Elsevier (2000)","DOI":"10.1016\/B978-044450556-9\/50065-4"},{"key":"1_CR54","unstructured":"Knapp, A.: A Formal Approach to Object-Oriented Software Engineering. Shaker Verlag, Aachen, Germany (2001), phD thesis, Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, 2000."},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"1_CR56","unstructured":"Lee, E.A.: Modeling concurrent real-time processes using discrete events. Ann. Software Eng. 7, 25\u201345 (1999)"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: ISoLA\u201922. Lecture Notes in Computer Science, vol. 13703, pp. 47\u201364. Springer (2022)","DOI":"10.1007\/978-3-031-19759-8_4"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: Rigorous model engineering of hierarchical multirate CPSs in MR-HybridSynchAADL. In: ISoLA\u201924. Lecture Notes in Computer Science, vol. 15220, pp. 243\u2013262. Springer (2024)","DOI":"10.1007\/978-3-031-75107-3_15"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: HybridSynchAADL: Modeling and formal analysis of virtually synchronous CPSs in AADL. In: CAV\u201921. Lecture Notes in Computer Science, vol. 12759, pp. 491\u2013504. Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_23"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Lepri, D., \u00c1brah\u00e1m, E., \u00d6lveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Science of Computer Programming 99, 128\u2013192 (2015)","DOI":"10.1016\/j.scico.2014.06.006"},{"key":"1_CR61","doi-asserted-by":"publisher","unstructured":"Liu, S., Duan, H., Heimes, L., Bearzi, M., Vieli, J., Basin, D.A., Perrig, A.: A formal framework for end-to-end DNS resolution. In: Schulzrinne, H., Misra, V., Kohler, E., Maltz, D.A. (eds.) Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM 2023, New York, NY, USA, 10-14 September 2023. pp. 932\u2013949. ACM (2023). https:\/\/doi.org\/10.1145\/3603269.3604870, https:\/\/doi.org\/10.1145\/3603269.3604870","DOI":"10.1145\/3603269.3604870"},{"key":"1_CR62","unstructured":"Liu, S., Ganhotra, J., Rahman, M.R., Nguyen, S., Gupta, I., Meseguer, J.: Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Trans. Embed. Syst. 4(1), 03:1\u201303:26 (2017)"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.A.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315\u2013344 (2022)","DOI":"10.1145\/3563299"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Ganhotra, J., Gupta, I., Meseguer, J.: Exploring design alternatives for RAMP transactions through statistical model checking. In: Proc. Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017. Lecture Notes in Computer Science, vol. 10610, pp. 298\u2013314. Springer (2017)","DOI":"10.1007\/978-3-319-68690-5_18"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Gupta, I., Meseguer, J.: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. Formal Aspects Comput. 31(5), 503\u2013540 (2019)","DOI":"10.1007\/s00165-019-00489-w"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic analysis of consistency properties of distributed transaction systems in Maude. In: Proc. TACAS 2019, Part II. Lecture Notes in Computer Science, vol. 11428, pp. 40\u201357. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_3"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"Liu, S., Rahman, M.R., Skeirik, S., Gupta, I., Meseguer, J.: Formal modeling and analysis of Cassandra in Maude. In: Formal Methods and Software Engineering \u2013 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08829, pp. 332\u2013347. Springer (2014)","DOI":"10.1007\/978-3-319-11737-9_22"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Liu, S., Sandur, A., Meseguer, J., \u00d6lveczky, P.C., Wang, Q.: Generating correct-by-construction distributed implementations from formal Maude designs. In: Proc. NASA Formal Methods: 12th International Symposium, NFM 2020,. Lecture Notes in Computer Science, vol. 12229, pp. 22\u201340. Springer (2020)","DOI":"10.1007\/978-3-030-55754-6_2"},{"key":"1_CR69","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd. Edition, pp. 1\u201387. Kluwer Academic Publishers (2002), first published as SRI Tech. Report SRI-CSL-93-05, August 1993","DOI":"10.1007\/978-94-017-0464-9_1"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project. Theoretical Computer Science 373, 213\u2013237 (2007)","DOI":"10.1016\/j.tcs.2006.12.018"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Proceedings of ECOOP\u201902, M\u00e1laga, Spain, June 2002. pp. 1\u201336. Springer LNCS 2374 (2002)","DOI":"10.1007\/3-540-47993-7_1"},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: General logics. In: et\u00a0al., H.D.E. (ed.) Logic Colloquium\u201987. pp. 275\u2013329. North-Holland (1989)","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73\u2013155 (1992)","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314\u2013390. MIT Press (1993)","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Algebraic and Logic Programming 81, 721\u2013781 (2012)","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Taming distributed system complexity through formal patterns. Sci. Comput. Program. 83, 3\u201334 (2014)","DOI":"10.1016\/j.scico.2013.07.004"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"1_CR78","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Building correct-by-construction systems with formal patterns. In: Madeira, A., Martins, M.A. (eds.) Recent Trends in Algebraic Development Techniques - 26th IFIP WG 1.3 International Workshop, WADT 2022, Aveiro, Portugal, June 28-30, 2022, Revised Selected Papers. Lecture Notes in Computer Science, vol. 13710, pp. 3\u201324. Springer (2022)","DOI":"10.1007\/978-3-031-43345-0_1"},{"key":"1_CR79","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Checking sufficient completeness by inductive theorem proving. In: Bae, K. (ed.) Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022, Revised Selected Papers. Lecture Notes in Computer Science, vol. 13252, pp. 171\u2013190. Springer (2022)","DOI":"10.1007\/978-3-031-12441-9_9"},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for real-time systems. In: 12th International Conference on Formal Engineering Methods (ICFEM 2010). vol.\u00a06447, pp. 303\u2013320. Springer LNCS (2010)","DOI":"10.1007\/978-3-642-16901-4_21"},{"key":"1_CR81","doi-asserted-by":"crossref","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1\u201337 (2012)","DOI":"10.1016\/j.tcs.2012.05.040"},{"key":"1_CR82","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project: A progress report. Inf. Comput. 231, 38\u201369 (2013)","DOI":"10.1016\/j.ic.2013.08.004"},{"key":"1_CR83","doi-asserted-by":"crossref","unstructured":"Miller, S., Cofer, D., Sha, L., Meseguer, J., Al-Nayeem, A.: Implementing logical synchrony in integrated modular avionics. In: Proc. 28th Digital Avionics Systems Conference. IEEE (2009)","DOI":"10.1109\/DASC.2009.5347579"},{"key":"1_CR84","doi-asserted-by":"crossref","unstructured":"Mokhati, F., Badri, M.: Generating Maude specifications from UML use case diagrams. Journal of Object Technology 8(2), 319\u2013136 (2009)","DOI":"10.5381\/jot.2009.8.2.a2"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Mokhati, F., Gagnon, P., Badri, M.: Verifying UML diagrams with model checking: A rewriting logic based approach. In: Mathur, A., Wong, W.E. (eds.) Proceedings of the Seventh International Conference on Quality Software, QSIC 2007, Portland, Oregon, USA, October 11-12, 2007. pp. 356\u2013362. IEEE Computer Society (2007)","DOI":"10.1109\/QSIC.2007.4385520"},{"key":"1_CR86","doi-asserted-by":"crossref","unstructured":"Mokhati, F., Sahraoui, B., Bouzaher, S., Kimour, M.T.: A tool for specifying and validating agents\u2019 interaction protocols: From Agent UML to Maude. Journal of Object Technology 9(3), 59\u201377 (2010)","DOI":"10.5381\/jot.2010.9.3.a2"},{"key":"1_CR87","doi-asserted-by":"crossref","unstructured":"Nakajima, S.: Using algebraic specification techniques in development of object-oriented frameworks. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II. Lecture Notes in Computer Science, vol.\u00a01709, pp. 1664\u20131683. Springer (1999)","DOI":"10.1007\/3-540-48118-4_38"},{"key":"1_CR88","doi-asserted-by":"crossref","unstructured":"Nakajima, S., Futatsugi, K.: An object-oriented modeling method for algebraic specifications in CafeOBJ. In: Proceedings of the 19th International Conference on Software Engineering, ICSE\u201997, Boston, Massachussets, May 17-23, 1997. ACM Press (1997)","DOI":"10.1145\/253228.253238"},{"key":"1_CR89","doi-asserted-by":"crossref","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015)","DOI":"10.1145\/2699417"},{"key":"1_CR90","doi-asserted-by":"crossref","unstructured":"Olarte, C., Pimentel, E., Rocha, C.: A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems. Journal of Logical and Algebraic Methods in Programming 130, 100827 (2023)","DOI":"10.1016\/j.jlamp.2022.100827"},{"key":"1_CR91","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1\u20132), 161\u2013196 (2007)","DOI":"10.1007\/s10990-007-9001-5"},{"key":"1_CR92","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C. (ed.): Proceedings of the First International Workshop on Rewriting Techniques for Real-Time Systems, RTRTS 2010, Longyearbyen, Spitsbergen, Norway, April 6-9, 2010. Electronic Proceedings in Theoretical Computer Science, Computing Research Repository (CoRR)","DOI":"10.4204\/EPTCS.36.0"},{"key":"1_CR93","unstructured":"\u00d6lveczky, P.C. (ed.): Rewriting Logic and its Applications. 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol.\u00a06381. Springer (2010)"},{"key":"1_CR94","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: FMOODS\/FORTE\u201910. Lecture Notes in Computer Science, vol.\u00a06117, pp. 47\u201362. Springer (2010)","DOI":"10.1007\/978-3-642-13464-7_5"},{"key":"1_CR95","doi-asserted-by":"crossref","unstructured":"Riesco, A., Ogata, K.: An integrated tool set for verifying cafeobj specifications. Journal of Systems and Software 189, 111302 (2022). https:\/\/doi.org\/https:\/\/doi.org\/10.1016\/j.jss.2022.111302","DOI":"10.1016\/j.jss.2022.111302"},{"key":"1_CR96","doi-asserted-by":"crossref","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: On the behavioral semantics of real-time domain specific visual languages. In: \u00d6lveczky [93], pp. 174\u2013190","DOI":"10.1007\/978-3-642-16310-4_12"},{"key":"1_CR97","doi-asserted-by":"crossref","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. J. Log. Algebraic Methods Program. 123, 100700 (2021)","DOI":"10.1016\/j.jlamp.2021.100700"},{"key":"1_CR98","doi-asserted-by":"crossref","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: QMaude: Quantitative specification and verification in rewriting logic. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods - 25th International Symposium, FM 2023, L\u00fcbeck, Germany, March 6-10, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14000, pp. 240\u2013259. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_15"},{"key":"1_CR99","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled systems in rewriting logic. CoRR abs\/2401.07616 (2024)"},{"key":"1_CR100","unstructured":"Sasse, R.: Security models in rewriting logic for cryptographic protocols and browsers. Ph.D. thesis, University of Illinois at Urbana-Champaign (2012), http:\/\/hdl.handle.net\/2142\/34373"},{"key":"1_CR101","doi-asserted-by":"crossref","unstructured":"Sasse, R., King, S.T., Meseguer, J., Tang, S.: IBOS: A correct-by-construction modular browser. In: FACS 2012. Lecture Notes in Computer Science, vol.\u00a07684, pp. 224\u2013241. Springer (2013)","DOI":"10.1007\/978-3-642-35861-6_14"},{"key":"1_CR102","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C., Stehr, M.O.: An executable formalization of the hol\/nuprl connection in the metalogical framework twelf. pp. 150\u2013166 (11 2006). https:\/\/doi.org\/10.1007\/11916277_11","DOI":"10.1007\/11916277_11"},{"key":"1_CR103","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Horv\u00e1th, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools \u201913, Torino, Italy, December 10-12, 2013. pp. 310\u2013315. ICST\/ACM (2013)"},{"key":"1_CR104","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F.: A Rewriting Approach to Concurrent Programming Language Design and Semantics. Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign (2010), http:\/\/hdl.handle.net\/2142\/18252, http:\/\/hdl.handle.net\/2142\/18252"},{"key":"1_CR105","doi-asserted-by":"crossref","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: K-Maude: A rewriting based tool for semantics of programming languages. In: \u00d6lveczky [93], pp. 104\u2013122","DOI":"10.1007\/978-3-642-16310-4_8"},{"key":"1_CR106","doi-asserted-by":"crossref","unstructured":"Skeirik, S., Meseguer, J., Rocha, C.: Verification of the IBOS browser security properties in reachability logic. In: Proc. WRLA 2020. LNCS, vol. 12328, pp. 176\u2013196. Springer (2020)","DOI":"10.1007\/978-3-030-63595-4_10"},{"key":"1_CR107","unstructured":"Skeirik, S.: Rewriting-based symbolic methods for distributed system verification. Ph.D. thesis, University of Illinois at Urbana-Champaign (2019), http:\/\/hdl.handle.net\/2142\/106224"},{"key":"1_CR108","doi-asserted-by":"publisher","unstructured":"Sovran, Y., Power, R., Aguilera, M.K., Li, J.: Transactional storage for geo-replicated systems. In: Wobber, T., Druschel, P. (eds.) Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, SOSP 2011, Cascais, Portugal, October 23-26, 2011. pp. 385\u2013400. ACM (2011). https:\/\/doi.org\/10.1145\/2043556.2043592, https:\/\/doi.org\/10.1145\/2043556.2043592","DOI":"10.1145\/2043556.2043592"},{"key":"1_CR109","doi-asserted-by":"crossref","unstructured":"Stehr, M.O., Naumov, P., Meseguer, J.: The HOL\/NuPRl proof translator\u2014A practical approach to formal interoperability. In: Proc. $$14^{th}$$ Intl. Conf. on Theorem Proving In Higher Order Logics (TPHOL\u20192001) Edinburgh, Scotland, September 2001. pp. 329\u2013345. Springer LNCS 2152 (2001)","DOI":"10.1007\/3-540-44755-5_23"},{"key":"1_CR110","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J.: Distributed real-time emulation of formally-defined patterns for safe medical device control. In: \u00d6lveczky [92], pp. 158\u2013177, http:\/\/dx.doi.org\/10.4204\/EPTCS.36.9","DOI":"10.4204\/EPTCS.36.9"},{"key":"1_CR111","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J.: Formal specification of button-related fault-tolerance micropatterns. In: Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a08663, pp. 263\u2013279. Springer (2014)","DOI":"10.1007\/978-3-319-12904-4_15"},{"key":"1_CR112","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J., Sha, L.: A formal pattern architecture for safe medical systems. In: Proc. WRLA 2010. vol.\u00a06381, pp. 157\u2013173. Springer LNCS (2010)","DOI":"10.1007\/978-3-642-16310-4_11"},{"key":"1_CR113","unstructured":"Tang, S.: Towards Secure Web Browsing. Ph.D. thesis, University of Illinois at Urbana-Champaign (2011), 2011-05-25, http:\/\/hdl.handle.net\/2142\/24307"},{"key":"1_CR114","doi-asserted-by":"crossref","unstructured":"Verdejo, A.: Building tools for LOTOS symbolic semantics in maude. In: Formal Techniques for Networked and Distributed Systems - FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings. pp. 292\u2013307 (2002)","DOI":"10.1007\/3-540-36135-9_19"},{"key":"1_CR115","doi-asserted-by":"crossref","unstructured":"Weghorn, T., Liu, S., Sprenger, C., Perrig, A., Basin, D.: N-tube: Formally verified secure bandwidth reservation in path-aware internet architectures. In: 2022 IEEE 35th Computer Security Foundations Symposium (CSF). pp. 147\u2013162 (2022)","DOI":"10.1109\/CSF54842.2022.9919646"},{"key":"1_CR116","doi-asserted-by":"crossref","unstructured":"Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic and its Applications, WRLA\u201996, Asilomar, California, September 3-6, 1996. Electronic Notes in Theoretical Computer Science, vol.\u00a04, pp. 322\u2013360. Elsevier (1996), http:\/\/dx.doi.org\/10.1016\/S1571-0661(04)00046-5","DOI":"10.1016\/S1571-0661(04)00046-5"},{"key":"1_CR117","doi-asserted-by":"crossref","unstructured":"Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. Theoretical Computer Science 285(2), 519\u2013560 (2002), http:\/\/dx.doi.org\/10.1016\/S0304-3975(01)00367-X","DOI":"10.1016\/S0304-3975(01)00367-X"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:23Z","timestamp":1745988323000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":117,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}