{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T08:12:56Z","timestamp":1758960776644},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,3,12]],"date-time":"2011-03-12T00:00:00Z","timestamp":1299888000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s11334-011-0147-2","type":"journal-article","created":{"date-parts":[[2011,3,11]],"date-time":"2011-03-11T08:29:08Z","timestamp":1299832148000},"page":"97-107","source":"Crossref","is-referenced-by-count":9,"title":["A model advisor for NuSMV specifications"],"prefix":"10.1007","volume":"7","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,3,12]]},"reference":[{"key":"147_CR1","unstructured":"The NuSMV website. http:\/\/nusmv.fbk.eu\/"},{"key":"147_CR2","unstructured":"The ASMETA website (2010) http:\/\/asmeta.sf.net\/"},{"key":"147_CR3","unstructured":"The nusmv-tools website (2010) http:\/\/code.google.com\/a\/eclipselabs.org\/p\/nusmv-tools\/"},{"key":"147_CR4","unstructured":"The Xtext website (2010) http:\/\/www.eclipse.org\/Xtext\/"},{"key":"147_CR5","doi-asserted-by":"crossref","unstructured":"Arcaini P, Gargantini A, Riccobene E (2010) AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier M, Gl\u00e4sser U, Khurshid S, Laleau R, Reeves S (eds) ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Heidelberg, pp 61\u201374","DOI":"10.1007\/978-3-642-11811-1_6"},{"key":"147_CR6","unstructured":"Arcaini P, Gargantini A, Riccobene E (2010) Automatic review of abstract state machines by meta property verification. In: Mu\u00f1oz C (ed) Proceedings of the second NASA formal methods symposium (NFM 2010), NASA\/CP-2010-216215. Langley Research Center, Hampton, VA, April. NASA, pp 4\u201313"},{"key":"147_CR7","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (1997) Efficient detection of vacuity in ACTL formulas. In: Proceedings of the 9th international computer aided verification conference. Lecture Notes in Computer Science, vol 1254, pp 279\u2013290","DOI":"10.1007\/3-540-63166-6_28"},{"key":"147_CR8","doi-asserted-by":"crossref","unstructured":"Bloem R, Cavada R, Pill I, Roveri M, Tchaltsev A (2007) Rat: a tool for the formal analysis of requirements. In: Damm W, Hermanns H (eds) CAV. Lecture Notes in Computer Science, vol 4590. Springer, Heidelberg, pp 263\u2013267","DOI":"10.1007\/978-3-540-73368-3_30"},{"key":"147_CR9","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E, St\u00e4rk R (2003) Abstract State Machines: a method for high-level system design and analysis. Springer, Berlin","DOI":"10.1007\/978-3-642-18216-7"},{"key":"147_CR10","unstructured":"Cavada R, Cimatti A, Jochim CA, Keighren G, Olivetti E, Pistore M, Roveri M, Tchaltsev A (2010) NuSMV 2.5 user manual. http:\/\/nusmv.fbk.eu\/"},{"key":"147_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV Version 2: an opensource tool for symbolic model checking. In: Proceedings of the international conference on computer-aided verification (CAV 2002), July. LNCS, vol 2404. Springer, Heidelberg","DOI":"10.1007\/3-540-45657-0_29"},{"key":"147_CR12","unstructured":"Gheorghiu M, Gurfinkel A (2006) Vaquot: a tool for vacuity detection. In: Posters & research tools track, FM 2006"},{"issue":"3","key":"147_CR13","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C Heitmeyer","year":"1996","unstructured":"Heitmeyer C, Jeffords R, Labaw B (1996) Automated consistency checking of requirements specifications. ACM Trans Softw Eng Methodol 5(3): 231\u2013261","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"3","key":"147_CR14","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1002\/stvr.218","volume":"11","author":"T Kim","year":"2001","unstructured":"Kim T, Cha SD (2001) Automated structural analysis of SCR-style software requirements specifications using PVS. Softw Test Verif Reliab 11(3): 143\u2013163","journal-title":"Softw Test Verif Reliab"},{"key":"147_CR15","doi-asserted-by":"crossref","unstructured":"Kupferman O (2006) Sanity checks in formal verification. In: Baier C, Hermanns H (eds) CONCUR. Lecture Notes in Computer Science, vol 4137. Springer, Heidelberg, pp 37\u201351","DOI":"10.1007\/11817949_3"},{"issue":"2","key":"147_CR16","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman O, Vardi MY (2003) Vacuity detection in temporal model checking. Int J Softw Tools Technol Transfer (STTT) 4(2): 224\u2013233","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"key":"147_CR17","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Norwell","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"147_CR18","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Proceedings of the 11th international conference on automated deduction (CADE-11). Springer, London, pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"147_CR19","doi-asserted-by":"crossref","unstructured":"Parnas DL (1994) Some theorems we should prove. In: HUG \u201993: 6th international workshop on higher order logic theorem proving and its applications. Springer, London, pp 155\u2013162","DOI":"10.1007\/3-540-57826-9_132"},{"key":"147_CR20","unstructured":"Prochnow S, Schaefer G, Bell K, von Hanxleden R (2006) Analyzing robustness of UML state machines. In: Workshop on modeling and analysis of real-time and embedded systems (MARTES 06)"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0147-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-011-0147-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0147-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,9]],"date-time":"2019-06-09T02:31:03Z","timestamp":1560047463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-011-0147-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,12]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["147"],"URL":"https:\/\/doi.org\/10.1007\/s11334-011-0147-2","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3,12]]}}}