{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:20:47Z","timestamp":1747887647713,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319165769"},{"type":"electronic","value":"9783319165776"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-16577-6_6","type":"book-chapter","created":{"date-parts":[[2015,3,29]],"date-time":"2015-03-29T02:05:04Z","timestamp":1427594704000},"page":"133-147","source":"Crossref","is-referenced-by-count":7,"title":["Temporal Properties Verification of Real-Time Systems Using UML\/MARTE\/OCL-RT"],"prefix":"10.1007","author":[{"given":"Aymen","family":"Louati","sequence":"first","affiliation":[]},{"given":"Kamel","family":"Barkaoui","sequence":"additional","affiliation":[]},{"given":"Chadlia","family":"Jerad","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"UML Profile for MARTE: Modeling and analysis of Real Time Embedded Systems, version 1.1(2012) OMG, http:\/\/www.omg.org"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"1509","DOI":"10.1093\/logcom\/exp036","volume":"19","author":"H. Boucheneb","year":"2009","unstructured":"Boucheneb, H., Gardey, G., Roux, O.: TCTL model- checking of Time Petri Nets. International Journal of Logic and Computation\u00a019, 1509\u20131540 (2009)","journal-title":"International Journal of Logic and Computation"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Tebibel, T.: Semantics of the Interaction Overview Diagram. In: Proceedings of the 10th IEEE International Conference on Information Reuse and Integration, USA, pp. 278\u2013283 (2009)","DOI":"10.1109\/IRI.2009.5211565"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-21210-9_9","volume-title":"Models in Software Engineering","author":"L. Baresi","year":"2011","unstructured":"Baresi, L., Morzenti, A., Motta, A., Rossi, M.: From Interaction Overview Diagrams to Temporal Logic. In: Dingel, J., Solberg, A. (eds.) MODELS 2010. LNCS, vol.\u00a06627, pp. 90\u2013104. Springer, Heidelberg (2011)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Louati, A., Jerad, C., Barkaoui, K.: On CPN-based Verification of Hierarchical Formalization of UML2 Interaction Overview Diagrams. In: 5th IEEE International Conference On Modeling, Simulation and Applied Optimization, Tunis, pp. 1\u20136 (2013)","DOI":"10.1109\/ICMSAO.2013.6552703"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Andrade, E., Marcel, P., Callou, G., Nogueira, B.: A Methodology for Mapping SysML Activity Diagram to Time Petri Net for Requirement Validation of Embedded Real-Time Systems with Energy Constraints. In: 3rd IEEE International Conference on Digital Society, USA, pp. 266\u2013271 (2009)","DOI":"10.1109\/ICDS.2009.19"},{"key":"6_CR7","unstructured":"Kangle, C., Zongyuan, Y., Jinkui, X., Kaiyu, W.: Unifying Modeling and Simulation Based on UML Timing Diagram and UPPAAL. In: IEEE Conference on Computer Modeling and Simulation, USA, pp. 615\u2013620 (2010)"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1504\/IJCCBS.2014.064663","volume":"5","author":"S. Boufenara","year":"2014","unstructured":"Boufenara, S., Barkaoui, K., Belala, F., Boucheneb, H.: Transactional Petri Nets: A Semantic Framework for UML2 Activities. International Journal on Critical Computing Based Systems\u00a05, 5\u201323 (2014)","journal-title":"International Journal on Critical Computing Based Systems"},{"key":"6_CR9","first-page":"53","volume":"19","author":"H. Seok Min","year":"2013","unstructured":"Seok Min, H., Chung, S.M., ChoiSmith, J.Y.: Deriving system behavior from UML state machine diagram. International Journal on computer Science Applied to Miss. Project.\u00a019, 53\u201377 (2013)","journal-title":"International Journal on computer Science Applied to Miss. Project."},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s11334-009-0116-1","volume":"6","author":"H. Hansen","year":"2010","unstructured":"Hansen, H., Ketema, J., Luttik, B., Mousavi, M., Van de Pol, J.: Towards model checking executable uml specifications in mcrl2. International Journal of Innovations in Systems and Software Engineering\u00a06, 83\u201399 (2010)","journal-title":"International Journal of Innovations in Systems and Software Engineering"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Andrade, E., Maciel, P., Callou, N.G.: Mapping UML interaction overview diagram to Time petri net for analysis and verification of Embedded real-time systems with Energy constraints. In: IEEE Conference on Computational Intelligence for Modeling Control and Automation, Vienna, pp. 615\u2013620 (2008)","DOI":"10.1109\/CIMCA.2008.44"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Ge, N., Pantel, M.: Time Properties Verification Framework for UML-MARTE Safety Critical Real-Time Systems. In: 8th European conference on Modeling Foundations and Applications, Lyngby, pp. 352\u2013367 (2012)","DOI":"10.1007\/978-3-642-31491-9_27"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Choi, J., Bae, D.H.: An approach to contructing Timing Diagrams from UML\/MARTE Behavioral Models for Guidance and Control Unit Software. In: International Conference, EL, DTA, and UNESST, Korea, pp. 107\u2013110 (2012)","DOI":"10.1007\/978-3-642-35603-2_16"},{"key":"6_CR14","unstructured":"Object Management Group, Inc: OMG UML2.5, Superstructure (October 2012), http:\/\/www.omg.org"},{"key":"6_CR15","unstructured":"Romeo tools, https:\/\/romeo.rts-software.org"},{"key":"6_CR16","first-page":"2138","volume":"2","author":"G.B. Vinai","year":"2013","unstructured":"Vinai, G.B., Vinod, K.A.: Verification of Interaction Overview Diagrams Using Colored Petri nets. International Journal of Advanced Research in Computer and Communication Engineering\u00a02, 2138\u20132149 (2013)","journal-title":"International Journal of Advanced Research in Computer and Communication Engineering"},{"key":"6_CR17","unstructured":"Joochim, T.: Bringing Requirements Engineering to Formal Methods Timing diagrams for Event-B and KAOS. Phd. Thesis, School of Electronics and Computer Science, University of Southampton (2010)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Louati, A., Barkaoui, K., Jerad, C.: Time properties Verification of UML\/MARTE Real-Time Systems. In: IEEE Workshop on Formal Methods Integration (IRI-FMI), San Francisco (2014)","DOI":"10.1109\/IRI.2014.7051915"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-45800-X_16","volume-title":"\u00abUML\u00bb 2002 - The Unified Modeling Language. Model Engineering, Concepts, and Tools","author":"S. Flake","year":"2002","unstructured":"Flake, S., M\u00fcller, W.: A UML Profile for Real-Time Constraints with the OCL. In: J\u00e9z\u00e9quel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol.\u00a02460, pp. 179\u2013195. Springer, Heidelberg (2002)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Flake, S., Mueller, W.: Specification of Real-Time Properties for UML Models. In: IEEE 35th Annual Hawaii International Conference on system sciences (HICSS-35), Hawaii, pp. 3977\u20133986 (2002)","DOI":"10.1109\/HICSS.2002.994469"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Flake, S., Mueller, W.: Past-and future-oriented time-bounded temporal properties with OCL. In: 2nd IEEE Conference on Software Engineering and Formal Methods, China, pp. 154\u2013163 (2004)","DOI":"10.1109\/SEFM.2004.1347516"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S1571-0661(05)80753-4","volume":"39","author":"E.E. Roubtsova","year":"2000","unstructured":"Roubtsova, E.E., Katwijk, J., Van Toetenel, W.J., Rooij, R.C.M.: Specification of Real-Time Systems in UML. Electronic Notes in Theoritical Computer Scince\u00a039, 293\u2013305 (2000)","journal-title":"Electronic Notes in Theoritical Computer Scince"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Tebibel, T.: Formal validation with OCL. In: IEEE Conference on Systems, Man and Cybernetics, Taipei, pp. 2736\u20132741 (2006)","DOI":"10.1109\/ICSMC.2006.385287"},{"key":"6_CR24","unstructured":"Bouamari, A., Mostefai, M.: V\u00e9rification formelle des mod\u00e8les UML temps-r\u00e9el. In: 4th International Conference on Computer Integrated Manufacturing, Troyes (2007)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Garcia, D.C., Cengarle, M.V., Szasz, N.: UML2.0 Interactions with OCL\/RT Constraints. In: Forum on Specification, Verification and Design Languages, Stuttgart, pp. 167\u2013172 (2008)","DOI":"10.1109\/FDL.2008.4641440"},{"key":"6_CR26","unstructured":"Boucheneb, H., Barkaoui, K.: Parametric Verification of Time Workflow Nets. In: 24th International Conference on Software Engineering, San Francisco, pp. 375\u2013380 (2012)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Ruf, J., Kropf, T.: Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. CHARME. In: Proceedings of International Conference. IFIP, pp. 146\u2013163. Chapman and Hall (1997)","DOI":"10.1007\/978-0-387-35190-2_10"}],"container-title":["Advances in Intelligent Systems and Computing","Formalisms for Reuse and Systems Integration"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-16577-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T18:18:48Z","timestamp":1747851528000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-16577-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319165769","9783319165776"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-16577-6_6","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2015]]}}}