{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:04:39Z","timestamp":1743123879278,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214092"},{"type":"electronic","value":"9783319214108"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21410-8_47","type":"book-chapter","created":{"date-parts":[[2015,6,18]],"date-time":"2015-06-18T15:57:14Z","timestamp":1434643034000},"page":"612-627","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards a Wide Acceptance of Formal Methods to the Design of Safety Critical Software: an Approach Based on UML and Model Checking"],"prefix":"10.1007","author":[{"given":"Eduardo Rohde","family":"Eras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luciana Brasil Rebelo","family":"dos Santos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valdivino Alexandre","family":"de Santiago J\u00fanior","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nandamudi Lankalapalli","family":"Vijaykumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,19]]},"reference":[{"key":"47_CR1","unstructured":"Nusmv home page (2011)"},{"key":"47_CR2","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. The MIT Press, Cambridge (2008). p. 975"},{"key":"47_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-25271-6_14","volume-title":"Formal Methods for Components and Objects","author":"L Baresi","year":"2011","unstructured":"Baresi, L., Morzenti, A., Motta, A., Rossi, M.: Towards the UML-based formal verification of timed systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 267\u2013286. Springer, Heidelberg (2011)"},{"issue":"4","key":"47_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.10.024","volume":"127","author":"ME Beato","year":"2005","unstructured":"Beato, M.E., Barrio-Sol\u00f3rzano, M., Cuesta, C.E., de la Fuente, P.: Uml automatic verification tool with formal methods. Electronic Notes in Theoretical Computer Science 127(4), 3\u201316 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"47_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-69850-0_12","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196\u2013215. Springer, Heidelberg (2008)"},{"key":"47_CR6","volume-title":"Writing Effective Use Cases","author":"A Cockburn","year":"2000","unstructured":"Cockburn, A.: Writing Effective Use Cases, 1st edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2000)","edition":"1"},{"issue":"1","key":"47_CR7","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0167-6423(02)00033-3","volume":"44","author":"V Cortellessa","year":"2002","unstructured":"Cortellessa, V., Mirandola, R.: Prima-uml: a performance validation incremental methodology on early uml diagrams. Science of Computer Programming 44(1), 101\u2013129 (2002)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"47_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s11219-011-9155-6","volume":"20","author":"VA de Santiago Jr","year":"2012","unstructured":"de Santiago Jr, V.A., Vijaykumar, N.L.: Vijaykumar. Generating model-based test cases from natural language requirements for space application software. Software Quality Journal 20(1), 77\u2013143 (2012)","journal-title":"Software Quality Journal"},{"key":"47_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/978-3-319-09144-0_48","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2014","author":"LBR dos Santos","year":"2014","unstructured":"dos Santos, L.B.R., Eras, E.R., de Santiago Jr, V.A., Vijaykumar, N.L.: A formal verification tool for UML behavioral diagrams. In: Murgante, B., Misra, S., Rocha, A.M.A.C., Torre, C., Rocha, J.G., Falc\u00e3o, M.I., Taniar, D., Apduhan, B.O., Gervasi, O. (eds.) ICCSA 2014, Part I. LNCS, vol. 8579, pp. 696\u2013711. Springer, Heidelberg (2014)"},{"key":"47_CR10","doi-asserted-by":"crossref","unstructured":"Dubrovin, J., Junttila, T.: Symbolic model checking of hierarchical uml state machines. In: 8th International Conference on Application of Concurrency to System Design, ACSD 2008, pp. 108\u2013117. IEEE (2008)","DOI":"10.1109\/ACSD.2008.4574602"},{"key":"47_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering, 1999, pp. 411\u2013420. IEEE (1999)","DOI":"10.1145\/302405.302672"},{"key":"47_CR12","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/MS.2008.107","volume":"25","author":"KE Emam","year":"2008","unstructured":"Emam, K.E., Koru, A.G.: A replicated survey of it software project failures. IEEE Software 25, 84\u201390 (2008)","journal-title":"IEEE Software"},{"issue":"7","key":"47_CR13","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1109\/TSE.2004.33","volume":"30","author":"R Eshuis","year":"2004","unstructured":"Eshuis, R., Wieringa, R.: Tool support for verifying uml activity diagrams. IEEE Transactions on Software Engineering 30(7), 437\u2013447 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"47_CR14","unstructured":"Kannenberg, A., Saiedian, H.: Why software requirements traceability remains a challenge. The Journal of Defense Software Engineering, 14\u201318 (2009)"},{"issue":"1","key":"47_CR15","first-page":"43","volume":"14","author":"VSW Lam","year":"2007","unstructured":"Lam, V.S.W.: A formalism for reasoning about uml activity diagrams. Nordic Journal of Computing 14(1), 43\u201364 (2007)","journal-title":"Nordic Journal of Computing"},{"issue":"6","key":"47_CR16","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of uml statechart diagrams using the spin model-checker. Formal Aspects of Computing 11(6), 637\u2013664 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"47_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.entcs.2009.09.064","volume":"254","author":"V Lima","year":"2009","unstructured":"Lima, V., Talhi, C., Mouheb, D., Debbabi, M., Wang, L., Pourzandi, M.: Formal verification and validation of uml 2.0 sequence diagrams using source and destination of messages. Electronic Notes in Theoretical Computer Science 254, 143\u2013160 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"47_CR18","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/TSE.2009.50","volume":"36","author":"N Moha","year":"2010","unstructured":"Moha, N., Gu\u00e9h\u00e9neuc, Y.-G., Duchien, L., Le Meur, A.-F.: DECOR: A method for the specification and detection of code and design smells. IEEE Trans. Software Eng. 36(1), 20\u201336 (2010)","journal-title":"IEEE Trans. Software Eng."},{"key":"47_CR19","unstructured":"The Object Management Group (OMG), Needham, MA, USA. OMG Unified Modeling Language (OMG UML), Superstructure, V2.1.2 (2007)"},{"key":"47_CR20","doi-asserted-by":"crossref","unstructured":"Palomba, F., Bavota, G., Di Penta, M., Oliveto, R., De Lucia, A.: Do they really smell bad? a study on developers\u2019 perception of bad code smells. In: 30th IEEE International Conference on Software Maintenance and Evolution, Victoria, BC, Canada, September 29 - October 3, 2014, pp. 101\u2013110. IEEE (2014)","DOI":"10.1109\/ICSME.2014.32"},{"issue":"2","key":"47_CR21","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1109\/TSE.1986.6312940","volume":"12","author":"DL Parnas","year":"1986","unstructured":"Parnas, D.L., Clements, P.C.: A rational design process: How and why to fake it. IEEE Trans. Software Eng. 12(2), 251\u2013257 (1986)","journal-title":"IEEE Trans. Software Eng."},{"key":"47_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-69850-0_13","volume-title":"25 Years of Model Checking","author":"JP Queille","year":"2008","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of conurrent systems in CESAR. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 216\u2013230. Springer, Heidelberg (2008)"},{"key":"47_CR23","unstructured":"dos Santos, L.B.R., de Santiago, Jr., V.A., Vijaykumar, N.L.: Transformation of uml behavioral diagrams to support software model checking (2014). arXiv preprint arXiv:1404.0855"},{"key":"47_CR24","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-10619-4_9","volume-title":"Advances in Software Engineering","author":"B Solemon","year":"2009","unstructured":"Solemon, B., Sahibuddin, S., Ghani, A.A.A.: Requirements engineering problems and practices in software companies: an industrial survey. In: \u015alezak, D., Kim, T., Kiumi, A., Jiang, T., Verner, J., Abrah\u00e3o, S. (eds.) ASEA 2009. CCIS, vol. 59, pp. 70\u201377. Springer, Heidelberg (2009)"},{"issue":"3","key":"47_CR25","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1109\/TSE.2009.1","volume":"35","author":"N Tsantalis","year":"2009","unstructured":"Tsantalis, N., Chatzigeorgiou, A.: Identification of move method refactoring opportunities. IEEE Trans. Software Eng. 35(3), 347\u2013367 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"47_CR26","unstructured":"UBM Tech. 2013 embedded market study. DESIGN West 2013 Conference (2013)"},{"key":"47_CR27","unstructured":"Uchitel, S., Kramer, J.: A workbench for synthesising behaviour models from scenarios. In: Proceedings of the 23rd International Conference on Software Engineering, pp. 188\u2013197. IEEE Computer Society (2001)"},{"key":"47_CR28","doi-asserted-by":"crossref","unstructured":"van Lamsweerde, A.: Requirements engineering in the year 00: a research perspective. In: Proceedings of International Conference on Software Engineering (ICSE), pp. 5\u201319. ACM, New York (2000)","DOI":"10.1145\/337180.337184"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications -- ICCSA 2015"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21410-8_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:36:54Z","timestamp":1676947014000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21410-8_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214092","9783319214108"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21410-8_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}