{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:01:57Z","timestamp":1725566517452},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540233077"},{"type":"electronic","value":"9783540301875"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30187-5_24","type":"book-chapter","created":{"date-parts":[[2010,9,22]],"date-time":"2010-09-22T19:50:15Z","timestamp":1285185015000},"page":"335-349","source":"Crossref","is-referenced-by-count":9,"title":["Deductive Verification of UML Models in TLPVS"],"prefix":"10.1007","author":[{"given":"Tamarah","family":"Arons","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jozef","family":"Hooman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hillel","family":"Kugler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Zwaag","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-45739-9_22","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W. Damm","year":"2002","unstructured":"Damm, W., Jonsson, B.: Eliminating queues from RT UML model representations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 375\u2013393. Springer, Heidelberg (2002)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-39656-7_3","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: A formal semantics of concurrency and communication in Real-Time UML. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 71\u201398. Springer, Heidelberg (2003)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-39656-7_4","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"Damm, W., Westphal, B.: Live and let die: LSC-based verification of UML-models. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 99\u2013135. Springer, Heidelberg (2003)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/3-540-45923-5_15","volume-title":"Fundamental Approaches to Software Engineering","author":"A. David","year":"2002","unstructured":"David, A., Moller, O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 218. Springer, Heidelberg (2002)"},{"key":"#cr-split#-24_CR5.1","doi-asserted-by":"crossref","unstructured":"Harel, D., Gery, E.: Executable object modeling with statecharts. Computer (July 1997);","DOI":"10.1109\/2.596624"},{"key":"#cr-split#-24_CR5.2","unstructured":"Also in Proc. 18th Int. Conf. Soft. Eng., Berlin. IEEE Press, Los Alamitos (1996)"},{"issue":"9","key":"24_CR6","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1109\/TSE.2002.1033228","volume":"28","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kupferman, O.: On object systems and behavioral inheritance. IEEE Trans. Software Engineering\u00a028(9), 889\u2013903 (2002)","journal-title":"IEEE Trans. Software Engineering"},{"key":"24_CR7","unstructured":"Hooman, J., van der Zwaag, M.B.: A semantics of communicating reactive objects with timing. Technical report, EU project IST 33522 OMEGA (2004), Available at \n                    \n                      http:\/\/www-omega.imag.fr"},{"key":"24_CR8","unstructured":"Rhapsody. I-Logix, Inc., products web page, \n                    \n                      http:\/\/www.ilogix.com\/products\/"},{"key":"24_CR9","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. and Comp.\u00a0163, 203\u2013243 (2000)","journal-title":"Inf. and Comp."},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking \u2013 timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, p. 395. Springer, Heidelberg (2002)"},{"key":"24_CR11","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Semantic Foundations of Engineering Design Languages (SFEDL 2004)","author":"M. Kyas","year":"2004","unstructured":"Kyas, M., Fecher, H., de Boer, F.S., Jacob, J., van der Zwaag, M.B., Hooman, J., Arons, T., Kugler, H.: Formalizing UML models and OCL constraints in PVS. In: Semantic Foundations of Engineering Design Languages (SFEDL 2004). Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam (2004) (to appear)"},{"key":"24_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-540-24732-6_9","volume-title":"Model Checking Software","author":"I. Ober","year":"2004","unstructured":"Ober, I., Graf, S., Ober, I.: Validation of UML models via a mapping to communicating extended timed automata. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 127\u2013145. Springer, Heidelberg (2004)"},{"key":"24_CR14","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide, Menlo Park, CA (November 2001)"},{"key":"24_CR15","volume-title":"Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering (ASE 1999)","author":"I.P. Paltor","year":"1999","unstructured":"Paltor, I.P., Lilius, J.: vUML: A tool for verifying UML models. In: Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering (ASE 1999), IEEE, Los Alamitos (1999)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1007\/978-3-540-39910-0_26","volume-title":"Verification: Theory and Practice","author":"A. Pnueli","year":"2004","unstructured":"Pnueli, A., Arons, T.: TLPVS: A PVS-based LTL verification system. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 598\u2013623. Springer, Heidelberg (2004)"},{"key":"24_CR17","unstructured":"OMEGA. EU project IST 33522 (Correct Development of Real-Time Embedded systems). Homepage, \n                    \n                      http:\/\/www-omega.imag.fr\/"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-46428-X_10","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Reggio","year":"2000","unstructured":"Reggio, G., Astesiano, E., Choppy, C., Hussmann, H.: Analysing UML active classes and associated state machines \u2013 A lightweight formal approach. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 127. Springer, Heidelberg (2000)"},{"key":"24_CR19","unstructured":"Rational Rose Technical Developer. Rational, Inc., web page, \n                    \n                      http:\/\/www-306.ibm.com\/software\/awdtools\/developer\/technical\/"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-44450-5_26","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"E. Sedletsky","year":"2000","unstructured":"Sedletsky, E., Pnueli, A., Ben-Ari, M.: Formal verification of the Ricart-Agrawala algorithm. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 325\u2013335. Springer, Heidelberg (2000)"},{"key":"24_CR21","volume-title":"Real-Time Object-Oriented Modeling","author":"B. Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.: Real-Time Object-Oriented Modeling. John Wiley & Sons, New York (1994)"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-45221-8_6","volume-title":"\u00abUML\u00bb 2003 - The Unified Modeling Language. Modeling Languages and Applications","author":"S. Shankar","year":"2003","unstructured":"Shankar, S., Asa, S.: Formal semantics of UML with real-time constructs. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol.\u00a02863, pp. 60\u201375. Springer, Heidelberg (2003)"},{"key":"24_CR23","unstructured":"Telelogic TAU. Telelogic, Inc., \n                    \n                      http:\/\/www.telelogic.com\/products\/tau\/"},{"key":"24_CR24","unstructured":"TLPVS. Homepage, \n                    \n                      http:\/\/www.wisdom.weizmann.ac.il\/~verify\/tlpvs"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Traore, I., Aredo, D.B., Ye, H.: An integrated framework for formal development of open distributed systems. In: Proc. of ACM Symposium on Applied Computing, ACM SAC 2003 (2003)","DOI":"10.1145\/952532.952744"},{"key":"24_CR26","unstructured":"UML. Documentation of the Unified Modeling Language. Available from the Object Management Group (OMG), \n                    \n                      http:\/\/www.omg.org"}],"container-title":["Lecture Notes in Computer Science","<\u2009<UML>\u2009> 2004 - The Unified Modeling Language. Modelling Languages and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30187-5_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:53:38Z","timestamp":1620014018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30187-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540233077","9783540301875"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30187-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}