{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:07:48Z","timestamp":1761487668540},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,8,23]],"date-time":"2006-08-23T00:00:00Z","timestamp":1156291200000},"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":[[2007,3,2]]},"DOI":"10.1007\/s10009-006-0024-8","type":"journal-article","created":{"date-parts":[[2006,8,23]],"date-time":"2006-08-23T05:34:51Z","timestamp":1156311291000},"page":"179-192","source":"Crossref","is-referenced-by-count":2,"title":["Towards UML-based formal specifications of component-based real-time software"],"prefix":"10.1007","volume":"9","author":[{"given":"Vieri del","family":"Bianco","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Lavazza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Mauri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Occorso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,8,23]]},"reference":[{"key":"24_CR1","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. (1994) A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235","journal-title":"Theor. Comput. Sci."},{"key":"24_CR2","unstructured":"http:\/\/www.xjtek.com"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Bertin, V., Closse, E., Poize, M., Pulou, J., Sifakis, J., Venier, P., Weil, D., Yovine, S.: Taxys = Esterel + Kronos. A tool for verifying real-time properties of embedded systems. In: Conference on Decision and Control, CDC\u201901. Orlando, IEEE Control Systems Society (2001)","DOI":"10.1109\/CDC.2001.980712"},{"key":"24_CR4","unstructured":"Del Bianco, V.: Tecniche object-oriented formali per lo sviluppo di sistemi real-time, Politecnico di Milano. PhD Thesis, In Italian (2005)"},{"key":"24_CR5","unstructured":"Del Bianco, V., Lavazza, L., Mauri, M.: An application of the DESS modeling approach: the Car Speed Regulator, SIVOOES 2001, Budapest (2001)"},{"key":"24_CR6","unstructured":"Del Bianco, V., Lavazza, L., Mauri, M.: A classification of real-time specifications complexity, SIVOOES 2001, Budapest (2001)"},{"key":"24_CR7","unstructured":"Del Bianco, V., Lavazza, L., Mauri, M.: An introduction to the DESS approach to the specification of real-time software. CEFRIEL Technical Report RT01002 (2001)"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Del Bianco, V., Lavazza, L., Mauri, M.: Model Checking UML Specifications of Real Time Software. In: The Eighth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS02), Greenbelt (2002)","DOI":"10.1109\/ICECCS.2002.1181513"},{"key":"24_CR9","unstructured":"Del Bianco, V., Lavazza, L., Mauri, M.: A Formalization of UML Statecharts for Real-Time Software Modeling. In: The 6th Biennial World Conference On Integrated Design Process Technology (IDPT 2002), \u201cTowards a rigorous UML\u201d session, Pasadena (2002)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Eshuis, R., Wieringa, R.: Requirements-Level Semantics For UML Statecharts. Formal Methods for Open Object-Based Distributed Systems \u2013 FMOODS\u20192000, Stanford, 2000.","DOI":"10.1007\/978-0-387-35520-7_6"},{"key":"24_CR11","unstructured":"Eshuis, R.: Semantics and Verification of UML Activity Diagrams for Workflow Modelling, University of Twente, Centre for Telematics and Information Technology (2002)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., Mandrioli, D., Morzenti A.: TRIO, a logic language for executable specifications of real-time systems. The Journal of Systems and Software. vol. 12, n. 2. Elsevier, Amsterdam (1990)","DOI":"10.1016\/0164-1212(90)90074-V"},{"key":"24_CR13","unstructured":"Heitmeyer C.L., Jeffords R.D., Labaw B.G.: Comparing different approaches for Specifying and verifying Real-Time Systems. In: 10th IEEE Workshop on Real-Time Operating Systems and Software, pp. 122\u2013129 New York (1993)"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Timed and Hybrid Statecharts and their Textual Representation. In: Formal Techniques in Real-Time and Fault-Tolerant Systems 2nd International Symposium (1992)","DOI":"10.1007\/3-540-55092-5_32"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Lavazza, L., Quaroni, G., Venturelli, M.: Combining UML and formal notations for modelling real-time systems. In: Proceedings of ESEC\/FSE 2001. ACM Press Vienna (2001)","DOI":"10.1145\/503271.503236"},{"key":"24_CR16","unstructured":"Mauri, M.: Estensione di UML per la specifica e la verifica delle propriet\u00e0 di sistemi Real Time. Politecnico di Milano, Thesis, in Italian (2001)"},{"key":"24_CR17","unstructured":"OMG Unified Modeling Language Specification, Version 1.4 (OMG 2001)"},{"key":"24_CR18","unstructured":"OMG UML 2.0 Superstructure Specifcation Final Adopted Specification, ptc\/03-08-02, (OMG August 2003)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli A., Shalev, M.: What is in a step: On the semantics of statecharts. Intl. Conf. TACS \u201991: theoretical Aspects of Computer Software. Lecture Notes in Computer Science, vol. 526, pp. 244\u2013264 Springer, Berlin Heidelberg New York (1991)","DOI":"10.1007\/3-540-54415-1_49"},{"key":"24_CR20","unstructured":"Rational Software Corporation Modeling Language Guide, Rational Rose Real Time (2002)"},{"key":"24_CR21","unstructured":"Rational Software Corporation, Modeling Language Guide, Rational Rose Real Time, Version: 2002.05.00 (2002)"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Reggio, G., Astesiano, E., Choppy C., Hussmann, H.: Analysing UML active classes and associated state machines-a lightweight formal approach. In: FASE 2000 \u2013 to Software Engineering Lecture Notes in Science, vol. 1783. Springer, Berlin Heidelberg New York (2000)","DOI":"10.1007\/3-540-46428-X_10"},{"key":"24_CR23","volume-title":"Real-Time Object-Oriented Modeling","author":"B. Selic","year":"1994","unstructured":"Selic B., Gullekson G., Ward P.T. (1994) Real-Time Object-Oriented Modeling. Wiley, New York"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Sifakis, J.: Modeling real-time systems-challenges and work directions, EMSOFT01 Tahoe City, October 2001. Lecture Notes in Computer Science, vol. 2211. Springer, Berlin Heidelberg New York (2001)","DOI":"10.1007\/3-540-45449-7_26"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos, A Verification Tool for Real-Time Systems, Kronos User\u2019s Manual Release 2.2. Springer International Journal of Software Tools for technology Transfer, vol. 1, October (1997)","DOI":"10.1007\/s100090050009"},{"issue":"7","key":"24_CR26","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1109\/TSE.2004.34","volume":"30","author":"L. Apvrille","year":"2004","unstructured":"Apvrille L., Courtiat J., Lohr C., de Saqui-Sannes P. (2004) TURTLE: a real-time UML profile supported by a formal validation toolkit. IEEE Trans. Softw. Eng. 30(7): 473\u2013487","journal-title":"IEEE Trans. Softw. Eng."},{"key":"24_CR27","unstructured":"Real-time LOTOS, http:\/\/www.laas.fr\/RT-LOTOS (1998)"},{"key":"24_CR28","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. Computer Science, Automata, Languages and Programming vol. 443. Springer, Berlin Heidelberg New York (1990)"},{"key":"24_CR29","volume-title":"From HUPPAAL to UPPAAL-A translation from heirarchical timed automata to flat timed automata","author":"A. David","year":"2001","unstructured":"David A., M\u00f6ller M.O. (2001) From HUPPAAL to UPPAAL-A translation from heirarchical timed automata to flat timed automata. Deptartmenet Computer Science Aarhus Universitet, Aarhus"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2013 a tool suite for automatic verification of real-time systems, Computer Science, Hybrid Control Systems vol. 1066. Springer, Berlin Heidelberg New York (1996)","DOI":"10.1007\/BFb0020949"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Wang, F.: Model-checking distributed real-time systems with states, events, and multiple fairness assumptions. In: 10th International Conference Algebraic Methodology and Software Technology (2004)","DOI":"10.1007\/978-3-540-27815-3_41"},{"key":"24_CR32","unstructured":"Alur, R., Courcoubetis, C., Dill, D. L.: Model checking for realtime systems. In: 5th IEEE Symposium Logic in Computer Science (1990)"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Fischer, C., Olderog, E., Wehrheim, H.: A CSP View on UML-RT Structure Diagrams, LNCS vol. 2029 (2001)","DOI":"10.1007\/3-540-45314-8_8"}],"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-006-0024-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-006-0024-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0024-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:22Z","timestamp":1559100322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-006-0024-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8,23]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,3,2]]}},"alternative-id":["24"],"URL":"https:\/\/doi.org\/10.1007\/s10009-006-0024-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8,23]]}}}