{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,16]],"date-time":"2023-08-16T15:22:30Z","timestamp":1692199350842},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T00:00:00Z","timestamp":1078099200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2004,3]]},"DOI":"10.1007\/s10270-003-0029-7","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T18:29:20Z","timestamp":1079720960000},"page":"31-54","source":"Crossref","is-referenced-by-count":6,"title":["Formalization of UML state machines using temporal logic"],"prefix":"10.1007","volume":"3","author":[{"given":"Carlos","family":"Rossi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Enciso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inmaculada P.","family":"de Guzm\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,3,1]]},"reference":[{"key":"29_CR1","unstructured":"2U Consortium. UML 2 Submission, 2002. http:\/\/www.2uworks.org"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Allen, J.F.: Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11): 832\u2013843, 1983","DOI":"10.1145\/182.358434"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Allen, J.F.: Towards a general theory of action and time. Artificial Intelligence, 23(2): 123\u2013154, 1984","DOI":"10.1016\/0004-3702(84)90008-0"},{"key":"29_CR4","unstructured":"Anil Saldhana, J., Shatz, S.M.: UML diagrams to object Petri net models: An approach for modeling and analysis. In: Proceedings of the International Conference of Software and Knowledge Engineering SEKE\u201900, 2000, pp. 103\u2013110"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Barroca, L.M., McDermid, J.A.: Formal methods: Use and relevance for the development of safety-critical systems. Computer Journal, 35(6): 579\u2013599, 1992","DOI":"10.1093\/comjnl\/35.6.579"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Bicarregui, J.C.: Exploiting formality in software engineering, 1999. Invited paper at SOFSEM\u201999, 26th Annual Conference on Current Trends in Theory and Practice of Informatics","DOI":"10.1007\/3-540-47849-3_10"},{"key":"29_CR7","unstructured":"Booch, G.: Object-Oriented Analysis and Design with Applications. Addison Wesley, 1994"},{"key":"29_CR8","unstructured":"Booch, G., Rumbaugh J., Jacobson I.: Unified Modeling Language User Guide. Addison-Wesley, 1999"},{"key":"29_CR9","unstructured":"B\u00f6rger, E., Cavarra, A., Riccobene, E.: Modeling the dynamics of UML statecharts. In: Proceedings of International Workshop on Abstract State Machines ASM\u20192000, 2000, pp. 223\u2013241"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Chomicki, J., Saake, G. (eds.) Logics for database and information systems. Kluwer Academic Publishers, 1998","DOI":"10.1007\/978-1-4615-5643-5"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"de Guzm\u00e1n, I.P., Rossi, C.: LNint: a temporal logic that combines points and intervals and the absolute and relative approaches. Journal of the IGPL, 3(5), 1995","DOI":"10.1093\/jigpal\/3.5.745"},{"key":"29_CR12","unstructured":"Derr, K.W.: Applying OMT. SIGS Books, 1995"},{"key":"29_CR13","unstructured":"Diethers, K., Goltz, U., Huhn, M.: Model Checking UML Statecharts with Time. In: J\u00fcrjens, J., Cengarle, M.V., Fernandez, E.B., Rumpe, B., Sandner, R. (eds.) Wsh. Critical Systems Development with UML, Dresden, 2002, pp. 35\u201352. Technische Universit\u00e4t M\u00fcnchen, Institut f\u00fcr Informatik"},{"key":"29_CR14","unstructured":"Enciso, M., de Guzm\u00e1n, I.P., Rossi, C.: Using temporal logic to represent dynamic behaviour of UML statecharts. In: Hern\u00e1ndez, J., Moreira, A. (eds.) ECOOP 2002 Workshop on Integration and Transformation of UML Models, Lecture Notes in Computer Science, vol. 2548. Springer-Verlag, 2002"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M.: The declarative past and imperative future, Lecture Notes in Computer Science, vol. 398. Springer Verlag, 1989","DOI":"10.1007\/3-540-51803-7_36"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Latella, D., Massink, M.: Modular semantics for a UML statechart diagrams kernel and their extension to multicharts and branching time model checking. The Journal of Logic and Algebraic Programming, 51(1): 43\u201375, 2002","DOI":"10.1016\/S1567-8326(01)00012-1"},{"key":"29_CR17","unstructured":"Gogolla, M., Presicce, F.P.: State diagrams in UML: a formal semantics using graph transformations. In: Proceedings of Workshop on Precise Semantics of Modeling Techniques PSMT\u201998, 1998, pp. 55\u201372"},{"key":"29_CR18","unstructured":"Graw, G., Herrmann, P., Krumm, H.: Composing object-oriented specificactions and verifications with cTLA. In: Proceedings of Workshop on Semantics of Objects and Processes (SOAP\u201999). Lisboa, 1999, pp. 7\u201322"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Halpern, J., Shoham, Y.: A propositional modal logic of time intervals. Journal of the ACM, 38(4): 935\u2013962, 1991","DOI":"10.1145\/115234.115351"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming, 5: 231\u2013274, 1987","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Harel, D., Gery, E.: Executable object modeling with statecharts. Computer, 30(7): 31\u201342, 1997","DOI":"10.1109\/2.596624"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4): 293\u2013333, 1996","DOI":"10.1145\/235321.235322"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge, 1996","DOI":"10.4324\/9780203290644"},{"key":"29_CR24","unstructured":"Jacobson, I., Christerson, M., Jonsson, P., Overgard, G.: Object-Oriented Software Engineering. A Use Case Driven Approach. Addison-Wesley, 1992"},{"key":"29_CR25","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model Checking Timed UML State Machines and Collaborations. In: Damm, W., Olderog, E.R. (eds.) Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems, Lect. Notes Comp. Sci., vol. 2469. Springer, Berlin, 2002, pp. 395\u2013416"},{"key":"29_CR26","doi-asserted-by":"crossref","unstructured":"Kroger, F.: Temporal logic of programs. Springer Verlag, 1987. In EATCS Monograph on Theoretical Computer Science","DOI":"10.1007\/978-3-642-71549-5"},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"Kutsia, T.: Unification with sequence variables and flexible arity symbols and its extension with pattern.terms. In: Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AICS\u20192002 \u2013 Calculemos\u20192002 Conference, number 2385 in Lecture Notes in Artificial Intelligence. Springer-Verlag, 2002","DOI":"10.1007\/3-540-45470-5_26"},{"key":"29_CR28","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3): 872\u2013923, 1994","DOI":"10.1145\/177492.177726"},{"key":"29_CR29","doi-asserted-by":"crossref","unstructured":"Lano, K.: Logical specification of reactive and real-time systems. Journal of Logic and Computation, 8(5): 679\u2013711, 1998","DOI":"10.1093\/logcom\/8.5.679"},{"key":"29_CR30","unstructured":"Lano, K., Bicarregui, J.C.: Formalising the UML in structured temporal theories. In: Proceedings of Second ECOOP Workshop on Precise Behavioral Semantics, Brussels, Belgium, 1998"},{"key":"29_CR31","doi-asserted-by":"crossref","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-Checker. Formal Aspects Comp., 11(6): 637\u2013664, 1999","DOI":"10.1007\/s001659970003"},{"key":"29_CR32","doi-asserted-by":"crossref","unstructured":"Lavazza, L., Quaroni, G., Venturelli, M.: Combining UML and Formal Notations for Modelling Real-Time Systems. In: 8th Europ. Conf. Software Engineering, Wien, 2001","DOI":"10.1145\/503209.503236"},{"key":"29_CR33","unstructured":"Lilius, J., Porres, I.: The semantics of UML state machines. Technical report, Turku Centre for Computer Science, 1999"},{"key":"29_CR34","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. Springer-Verlag, 1995","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"29_CR35","unstructured":"Object Management Group. Unified Modeling Language Specification, version 1.4, 2001"},{"key":"29_CR36","unstructured":"Object Management Group. UML-Related Work In Progress, 2002. http:\/\/www.omg.org\/uml"},{"key":"29_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Symposium on the foundations of Computer Science. IEEE, 1977","DOI":"10.1109\/SFCS.1977.32"},{"key":"29_CR38","doi-asserted-by":"crossref","unstructured":"Polle, T., Ripke, T., Schewe, K.D. (eds.) Fundamentals of information systems. Kluwer Academic Publishers, 1999","DOI":"10.1007\/978-1-4615-5137-9"},{"key":"29_CR39","unstructured":"Reggio, G.: Metamodelling behavioural aspects: the case of the UML state machines. Technical Report DISI-TR-02-3, Universit\u00e9 di Genova, Italy, 2002"},{"key":"29_CR40","unstructured":"Robertson, D., Agust\u00ed, J.: Software Blueprints: Lightweight Uses of Logic in Conceptual Modelling. Addison-Wesley, 1999"},{"key":"29_CR41","unstructured":"Rossi, C.: L\u00f3gica Temporal de Intervalos. Formalizaci\u00f3n de Diagramas de Estados. PhD thesis, Universidad de M\u00e1laga, Spain, 2001"},{"key":"29_CR42","unstructured":"Rumbaugh, J., Blaha, M., Premerlani, W., Eddy, F., Lorensen, W.: Object-Oriented Modeling and Design. Prentice Hall, 1991"},{"key":"29_CR43","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Stoller, S., Visser, W. (eds.) Proc. Wsh. Software Model Checking, Elect. Notes Theo. Comp. Sci., vol. 55(3). Paris, 2001"},{"key":"29_CR44","unstructured":"Simons, A.J.: On the compositional properties of UML statechart diagrams. In: Clarke, A.N., Evans, A., Lano, K. (eds.) Proceedings of 3rd Conference on Rigourous Object-Oriented Methods, 2000, 2000, pp. 4.1\u20134.19"},{"key":"29_CR45","doi-asserted-by":"crossref","unstructured":"Simons, A.J., Graham, I.: 30 things that go wrong in object modelling with UML. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Precise Behavioral Specification of Businesses and Systems, chapter 17. Kluwer Academic Publishers, 1999","DOI":"10.1007\/978-1-4615-5229-1_17"},{"key":"29_CR46","doi-asserted-by":"crossref","unstructured":"Slotosch, O.: Overview over the project QUEST. In: Applied Formal Methods. Proceedings of FM-Trends 98, Boppard, Germany, Lecture Notes in Computer Science, vol. 1641. Springer Verlag, 1999, pp. 346\u2013350","DOI":"10.1007\/3-540-48257-1_25"},{"key":"29_CR47","unstructured":"U2 Partners. UML 2.0 Proposal, 2002. http:\/\/www.u2-partners.org"},{"key":"29_CR48","doi-asserted-by":"crossref","unstructured":"von der Beeck, M.: A comparison of statechart variants. In: Formal Techniques in Real-Time and Fault-Tolerant Systems, in Lecture Notes in Computer Science, vol. 863. Springer-Verlag, 1994, pp. 128\u2013148","DOI":"10.1007\/3-540-58468-4_163"},{"key":"29_CR49","doi-asserted-by":"crossref","unstructured":"von der Beeck, M.: A structured operational semantics for UML-statecharts. Software and System Modeling, 1(2): 130\u2013141, 2002","DOI":"10.1007\/s10270-002-0012-8"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-003-0029-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-003-0029-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-003-0029-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-003-0029-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T17:52:03Z","timestamp":1585677123000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-003-0029-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["29"],"URL":"https:\/\/doi.org\/10.1007\/s10270-003-0029-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}