{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T13:10:28Z","timestamp":1740316228945,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_17","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"234-251","source":"Crossref","is-referenced-by-count":9,"title":["Translation from Adapted UML to Promela for CORBA-Based Applications"],"prefix":"10.1007","author":[{"given":"J.","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Cui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Cui, H.: Correctness of distributed systems with middleware. Master\u2019s Thesis. School of Computer Science, University of Windsor (April 2003)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Duval, G.: Specification and verification of an object request broker. In: Proc. of the 20th International Conference on Software Engineering, pp. 43\u201352 (1998)","DOI":"10.1109\/ICSE.1998.671101"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-44829-2_11","volume-title":"Model Checking Software","author":"D. Garlan","year":"2003","unstructured":"Garlan, D., Khersonsky, S., Kim, J.: Model checking publish-subscribe systems. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 166\u2013180. Springer, Heidelberg (2003)"},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1109\/ICSE.2003.1201197","volume-title":"Proc. of the 25th International Conference on Software Engineering","author":"J. Hatcliff","year":"2003","unstructured":"Hatcliff, J., Deng, X., Dwyer, M., Jung, G., Ranganath, V.P.: An integrated development, analysis, and verification environment for component-based systems. In: Proc. of the 25th International Conference on Software Engineering, pp. 160\u2013173. IEEE, Los Alamitos (2003)"},{"issue":"4","key":"17_CR5","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"17_CR6","volume-title":"The Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.: The Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5) (May 1997)","DOI":"10.1109\/32.588521"},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"M. Kamel","year":"2000","unstructured":"Kamel, M., Leue, S.: Formalization and validation of the general inter-ORB protocol (GIOP) using Promela and Spin. Software Tools for Technology Transfer\u00a02(4), 394\u2013409 (2000)","journal-title":"Software Tools for Technology Transfer"},{"key":"17_CR9","first-page":"44","volume-title":"Proc. of the Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9)","author":"N. Kaveh","year":"2001","unstructured":"Kaveh, N., Emmerich, W.: Deadlock detection in distributed object systems. In: Proc. of the Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9), pp. 44\u201351. ACM Press, New York (2001)"},{"key":"17_CR10","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, 637\u2013664 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-46852-8_31","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"J. Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.: Formalizing UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol.\u00a01723, pp. 430\u2013445. Springer, Heidelberg (1999)"},{"key":"17_CR12","volume-title":"Concurrency: Models and Programs \u2013 From Finite State Models to Java Programs","author":"J. Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: Models and Programs \u2013 From Finite State Models to Java Programs. John Wiley, Chichester (1999)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.: Implementing statecharts in PROMELA\/SPIN. In: Proc. of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 90\u2013101 (1998)","DOI":"10.1109\/WIFT.1998.766303"},{"key":"17_CR14","first-page":"1","volume":"47","author":"T. Schafer","year":"2001","unstructured":"Schafer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science\u00a047, 1\u201313 (2001)","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T12:30:19Z","timestamp":1740313819000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}