{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:40:02Z","timestamp":1746265202493,"version":"3.40.4"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,6,11]],"date-time":"2014-06-11T00:00:00Z","timestamp":1402444800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10009-014-0305-6","type":"journal-article","created":{"date-parts":[[2014,6,10]],"date-time":"2014-06-10T23:51:45Z","timestamp":1402444305000},"page":"399-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Quantitative and qualitative analysis of SysML activity diagrams"],"prefix":"10.1007","volume":"16","author":[{"given":"Yosr","family":"Jarraya","sequence":"first","affiliation":[]},{"given":"Mourad","family":"Debbabi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,6,11]]},"reference":[{"key":"305_CR1","unstructured":"OMG: OMG Unified Modeling Language Superstructure Version 2.4.1. Object Management Group (2011)"},{"key":"305_CR2","unstructured":"OMG: OMG Systems Modeling Language (OMG SysML) Version 1.3. Object Management Group (2012)"},{"key":"305_CR3","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1504\/IJPD.2005.006672","volume":"2","author":"C Bock","year":"2005","unstructured":"Bock, C.: Systems engineering in the product lifecycle. Int. J. Prod. Dev. 2, 123\u2013137 (2005)","journal-title":"Int. J. Prod. Dev."},{"issue":"2","key":"305_CR4","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"305_CR5","first-page":"130","volume":"121","author":"RJV Glabbeek","year":"1990","unstructured":"Glabbeek, R.J.V., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121, 130\u2013141 (1990)","journal-title":"Inf. Comput."},{"key":"305_CR6","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: Symposium on Principles of Programming Languages, pp. 344\u2013352 (1989). doi: 10.1145\/75277.75307","DOI":"10.1145\/75277.75307"},{"key":"305_CR7","doi-asserted-by":"crossref","unstructured":"Jarraya, Y., Debbabi, M., Bentahar, J.: On the meaning of SysML activity diagrams. In: The Proceedings of the 16th Annual IEEE International Conference on the Engineering of Computer Based Systems (ECBS), vol 0, pp. 95\u2013105. IEEE Computer Society, Los Alamitos (2009)","DOI":"10.1109\/ECBS.2009.25"},{"key":"305_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-15228-3","volume-title":"Verification and Validation in Systems Engineering: Assessing UML\/SysML Design Models","author":"M Debbabi","year":"2010","unstructured":"Debbabi, M., Hassaine, F., Jarraya, Y., Soeanu, A., Alawneh, L.: Verification and Validation in Systems Engineering: Assessing UML\/SysML Design Models. Springer, Berlin (2010)"},{"key":"305_CR9","doi-asserted-by":"crossref","unstructured":"Jarraya, Y., Debbabi, M.: Formal specification and probabilistic verification of SysML activity diagrams. In: Margaria, T, Qiu, Z., Yang, H. (eds.) TASE, pp. 17\u201324. IEEE (2012)","DOI":"10.1109\/TASE.2012.34"},{"key":"305_CR10","unstructured":"Beato, M.E., Barrio-Sol\u00f3rzano, M., Cuesta, C.E.: UML automatic verification tool (TABU). In: Proceedings of the 12th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Specification and Verification of Component-Based Systems, Newport Beach, California, USA (SAVCBS\u201904), Department of Computer Science, Iowa State University, Ames, Iowa, United States (2004)"},{"issue":"1","key":"305_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1125808.1125809","volume":"15","author":"R Eshuis","year":"2006","unstructured":"Eshuis, R.: Symbolic model checking of UML activity diagrams. ACM Trans. Softw. Eng. Methodol. 15(1), 1\u201338 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"305_CR12","doi-asserted-by":"crossref","unstructured":"Canevet,C., Gilmore, S., Hillston, J., Kloul, L., Stevens, P.: Analysing UML 2.0 activity diagrams in the software performance engineering process. In: The Proceedings of the Fourth International Workshop on Software and Performance. ACM Press, Redwood Shores, California, USA, pp 74\u201378 (2004)","DOI":"10.1145\/974043.974055"},{"key":"305_CR13","doi-asserted-by":"crossref","unstructured":"Gallotti, S., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Quality prediction of service compositions through probabilistic model checking. In: The Proceedings of the 4th International Conference on Quality of Software-Architectures (QoSA\u201908), pp. 119\u2013134. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-87879-7_8"},{"key":"305_CR14","doi-asserted-by":"crossref","unstructured":"Lindemann, C., Th\u00fcmmler, A., Klemm, A., Lohmann, M., Waldhorst, O.P.: Performance analysis of time-enhanced UML diagrams based on stochastic processes. In: The Proceedings of the 3rd International Workshop on Software and Performance (WOSP), pp. 25\u201334. ACM Press, New York (2002)","DOI":"10.1145\/584369.584375"},{"key":"305_CR15","doi-asserted-by":"crossref","unstructured":"Tabuchi, N., Sato, N., Nakamura, H.: Model-driven performance analysis of UML design models based on stochastic process algebra. In: The Proceedings of the First European Conference on Model Driven Architecture\u2014Foundations and Applications (ECMDA-FA). LNCS, vol. 3748, pp. 41\u201358. Springer, Berlin (2005)","DOI":"10.1007\/11581741_5"},{"key":"305_CR16","doi-asserted-by":"crossref","unstructured":"Tribastone, M., Gilmore, S.: Automatic extraction of PEPA performance models from UML activity diagrams annotated with the MARTE profile. In: The Proceedings of the 7th International Workshop on Software and Performance (WOSP), pp. 67\u201378. ACM, New York (2008)","DOI":"10.1145\/1383559.1383569"},{"key":"305_CR17","doi-asserted-by":"crossref","unstructured":"Tribastone, M., Gilmore, S.: Automatic translation of UML sequence diagrams into PEPA models. In: Proceedings of the Fifth International Conference on Quantitative Evaluation of Systems September 2008 (QEST), pp 205\u2013214. IEEE Computer Society, Los Alamitos (2008)","DOI":"10.1109\/QEST.2008.18"},{"key":"305_CR18","doi-asserted-by":"crossref","unstructured":"Jarraya, Y., Soeanu, A., Debbabi, M., Hassa\u00efne, F.: Automatic verification and performance analysis of time-constrained SysML activity diagrams. In: The Proceedings of the 14th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS), pp. 515\u2013522. IEEE Computer Society, Los Alamitos, CA, USA (2007)","DOI":"10.1109\/ECBS.2007.22"},{"key":"305_CR19","unstructured":"OMG: UML Profile for Schedulability, Performance and Time. Object Management Group (2005)"},{"key":"305_CR20","unstructured":"OMG: A UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems, Beta 2. Object Management Group, OMG Adopted Specification (2008)"},{"key":"305_CR21","unstructured":"Leitner-Fischer F., Leue, S.: Quantitative analysis of UML models. In: Giese, H., Huhn, M., Phillips, J., Sch\u00e4tz, B. (eds.) MBEES, Fortiss GmbH, M\u00fcnchen, pp. 91\u2013100 (2011)"},{"key":"305_CR22","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2005.12.059","volume":"159","author":"A Kamandi","year":"2006","unstructured":"Kamandi, A., Azgomi, M.A., Movaghar, A.: Transformation of UML models into analyzable OSAN models. Electron. Notes Theor. Comput. Sci. 159, 3\u201322 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"305_CR23","doi-asserted-by":"crossref","unstructured":"St\u00f6rrle, H.: Semantics of control-flow in UML 2.0 activities. In: IEEE Symposium on Visual Languages and Human-Centric Computing (VL\/HCC), pp 235\u2013242. IEEE Computer Society (2004)","DOI":"10.1109\/VLHCC.2004.46"},{"key":"305_CR24","unstructured":"St\u00f6rrle, H.: Semantics of exceptions in UML 2.0 Activities. Technical Report 0403, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Institut f\u00fcr Informatik (2004)"},{"issue":"4","key":"305_CR25","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.entcs.2004.08.046","volume":"127","author":"H St\u00f6rrle","year":"2005","unstructured":"St\u00f6rrle, H.: Semantics and verification of data flow in UML 2.0 activities. Electron. Notes Theor. Comput. Sci. 127(4), 35\u201352 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"305_CR26","doi-asserted-by":"crossref","unstructured":"Yang, N., Yu, H., Sun, H., Qian, Z.: Mapping UML activity diagrams to analyzable Petri net models. In: International Conference on Quality Software, pp. 369\u2013372. IEEE Computer Society, Los Alamitos (2010)","DOI":"10.1109\/QSIC.2010.26"},{"key":"305_CR27","unstructured":"St\u00f6rrle, H., Hausmann, J.H.: Towards a formal semantics of UML 2.0 activities. In: Software Engineering, Gesellschaf fuer Informatik, GI, LNI, vol. 64, pp. 117\u2013128 (2005)"},{"key":"305_CR28","doi-asserted-by":"crossref","unstructured":"Pedroza, G., Apvrille, L., Knorreck, D.: AVATAR: a SysML environment for the formal verification of safety and security properties. In: The Proceedings of the 11th Annual International Conference on New Technologies of Distributed Systems (NOTERE), pp. 1\u201310 (2011)","DOI":"10.1109\/NOTERE.2011.5957992"},{"issue":"1","key":"305_CR29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1921532.1921556","volume":"36","author":"D Knorreck","year":"2011","unstructured":"Knorreck, D., Apvrille, L., de Saqui-Sannes, P.: TEPE: a SysML language for time-constrained property modeling and formal verification. ACM SIGSOFT Softw. Eng. Notes 36(1), 1\u20138 (2011)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"305_CR30","unstructured":"Kerzhner, A.A, Paredis, C.J.: Combining SysML and model transformations to support systems engineering analysis. In: Proceedings of the 4th International Workshop on Multi-Paradigm Modeling (MPM\u201910)-Electronic Communications of the EASST, vol. 42 (2011)"},{"key":"305_CR31","doi-asserted-by":"crossref","unstructured":"Kawahara, R., Nakamura, H., Dotan, D., Kirshin, A., Sakairi, T., Hirose, S., Ono, K., Ishikawa, H.: Verification of embedded system\u2019s specification using collaborative simulation of SysML and simulink models. In: International Conference on Model-Based, Systems Engineering, (MBSE\u201909), pp. 21\u201328 (2009)","DOI":"10.1109\/MBSE.2009.5031716"},{"key":"305_CR32","doi-asserted-by":"crossref","unstructured":"Huang, X., Sun, Q., Li, J., Zhang, T.: MDE-based verification of SysML state machine diagram by UPPAAL. In: Trustworthy Computing and Services, pp. 490\u2013497. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-35795-4_62"},{"key":"305_CR33","doi-asserted-by":"crossref","unstructured":"Dubois, H., Peraldi-Frati, M., Lakhal, F.: A model for requirements traceability in a heterogeneous model-based design process: application to automotive embedded systems. In: 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 233\u2013242 (2010)","DOI":"10.1109\/ICECCS.2010.2"},{"issue":"4","key":"305_CR34","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s11334-011-0170-3","volume":"7","author":"S Chouali","year":"2011","unstructured":"Chouali, S., Hammad, A.: Formal verification of components assembly based on SysML and interface automata. Innov. Syst. Softw. Eng. 7(4), 265\u2013274 (2011)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"305_CR35","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Quantitative analysis with the probabilistic model checker PRISM. Electron. Notes Theor. Comput. Sci. 153(2), 5\u201331 (2005)"},{"issue":"4","key":"305_CR36","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/1059816.1059820","volume":"32","author":"M Kwiatkowska","year":"2005","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: case studies with PRISM. ACM SIGMETRICS Perform. Eval. Rev. 32(4), 16\u201321 (2005)","journal-title":"ACM SIGMETRICS Perform. Eval. Rev."},{"key":"305_CR37","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Kattenbelt, M.: PRISM\u2014Probabilistic Symbolic Model Checker (2008). http:\/\/www.prismmodelchecker.org\/manual\/ . Last Visited March 2013"},{"issue":"1","key":"305_CR38","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Form. Methods Syst. Des."},{"key":"305_CR39","unstructured":"PRISM Team: The PRISM Language-Semantics (2008). http:\/\/www.prismmodelchecker.org\/doc\/semantics.pdf . Last Visited March 2013"},{"key":"305_CR40","unstructured":"Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)"},{"key":"305_CR41","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Branching vs. linear time: final showdown. In: The Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 1\u201322. Springer, London (2001)","DOI":"10.1007\/3-540-45319-9_1"},{"key":"305_CR42","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic . In: 25 Years of Model Checking. LNCS, vol. 5000, pp 196\u2013215. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-69850-0_12"},{"key":"305_CR43","volume-title":"Communicating and Mobile Systems: the $$\\pi $$ \u03c0","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the $$\\pi $$ \u03c0 -Calculus. Cambridge University Press, UK (1999)"},{"key":"305_CR44","unstructured":"OMG: OMG Systems Modeling Language (OMG SysML) Specification. Object Management Group, OMG Available Specification (2007)"},{"key":"305_CR45","doi-asserted-by":"crossref","unstructured":"Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical techniques for analyzing concurrent and probabilistic systems. In: Panangaden, P., van Breugel, F. (eds.) CRM Monograph Series, vol. 23. American Mathematical Society, Providence (2004)","DOI":"10.1090\/crmm\/023"},{"key":"305_CR46","unstructured":"Harper, R.: Programming in Standard ML. Online working draft (2009). http:\/\/www.cs.cmu.edu\/~rwh\/smlbook\/online.pdf"},{"key":"305_CR47","doi-asserted-by":"crossref","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Kret\u00ednsk\u00fd, M., Jancar, P. (eds.) Concurrency Theory (CONCUR\u201902). LNCS, vol. 2421, pp. 371\u2013386. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45694-5_25"},{"key":"305_CR48","unstructured":"Stoelinga, M.: Verification of Probabilistic, Real-Time and Parametric Systems. PhD thesis, University of Nijmegen, The Netherlands (2002)"},{"key":"305_CR49","doi-asserted-by":"crossref","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. In: The Proceedings of the Concurrency Theory (CONCUR\u201994), pp. 481\u2013496. Springer, London (1994)","DOI":"10.1007\/978-3-540-48654-1_35"},{"key":"305_CR50","unstructured":"Baier, C.: On algorithmic verification methods for probabilistic systems. Habilitation thesis, Fakult\u00e4t f\u00fcr Mathematik & Informatik, Universit\u00e4t Mannheim (1998). http:\/\/wwwneu.inf.tu-dresden.de\/content\/institutes\/thi\/algi\/publikationen\/texte\/15_98.pdf"},{"key":"305_CR51","unstructured":"PRISM: PRISM-Probabilistic Symbolic Model Checker (2007). http:\/\/www.prismmodelchecker.org\/index.php . Last visited March 2013"},{"key":"305_CR52","unstructured":"Pietriga, E.: A toolkit for addressing HCI issues in visual language environments. In: IEEE Symposium on Visual Languages and Human-Centric Computing (VL\/HCC), vol. 00, pp. 145\u2013152 (2005). http:\/\/doi.ieeecomputersociety.org\/10.1109\/VLHCC.2005.11"}],"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-014-0305-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0305-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0305-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:17:08Z","timestamp":1746263828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0305-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,11]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["305"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0305-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,6,11]]}}}