{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T15:55:22Z","timestamp":1773330922436,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642032394","type":"print"},{"value":"9783642032400","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03240-0_15","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T10:27:38Z","timestamp":1248690458000},"page":"166-181","source":"Crossref","is-referenced-by-count":12,"title":["From Informal Requirements to Property-Driven Formal Validation"],"prefix":"10.1007","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","reference":[{"key":"15_CR1","unstructured":"UML Version 2.1.2., \n                    \n                      http:\/\/www.omg.org\/spec\/UML\/2.1.2\/"},{"key":"15_CR2","volume-title":"The Vienna Development Method: The Meta-Language","year":"1978","unstructured":"Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language, vol.\u00a061. Springer, Heidelberg (1978)"},{"key":"15_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. C.U. Press, Cambridge (1996)"},{"key":"15_CR4","volume-title":"Compilers - Principles, techniques and tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers - Principles, techniques and tools. Addison-Wesley, Reading (1986)"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10515-006-5468-2","volume":"13","author":"V. Ambriola","year":"2006","unstructured":"Ambriola, V., Gervasi, V.: On the Systematic Analysis of Natural Language Requirements with CIRCE. Autom. Softw. Eng.\u00a013(1), 107\u2013167 (2006)","journal-title":"Autom. Softw. Eng."},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/11875567_10","volume-title":"Computer Safety, Reliability, and Security","author":"R. Banach","year":"2006","unstructured":"Banach, R., Bozzano, M.: Retrenchment, and the generation of fault trees for static, dynamic and cyclic systems. In: G\u00f3rski, J. (ed.) SAFECOMP 2006. LNCS, vol.\u00a04166, pp. 127\u2013141. Springer, Heidelberg (2006)"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods in System Design\u00a018(2), 141\u2013163 (2001)","journal-title":"Formal Methods in System Design"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74128-2_1","volume-title":"Model Checking and Artificial Intelligence","author":"P. Bertoli","year":"2007","unstructured":"Bertoli, P., Bozzano, M., Cimatti, A.: Symbolic model checking framework for safety analysis, diagnosis, and synthesis. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS, vol.\u00a04428, pp. 1\u201318. Springer, Heidelberg (2007)"},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10009-006-0001-2","volume":"9","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Villafiorita, A.: The FSAP\/NuSMV-SA Safety Analysis Platform. STTT\u00a09(1), 5\u201324 (2007)","journal-title":"STTT"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Carrington, D.A., Duke, D.J., Duke, R., King, P., Rose, G.A., Smith, G.: Object-Z: An Object-Oriented Extension to Z. In: FORTE 1989, Amsterdam (NL), pp. 281\u2013296 (1990)","DOI":"10.2307\/1372615"},{"key":"15_CR12","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 (2007)","DOI":"10.1109\/FAMCAD.2007.35"},{"key":"15_CR13","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proc. 1962 Int. Congr. Math., Upsala, pp. 23\u201325 (1963)"},{"issue":"4","key":"15_CR14","doi-asserted-by":"publisher","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\u00a02(4), 410\u2013425 (2000)","journal-title":"STTT"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Cimatti","year":"2008","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 52\u201367. Springer, Heidelberg (2008)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-540-73368-3_53","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean Abstraction for Temporal Logic Satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 532\u2013546. Springer, Heidelberg (2007)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Object models with temporal constraints. In: SEFM (2008) (to appear)","DOI":"10.1109\/SEFM.2008.23"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-540-71209-1_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Roveri, M., Tonetta, S.: Syntactic Optimizations for PSL Verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 505\u2013518. Springer, Heidelberg (2007)"},{"key":"15_CR19","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"15_CR20","first-page":"612","volume-title":"ICSE 1997","author":"R. Darimont","year":"1997","unstructured":"Darimont, R., Delor, E., Massonet, P., van Lamsweerde, A.: GRAIL\/KAOS: an environment for goal-driven requirements engineering. In: ICSE 1997, pp. 612\u2013613. ACM, New York (1997)"},{"key":"15_CR21","volume-title":"A Practical Introduction to PSL","author":"C. Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)"},{"issue":"3","key":"15_CR22","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BF01384048","volume":"4","author":"A. Fantechi","year":"1994","unstructured":"Fantechi, A., Gnesi, S., Ristori, G., Carenini, M., Vanocchi, M., Moreschini, P.: Assisting Requirement Formalization by Means of Natural Language Translation. Formal Methods in System Design\u00a04(3), 243\u2013263 (1994)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"15_CR23","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/s00766-004-0191-7","volume":"9","author":"A. Fuxman","year":"2004","unstructured":"Fuxman, A., Liu, L., Mylopoulos, J., Pistore, M., Roveri, M., Traverso, P.: Specifying and analyzing early requirements in Tropos. Requirements Engineering\u00a09(2), 132\u2013150 (2004)","journal-title":"Requirements Engineering"},{"issue":"3","key":"15_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C.L. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Trans. Softw. Eng. Methodol.\u00a05(3), 231\u2013261 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Nelken, R., Francez, N.: Automatic Translation of Natural Language System Specifications. In: CAV, pp. 360\u2013371 (1996)","DOI":"10.1007\/3-540-61474-5_83"},{"key":"15_CR26","unstructured":"OMG. Object Constraint Language: OMG available specification Version 2.0 (2006)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC 2006, pp. 821\u2013826 (2006)","DOI":"10.1109\/DAC.2006.229231"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symp. on Foundation of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th Annual ACM Symposium on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Schwitter, R.: Dynamic Semantics for a Controlled Natural Language. In: DEXA Workshops, pp. 43\u201347 (2004)","DOI":"10.1109\/DEXA.2004.1333447"},{"key":"15_CR31","volume-title":"The Z Notation: a reference manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: a reference manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)","edition":"2"},{"issue":"4","key":"15_CR32","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\u00a029(4), 401\u2013408 (2005)","journal-title":"Informatica"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03240-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:26:08Z","timestamp":1558268768000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03240-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032394","9783642032400"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03240-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}