{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:30:05Z","timestamp":1742963405209,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319226880"},{"type":"electronic","value":"9783319226897"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22689-7_33","type":"book-chapter","created":{"date-parts":[[2015,8,31]],"date-time":"2015-08-31T08:25:49Z","timestamp":1441009549000},"page":"425-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Probabilistic Verification of Time Constrained SysML State Machines"],"prefix":"10.1007","author":[{"given":"Abdelhakim","family":"Baouya","sequence":"first","affiliation":[]},{"given":"Djamal","family":"Bennouar","sequence":"additional","affiliation":[]},{"given":"Otmane","family":"Ait Mohamed","sequence":"additional","affiliation":[]},{"given":"Samir","family":"Ouchani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,1]]},"reference":[{"key":"33_CR1","unstructured":"OMG Systems Modeling Language ( Object Management Group SysML). O. M. Group (Ed.) (2012)"},{"key":"33_CR2","unstructured":"Abdelhakim, B.: State machine diagram verification (2015). https:\/\/github.com\/gitmodelcheking\/ATM\/blob\/master\/ATM.nm"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-39646-5_9","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2013","author":"T Ando","year":"2013","unstructured":"Ando, T., Yatsu, H., Kong, W., Hisazumi, K., Fukuda, A.: Formalization and model checking of SysML state machine diagrams by CSP#. In: Murgante, B., Misra, S., Carlini, M., Torre, C.M., Nguyen, H.-Q., Taniar, D., Apduhan, B.O., Gervasi, O. (eds.) ICCSA 2013, Part III. LNCS, vol. 7973, pp. 114\u2013127. Springer, Heidelberg (2013)"},{"key":"33_CR4","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"issue":"4","key":"33_CR6","first-page":"34","volume":"35","author":"M Ben-Menachem","year":"2010","unstructured":"Ben-Menachem, M.: Reactive systems: modelling, specification and verification. SIGSOFT Softw. Eng. Notes 35(4), 34\u201335 (2010)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"33_CR7","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-15228-3_9","volume-title":"Verification and Validation in Systems Engineering","author":"M Debbabi","year":"2010","unstructured":"Debbabi, M., Hassane, F., Jarraya, Y., Soeanu, A., Alawneh, L.: Probabilistic model checking of SysML activity diagrams. In: Debbabi, M., Hassane, F., Jarraya, Y., Soeanu, A., Alawneh, L. (eds.) Verification and Validation in Systems Engineering, pp. 153\u2013166. Springer, Berlin (2010)"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Doligalski, M., Adamski, M.: UML state machine implementation in FPGA devices by means of dual model and verilog. In: 11th IEEE International Conference on Industrial Informatics, INDIN 2013, 29\u201331 July 2013, Bochum, Germany, pp. 177\u2013184 (2013)","DOI":"10.1109\/INDIN.2013.6622878"},{"key":"33_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0504-8","volume-title":"Embedded System Design: Modeling, Synthesis and Verification","author":"DD Gajski","year":"2009","unstructured":"Gajski, D.D., Abdi, S., Gerstlauer, A., Schirner, G.: Embedded System Design: Modeling, Synthesis and Verification, 1st edn. Springer Publishing Company Incorporated, New York (2009)","edition":"1"},{"key":"33_CR10","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Huang, X., Sun, Q., Li, J., Pan, M., Zhang, T.: An MDE-based approach to the verification of SysML state machine diagram. In: Proceedings of the Fourth Asia-Pacific Symposium on Internetware, Internetware 2012, pp. 9:1\u20139:7. ACM, New York (2012)","DOI":"10.1145\/2430475.2430484"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Kaliappan, P.S., K\u00f6nig, H., Kaliappan, V.K.: Designing and verifying communication protocols using model driven architecture and spin model checker. In: International Conference on Computer Science and Software Engineering, CSSE 2008, Volume 2: Software Engineering, 12\u201314 December 2008, Wuhan, China, pp. 227\u2013230 (2008)","DOI":"10.1109\/CSSE.2008.976"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Mallet, F., de Simone, R.: MARTE: a profile for RT\/E systems modeling, analysis-and simulation? In: Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks and Systems & Workshops, SimuTools 2008, 3\u20137 March 2008, Marseille, France, p. 43 (2008)","DOI":"10.4108\/ICST.SIMUTOOLS2008.3097"},{"key":"33_CR14","volume-title":"Communicating and Mobile Systems: The $$\\pi $$-calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: The $$\\pi $$-calculus. Cambridge University Press, New York (1999)"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Norman, G., Palamidessi, C., Parker, D., Wu, P.: Model checking the probabilistic $$\\pi $$-calculus. In: Proceedings of the 4th International Conference on Quantitative Evaluation of Systems (QEST 2007), pp. 169\u2013178. IEEE Computer Society (2007)","DOI":"10.1109\/QEST.2007.31"},{"issue":"2","key":"33_CR16","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"33_CR17","doi-asserted-by":"crossref","unstructured":"Ouchani, S., Mohamed, O., Debbabi, M.: A probabilistic verification framework of sysml activity diagrams. In: IEEE 12th International Conference on Intelligent Software Methodologies, Tools and Techniques (SoMeT), vol. 246, pp. 165\u2013170, September 2013","DOI":"10.1109\/SoMeT.2013.6645657"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: From verification to implementation: a model translation tool and a pacemaker case study, pp. 173\u2013184 (2012)","DOI":"10.1109\/RTAS.2012.25"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201995: Concurrency Theory","author":"R Segala","year":"1995","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S. (eds.) CONCUR \u201995: Concurrency Theory. Lecture Notes in Computer Science, vol. 962, pp. 234\u2013248. Springer, Heidelberg (1995)"},{"key":"33_CR20","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"J Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. Communications in Computer and Information Science, vol. 17, pp. 307\u2013322. Springer, Heidelberg (2008)"}],"container-title":["Communications in Computer and Information Science","Intelligent Software Methodologies, Tools and Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22689-7_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:23:13Z","timestamp":1676960593000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22689-7_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319226880","9783319226897"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22689-7_33","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"1 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}