{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:10Z","timestamp":1773827470696,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T00:00:00Z","timestamp":1250640000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2011,5]]},"DOI":"10.1007\/s10270-009-0130-7","type":"journal-article","created":{"date-parts":[[2009,8,18]],"date-time":"2009-08-18T08:53:54Z","timestamp":1250585634000},"page":"147-160","source":"Crossref","is-referenced-by-count":21,"title":["Formalizing requirements with object models and temporal constraints"],"prefix":"10.1007","volume":"10","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"Angelo","family":"Susi","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,8,19]]},"reference":[{"key":"130_CR1","unstructured":"IEEE Standard for Property Specification Language (PSL). IEEE Std 1850\u20132005 (2005)"},{"key":"130_CR2","unstructured":"IEEE Standard for System Verilog\u2014Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800\u20132005 (2005)"},{"key":"130_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"3","key":"130_CR4","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/B:AGNT.0000018806.20944.ef","volume":"8","author":"P. Bresciani","year":"2004","unstructured":"Bresciani P., Giorgini P., Giunchiglia F., Mylopoulos J., Perini A.: Tropos: an agent-oriented software development methodology. Autonom. Agents Multi-Agent Syst. 8(3), 203\u2013236 (2004)","journal-title":"Autonom. Agents Multi-Agent Syst."},{"key":"130_CR5","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: CAV, pp. 299\u2013303 (2008)","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"130_CR6","doi-asserted-by":"crossref","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: CHARME, pp. 191\u2013206 (2005)","DOI":"10.1007\/11560548_16"},{"key":"130_CR7","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Franz\u00e9n, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD, pp. 69\u201376. IEEE, New York (2007)","DOI":"10.1109\/FAMCAD.2007.35"},{"issue":"4","key":"130_CR8","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti A., Clarke E.M., Giunchiglia F., Roveri M.: NuSMV: a new symbolic model checker. STTT 2(4), 410\u2013425 (2000)","journal-title":"STTT"},{"key":"130_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: TACAS, pp. 397\u2013412 (2008)","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"130_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: CAV, vol. 4590 of LNCS, pp 532\u2013546. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73368-3_53"},{"key":"130_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: From informal requirements to property-driven formal validation. In: FMICS, LNCS, L\u2019Aquila, Italy. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-642-03240-0_15"},{"key":"130_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Object models with temporal constraints. In: SEFM, pp. 249\u2013258. IEEE Computer Society, New York (2008)","DOI":"10.1109\/SEFM.2008.23"},{"issue":"10","key":"130_CR13","doi-asserted-by":"crossref","first-page":"1737","DOI":"10.1109\/TCAD.2008.2003303","volume":"27","author":"A. Cimatti","year":"2008","unstructured":"Cimatti A., Roveri M., Tonetta S.: PSL symbolic compilation. IEEE Trans. CAD Integr. Circ. Syst. 27(10), 1737\u20131750 (2008)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"130_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"130_CR15","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999). ISBN 0-262-03270-7"},{"key":"130_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Gupta, A., Kukula, J.H., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: CAV, pp. 265\u2013279 (2002)","DOI":"10.1007\/3-540-45657-0_20"},{"issue":"2\u20133","key":"130_CR17","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E.M. Clarke","year":"2004","unstructured":"Clarke E.M., Kroening D., Sharygina N., Yorav K.: Predicate abstraction of ANSI-C programs using SAT. Formal Meth. Syst. Des 25(2\u20133), 105\u2013127 (2004)","journal-title":"Formal Meth. Syst. Des"},{"issue":"1","key":"130_CR18","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.ic.2006.08.003","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri S., Lazic R., Nowak D.: On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput. 205(1), 2\u201324 (2007)","journal-title":"Inf. Comput."},{"key":"130_CR19","unstructured":"European train control system. http:\/\/www.era.europa.eu\/core\/ertms\/Pages\/FirstETCSSRS300.aspx"},{"key":"130_CR20","unstructured":"System Requirements Specification\u2014ETCS Subset 026 v230 (2006)"},{"key":"130_CR21","unstructured":"Formal Verification of ETCS specifications: EuRailCheck. http:\/\/www.era.europa.eu\/core\/ertms\/Pages\/Feasibility_Study.aspx , and http:\/\/es.fbk.eu\/events\/formal-etcs"},{"issue":"2","key":"130_CR22","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/s00766-004-0191-7","volume":"9","author":"A. Fuxman","year":"2004","unstructured":"Fuxman A., Liu L., Mylopoulos J., Roveri M., Traverso P.: Specifying and analyzing early requirements in tropos. Req. Eng. 9(2), 132\u2013150 (2004)","journal-title":"Req. Eng."},{"key":"130_CR23","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. In: CADE, pp. 362\u2013378 (2007)","DOI":"10.1007\/978-3-540-73595-3_25"},{"issue":"1\u20133","key":"130_CR24","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I.M. Hodkinson","year":"2000","unstructured":"Hodkinson I.M., Wolter F., Zakharyaschev M.: Decidable fragment of first-order temporal logics. Ann. Pure Appl. Logic 106(1\u20133), 85\u2013134 (2000)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"130_CR25","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"130_CR26","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: CAV, LNCS, pp. 424\u2013437. Springer, Heidelberg (2006)","DOI":"10.1007\/11817963_39"},{"key":"130_CR27","doi-asserted-by":"crossref","unstructured":"Lange, M.: Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness. In: CONCUR, pp. 90\u2013104 (2007)","DOI":"10.1007\/978-3-540-74407-8_7"},{"key":"130_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems, Specification","author":"Z. Manna","year":"1992","unstructured":"Manna Z., Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, Heidelberg (1992)"},{"key":"130_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna Z., Pnueli A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"130_CR30","unstructured":"OMG Object Constraint Language: OMG available specification Version 2.0 (2006)"},{"key":"130_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"130_CR32","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.Y.: Property-Driven Partitioning for Abstraction Refinement. In: TACAS, pp. 389\u2013404 (2007)","DOI":"10.1007\/978-3-540-71209-1_30"},{"key":"130_CR33","volume-title":"The Z Notation: a reference manual. 2nd edn","author":"J.M. Spivey","year":"1992","unstructured":"Spivey J.M.: The Z Notation: a reference manual. 2nd edn. Prentice-Hall, Englewood Cliffs (1992)"},{"issue":"4","key":"130_CR34","first-page":"401","volume":"29","author":"A. Susi","year":"2005","unstructured":"Susi A., Perini A., Giorgini P., Mylopoulos J.: The tropos metamodel and its use. Informatica 29(4), 401\u2013408 (2005)","journal-title":"Informatica"},{"key":"130_CR35","unstructured":"UML Version 2.1.2. http:\/\/www.omg.org\/spec\/UML\/2.1.2\/"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-009-0130-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-009-0130-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-009-0130-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:55:26Z","timestamp":1559116526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-009-0130-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8,19]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,5]]}},"alternative-id":["130"],"URL":"https:\/\/doi.org\/10.1007\/s10270-009-0130-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8,19]]}}}