{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T17:40:06Z","timestamp":1746294006682,"version":"3.40.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319091433"},{"type":"electronic","value":"9783319091440"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09144-0_48","type":"book-chapter","created":{"date-parts":[[2014,7,3]],"date-time":"2014-07-03T02:47:10Z","timestamp":1404355630000},"page":"696-711","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Verification Tool for UML Behavioral Diagrams"],"prefix":"10.1007","author":[{"given":"Luciana Brasil Rebelo","family":"dos Santos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eduardo Rohde","family":"Eras","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","reference":[{"key":"48_CR1","first-page":"975","volume-title":"Principles of model checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking, p. 975. The MIT Press, Cambridge (2008)"},{"issue":"3","key":"48_CR2","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1016\/S1571-0661(04)00262-2","volume":"55","author":"T. Sch\u00e4fer","year":"2001","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model checking uml state machines and collaborations. Electronic Notes in Theoretical Computer Science\u00a055(3), 357\u2013369 (2001)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"48_CR3","unstructured":"OMG, T.O.M.G.: Omg - unified modeling language (omg uml) (1997)"},{"key":"48_CR4","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-15228-3","volume-title":"Verification and Validation in Systems Engineering","author":"M. Debbabi","year":"2010","unstructured":"Debbabi, M., Hassa\u00efne, F., Jarraya, Y., Soeanu, A., Alawneh, L.: Verification and Validation in Systems Engineering, p. 270. Springer, Heidelberg (2010)"},{"issue":"7","key":"48_CR5","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\u00a030(7), 437\u2013447 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"48_CR6","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1016\/j.infsof.2008.05.002","volume":"51","author":"M. Sarma","year":"2009","unstructured":"Sarma, M., Mall, R.: Automatic generation of test specifications for coverage of system state transitions. Information and Software Technology\u00a051(2), 418\u2013432 (2009)","journal-title":"Information and Software Technology"},{"key":"48_CR7","volume-title":"Software Engineering: A Practitioner\u2019s Approach","author":"R.S. Pressman","year":"2010","unstructured":"Pressman, R.S.: Software Engineering: A Practitioner\u2019s Approach, 7th edn. McGrawHill, New York (2010)","edition":"7"},{"key":"48_CR8","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/302405.302672","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE)","author":"M.B. Dwyer","year":"1999","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the International Conference on Software Engineering (ICSE), pp. 411\u2013420. ACM Press, New York (1999)"},{"key":"48_CR9","first-page":"304","volume-title":"Writing Effective Use Cases","author":"A. Cockburn","year":"2000","unstructured":"Cockburn, A.: Writing Effective Use Cases, p. 304. Addison-Wesley Professional, US (2000)"},{"key":"48_CR10","unstructured":"Kessler, F.B.: Nusmv home page (2011)"},{"key":"48_CR11","unstructured":"eclipse.org: Papyrus (2014)"},{"key":"48_CR12","unstructured":"Holzmann, G.: The SPIN model checker: Primer and reference manual, vol.\u00a01003. Addison-Wesley (2004)"},{"key":"48_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"48_CR14","unstructured":"eclipse.org: Eclipse (2014)"},{"key":"48_CR15","unstructured":"Santiago, V., Mattiello-Francisco, M., Costa, R., Silva, W., Ambrosio, A.: Qsee project: an experience in outsourcing software development for space applications. In: The 19th International Conference on Software Engineering & Knowledge Engineering (SEKE), pp. 51\u201356 (2007)"},{"key":"48_CR16","doi-asserted-by":"crossref","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.: Implementing statecharts in promela\/spin. In: Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 90\u2013101. IEEE (1998)","DOI":"10.1109\/WIFT.1998.766303"},{"issue":"6","key":"48_CR17","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\u00a011(6), 637\u2013664 (1999)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"48_CR18","first-page":"43","volume":"14","author":"V. Lam","year":"2007","unstructured":"Lam, V.: A formalism for reasoning about uml activity diagrams. Nordic Journal of Computing\u00a014(1), 43\u201364 (2007)","journal-title":"Nordic Journal of Computing"},{"key":"48_CR19","doi-asserted-by":"crossref","unstructured":"Dubrovin, J., Junttila, T.: Symbolic model checking of hierarchical uml state machines. In: ACSD 2008. 8th International Conference on Application of Concurrency to System Design, pp. 108\u2013117. IEEE (2008)","DOI":"10.1109\/ACSD.2008.4574602"},{"key":"48_CR20","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Kramer, J.: A workbench for synthesising behaviour models from scenarios. In: Proceedings of the 23rd Intern. Conference on Software Engineering, pp. 188\u2013197. IEEE Computer Society (2001)","DOI":"10.1109\/ICSE.2001.919093"},{"key":"48_CR21","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.\u00a06957, pp. 267\u2013286. Springer, Heidelberg (2011)"},{"issue":"1","key":"48_CR22","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\u00a044(1), 101\u2013129 (2002)","journal-title":"Science of Computer Programming"},{"key":"48_CR23","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Computing Surveys\u00a041(4), 19:1\u201319:36 (2009)","DOI":"10.1145\/1592434.1592436"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09144-0_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T17:09:22Z","timestamp":1746292162000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09144-0_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319091433","9783319091440"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09144-0_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}