{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:29:41Z","timestamp":1770755381255,"version":"3.50.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T00:00:00Z","timestamp":1726099200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T00:00:00Z","timestamp":1726099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100009890","name":"Provincia Autonoma di Trento","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100009890","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100031478","name":"NextGenerationEU","doi-asserted-by":"crossref","award":["PE00000013"],"award-info":[{"award-number":["PE00000013"]}],"id":[{"id":"10.13039\/100031478","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004004","name":"Universit\u00e0 degli Studi di Trento","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004004","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The analysis of legacy systems requires the automated extraction of high-level specifications. We propose a framework, called Abstraction Modulo Stability, for the analysis of transition systems operating in stable states, and responding with run-to-completion transactions to external stimuli. The abstraction captures, in the form of a finite state machine, the effects of external stimuli on the system state. This approach is parametric on a set of predicates of interest and on the definition of stability. We consider some possible stability definitions, which yield different practically relevant abstractions, and propose parametric algorithms for abstraction computation. The framework is evaluated in terms of expressivity and adequacy within an industrial project with the Italian Railway Network, on reverse engineering of relay-based interlocking circuits to extract specifications for a computer-based reimplementation.<\/jats:p>","DOI":"10.1007\/s10703-024-00461-2","type":"journal-article","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T08:02:19Z","timestamp":1726128139000},"page":"134-169","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Abstraction Modulo Stability"],"prefix":"10.1007","volume":"66","author":[{"given":"Anna","family":"Becchi","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,12]]},"reference":[{"key":"461_CR1","unstructured":"de\u00a0Almeida\u00a0Pereira DI (2020) Analysis and formal specification of relay-based railway interlocking systems. (analyse et sp\u00e9cification formelle des syst\u00e8mes d\u2019enclenchement ferroviaire bas\u00e9s sur les relais). PhD thesis, \u00c9cole centrale de Lille, Villeneuve-d\u2019Ascq, France"},{"key":"461_CR2","doi-asserted-by":"crossref","unstructured":"Amendola A, Becchi A, Cavada R, et\u00a0al. (2020) A model-based approach to the design, verification and deployment of railway interlocking system. In: ISoLA (3), lecture notes in computer science, vol 12478. Springer, pp 240\u2013254","DOI":"10.1007\/978-3-030-61467-6_16"},{"key":"461_CR3","doi-asserted-by":"publisher","unstructured":"Amendola A, Becchi A, Cavada R, et\u00a0al. (2022) NORMA: a tool for the analysis of relay-based railway interlocking systems. In: Fisman D, Rosu G (eds) tools and algorithms for the construction and analysis of systems - 28th international conference, TACAS 2022, held as Part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, Proceedings, Part I, Lecture Notes in Computer Science, vol 13243. Springer, pp 125\u2013142, 2\u20137 April. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-030-99524-9_7","DOI":"10.1007\/978-3-030-99524-9_7"},{"key":"461_CR4","doi-asserted-by":"crossref","unstructured":"Barrett CW, Sebastiani R, Seshia SA, et\u00a0al. (2009) Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol 185. IOS Press, pp 825\u2013885","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"461_CR5","doi-asserted-by":"crossref","unstructured":"Basagiannis S, Battista L, Becchi A, et\u00a0al. (2023) Smt-based stability verification of an industrial switched pi control systems. In: 1st International Workshop on Verification & Validation of Dependable Cyber-Physical Systems","DOI":"10.1109\/DSN-W58399.2023.00063"},{"key":"461_CR6","doi-asserted-by":"publisher","unstructured":"Becchi A, Cimatti A (2022) Abstraction modulo stability for reverse engineering. In: Shoham S, Vizel Y (eds) Computer aided verification - 34th international conference, CAV 2022, Haifa, Israel, Proceedings, Part I, Lecture Notes in Computer Science, vol 13371. Springer, pp 469\u201348, 7\u201310 August. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-13185-1_23","DOI":"10.1007\/978-3-031-13185-1_23"},{"issue":"104","key":"461_CR7","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.ic.2020.104620","volume":"275","author":"A Becchi","year":"2020","unstructured":"Becchi A, Zaffanella E (2020) PPLite: zero-overhead encoding of NNC polyhedra. Inf Comput 275(104):62. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.ic.2020.104620","journal-title":"Inf Comput"},{"key":"461_CR8","doi-asserted-by":"crossref","unstructured":"Becchi A, Cimatti A, Zaffanella E (2020) Synthesis of P-stable abstractions. In: SEFM, Lecture Notes in Computer Science, vol 12310. Springer, pp 214\u2013230","DOI":"10.1007\/978-3-030-58768-0_12"},{"key":"461_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-023-01145-x","author":"A Becchi","year":"2024","unstructured":"Becchi A, Cimatti A, Zaffanella E (2024) P-stable abstractions of hybrid systems. Softw Syst Mod. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/s10270-023-01145-x","journal-title":"Softw Syst Mod"},{"key":"461_CR10","doi-asserted-by":"crossref","unstructured":"ter Beek MH, Bor\u00e4lv A, Fantechi A, et\u00a0al. (2019) Adopting formal methods in an industrial setting: the railways case. In: FM, Lecture Notes in Computer Science, vol 11800. Springer, pp 762\u2013772","DOI":"10.1007\/978-3-030-30942-8_46"},{"key":"461_CR11","doi-asserted-by":"publisher","unstructured":"Biere A, Cimatti A, Clarke EM, et\u00a0al. (1999) Symbolic model checking without bdds. In: Cleaveland R (ed) tools and algorithms for construction and analysis of systems, 5th international conference, TACAS \u201999, held as part of the European joint conferences on the theory and practice of software, ETAPS\u201999, Amsterdam, March 22-28, 1999, Proceedings, Lecture Notes in Computer Science, vol 1579. Springer, pp 193\u2013200. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"461_CR12","doi-asserted-by":"publisher","unstructured":"Cavada R, Cimatti A, Mover S, et\u00a0al. (2018) Analysis of relay interlocking systems via smt-based model checking of switched multi-domain kirchhoff networks. In: Bj\u00f8rner NS, Gurfinkel A (eds) 2018 formal methods in computer aided design, FMCAD 2018, Austin, TX, October 30 - November 2, 2018. IEEE, p 1. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.23919\/FMCAD.2018.8603007","DOI":"10.23919\/FMCAD.2018.8603007"},{"key":"461_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Mover S, et\u00a0al. (2013) Parameter synthesis with IC3. In: Formal methods in computer-aided design, FMCAD 2013, Portland, OR, October 20-23, 2013. IEEE, pp 165\u2013168. https:\/\/2.zoppoz.workers.dev:443\/https\/ieeexplore.ieee.org\/document\/6679406\/","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"461_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma B, et\u00a0al. (2013) The MathSAT5 SMT Solver. In: Piterman N, Smolka S (eds) Proceedings of TACAS, LNCS, vol 7795. Springer","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"461_CR15","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A, Mover S, et\u00a0al. (2014) Verifying LTL properties of hybrid systems with k-liveness. In: Biere A, Bloem R (eds) computer aided verification - 26th international conference, CAV 2014, held as part of the vienna summer of logic, VSL 2014, Vienna, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol 8559. Springer, pp 424\u201344https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-08867-9_28","DOI":"10.1007\/978-3-319-08867-9_28"},{"key":"461_CR16","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Magnago E, et\u00a0al. (2019) Extending nuxmv with timed transition systems and timed temporal properties. In: CAV (1), lecture notes in computer science, vol 11561. Springer, pp 376\u2013386","DOI":"10.1007\/978-3-030-25540-4_21"},{"key":"461_CR17","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.ic.2019.104502","volume":"272","author":"A Cimatti","year":"2020","unstructured":"Cimatti A, Griggio A, Magnago E et al (2020) SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Inf Comput 272:104\u201350. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.ic.2019.104502","journal-title":"Inf Comput"},{"issue":"1\u20133","key":"461_CR18","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst MD, Perkins JH, Guo PJ et al (2007) The daikon system for dynamic detection of likely invariants. Sci Comput Program 69(1\u20133):35\u201345","journal-title":"Sci Comput Program"},{"key":"461_CR19","unstructured":"Gario M, Micheli A, Kessler FB (2015) Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms"},{"key":"461_CR20","doi-asserted-by":"crossref","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: CAV, lecture notes in computer science, vol 1254. Springer, pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"461_CR21","doi-asserted-by":"crossref","unstructured":"Haxthausen AE, Kj\u00e6r AA, Bliguet ML (2011) Formal development of a tool for automated modelling and verification of relay interlocking systems. In: FM, lecture notes in computer science, vol 6664. Springer, pp 118\u2013132","DOI":"10.1007\/978-3-642-21437-0_11"},{"key":"461_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"LV Hong","year":"2017","unstructured":"Hong LV, Haxthausen AE, Peleska J (2017) Formal modelling and verification of interlocking systems featuring sequential release. Sci Comput Program 133:91\u2013115","journal-title":"Sci Comput Program"},{"issue":"4","key":"461_CR23","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1109\/9.664157","volume":"43","author":"M Johansson","year":"1998","unstructured":"Johansson M, Rantzer A (1998) Computation of piecewise quadratic lyapunov functions for hybrid systems. IEEE Trans Autom Control 43(4):555\u201355. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/9.664157","journal-title":"IEEE Trans Autom Control"},{"key":"461_CR24","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Bryant RE, Cook B (2003) A symbolic approach to predicate abstraction. In: CAV, lecture notes in computer science, vol 2725. Springer, pp 141\u2013153","DOI":"10.1007\/978-3-540-45069-6_15"},{"key":"461_CR25","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Nieuwenhuis R, Oliveras A (2006) SMT techniques for fast predicate abstraction. In: CAV, lecture notes in computer science, vol 4144. Springer, pp 424\u2013437","DOI":"10.1007\/11817963_39"},{"issue":"1\u20132","key":"461_CR26","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1006\/inco.1999.2817","volume":"156","author":"F Laroussinie","year":"2000","unstructured":"Laroussinie F, Schnoebelen P (2000) Specification in ctl+past for verification in CTL. Inf Comput 156(1\u20132):236\u201326. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1006\/inco.1999.2817","journal-title":"Inf Comput"},{"key":"461_CR27","unstructured":"Limbr\u00e9e C (2019) Formal verification of railway interlocking systems. In: PhD thesis, Catholic University of Louvain, Louvain-la-Neuve, Belgium"},{"key":"461_CR28","doi-asserted-by":"crossref","unstructured":"Limbr\u00e9e C, Cappart Q, Pecheur C, et\u00a0al. (2016) Verification of railway interlocking - compositional approach with OCRA. In: RSSRail, lecture notes in computer science, vol 9707. Springer, pp 134\u2013149","DOI":"10.1007\/978-3-319-33951-1_10"},{"issue":"2","key":"461_CR29","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1109\/TAC.2008.2012009","volume":"54","author":"H Lin","year":"2009","unstructured":"Lin H, Antsaklis PJ (2009) Stability and stabilizability of switched linear systems: a survey of recent results. IEEE Trans Autom Control 54(2):308\u201332. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/TAC.2008.2012009","journal-title":"IEEE Trans Autom Control"},{"key":"461_CR30","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner R (1983) Calculi for synchrony and asynchrony. Theor Comput Sci 25:267\u201331. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/0304-3975(83)90114-7","journal-title":"Theor Comput Sci"},{"key":"461_CR31","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, providence, Rhode Island, 31 October - 1 November 1977. IEEE Computer Society, pp 46\u20135https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"461_CR32","unstructured":"Somenzi F (1998) Cudd: Cu decision diagram package release"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00461-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/article\/10.1007\/s10703-024-00461-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00461-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T22:31:40Z","timestamp":1757111500000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/10.1007\/s10703-024-00461-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,12]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["461"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/s10703-024-00461-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,12]]},"assertion":[{"value":"25 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 July 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 September 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}