{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,9]],"date-time":"2024-05-09T07:45:35Z","timestamp":1715240735345},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,9,23]],"date-time":"2005-09-23T00:00:00Z","timestamp":1127433600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,4]]},"DOI":"10.1007\/s10009-005-0207-8","type":"journal-article","created":{"date-parts":[[2005,9,22]],"date-time":"2005-09-22T23:37:06Z","timestamp":1127432226000},"page":"97-112","source":"Crossref","is-referenced-by-count":6,"title":["A semantics of communicating reactive objects with timing"],"prefix":"10.1007","volume":"8","author":[{"given":"Jozef","family":"Hooman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark B.","family":"van der Zwaag","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,9,23]]},"reference":[{"key":"207_CR1","doi-asserted-by":"crossref","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M. Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Trans. Progr. Lang. Syst. 16, 1543\u20131571 (1994)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"207_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"207_CR3","doi-asserted-by":"crossref","unstructured":"Arons, T., Hooman, J., Kugler, H., Pnueli, A., van der Zwaag, M.: Deductive verification of UML models in TLPVS. In: Proceedings of the UML 2004, LNCS 3273, pp. 335\u2013349. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-30187-5_24"},{"key":"207_CR4","doi-asserted-by":"crossref","unstructured":"Bornot, S., Sifakis, J.: Relating time progress and deadlines in hybrid systems. In: Proceedings of the International Workshop, HART'97, Grenoble, LNCS 1201, pp. 286\u2013300. Spinger, Berlin Heidelberg New York (1997)","DOI":"10.1007\/BFb0014733"},{"key":"207_CR5","doi-asserted-by":"crossref","unstructured":"Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: a formal semantics of concurrency and communication in real-time UML. In: Proceedings of the Symposium on Formal Methods for Objects and Components (FMCO 2002), LNCS 2852, pp. 71\u201398. Springer, Berlin Heidelberg New York (2003)","DOI":"10.1007\/978-3-540-39656-7_3"},{"key":"207_CR6","unstructured":"Damm, W., Josko, B., Votintseva, A., Pnueli, A.: A formal semantics for a UML kernel language. Available via http:\/\/www-omega.imag.fr\/ Part I of IST\/33522\/WP1.1\/D1.1.2, Omega Deliverable (2003)"},{"key":"207_CR7","unstructured":"de Boer, F.S.: A proof rule for process creation. In: Proceedings of the Third IFIP WG 2.2 Working Conference (Formal Description of Programming Concepts 3) (1987)"},{"key":"207_CR8","doi-asserted-by":"crossref","unstructured":"Graf, S., Ober, I.: A real-time profile for UML and how to adapt it to SDL. In: Proceedings of the SDL 2003: System Design, SDL Forum, LNCS 2708, pp. 55\u201376 (2003)","DOI":"10.1007\/3-540-45075-0_4"},{"key":"207_CR9","doi-asserted-by":"crossref","unstructured":"Harel, D., Gery, E.: Executable object modeling with statecharts. IEEE Comput. 30, 31\u201342 (1997)","DOI":"10.1109\/2.596624"},{"key":"207_CR10","doi-asserted-by":"crossref","unstructured":"Harel, D., Kupfermann, O.: On the behavioral inheritance of state-based objects. In: Proceedings of the 34th International Conference on Component and Object Technology. IEEE Computer Society, Washington, DC (2000)","DOI":"10.1109\/TOOLS.2000.868961"},{"key":"207_CR11","unstructured":"Hooman, J., van der Zwaag, M.B.: UML semantics in PVS. http:\/\/www.cs.ru.nl\/\u223chooman\/STTTpvs.html"},{"key":"207_CR12","unstructured":"IBM\/Rational. Rose RealTime. http:\/\/www.ibm.com\/"},{"key":"207_CR13","unstructured":"IF: http:\/\/www-verimag.imag.fr\/\u223casync\/IF\/"},{"key":"207_CR14","unstructured":"Ilogix. Rhapsody. http:\/\/www.ilogix.com\/"},{"key":"207_CR15","doi-asserted-by":"crossref","unstructured":"Lilius, J., Paltor, I.P.: Formalising UML state machines for model checking. In: Proceedings of the UML 1999, LNCS 1723, pp. 430\u2013444. Springer, Berlin Heidelberg New York (1999)","DOI":"10.1007\/3-540-46852-8_31"},{"key":"207_CR16","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Proceedings of the 11th Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 607, pp. 748\u2013752. Springer, Berlin Heidelberg New York (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"207_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Arons, T.: TLPVS: a PVS-based LTL verification system. In: Proceedings of the Symposium on Verification: (Theory and Practice), LNCS 2772, pp. 598\u2013625. Springer, Berlin Heidelberg New York (2003)","DOI":"10.1007\/978-3-540-39910-0_26"},{"key":"207_CR18","unstructured":"PVS: http:\/\/pvs.csl.sri.com\/"},{"key":"207_CR19","doi-asserted-by":"crossref","unstructured":"Reggio, G., Astesiano, E., Choppy, C., Hu\u00dfmann, H.: Analysing UML active classes and associated statecharts\u2014a lightweight formal approach. In: Proceedings of the FASE 2000\u2013Fundamental Approaches to Software Engineering, LNCS 1783, pp. 127\u2013146. Springer, Berlin Heidelberg New York (2000)","DOI":"10.1007\/3-540-46428-X_10"},{"key":"207_CR20","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-time object-oriented modeling. Wiley, New York (1994)"},{"key":"207_CR21","unstructured":"UML: Documentation of the unified modeling language (uml). Available from the Object Management Group (OMG), http:\/\/www.uml.org\/"},{"key":"207_CR22","unstructured":"Uppaal: http:\/\/www.uppaal.com\/"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0207-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-005-0207-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0207-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T21:05:31Z","timestamp":1586466331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-005-0207-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,23]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["207"],"URL":"https:\/\/doi.org\/10.1007\/s10009-005-0207-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,9,23]]}}}