{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:45:38Z","timestamp":1742913938523,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_27","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"433-449","source":"Crossref","is-referenced-by-count":7,"title":["An SMT-Based Approach to the Formal Analysis of MARTE\/CCSL"],"prefix":"10.1007","author":[{"given":"Min","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Mallet","sequence":"additional","affiliation":[]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"key":"27_CR1","unstructured":"Andr\u00e9, C., Cuccuru, A., Dekeyser, J.L., et al.: MARTE: a new OMG profile RFP for the modeling and analysis of real-time embedded systems. In: Proceedings of the 2nd UML-SoC Workshop (2005)"},{"key":"27_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard (version 2.5) (2015)"},{"key":"27_CR3","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"issue":"3","key":"27_CR5","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/s10617-014-9158-1","volume":"19","author":"E Ebeid","year":"2015","unstructured":"Ebeid, E., Fummi, F., Quaglia, D.: HDL code generation from UML\/MARTE sequence diagrams for verification and synthesis. Des. Autom. Embed. Syst. 19(3), 277\u2013299 (2015)","journal-title":"Des. Autom. Embed. Syst."},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th POPL, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Feiler, P., Hansson, J.: Flow latency analysis with the architecture analysis and design language (AADL) (2007)","DOI":"10.21236\/ADA455842"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Gascon, R., Mallet, F., DeAntoni, J.: Logical time and temporal logics: comparing UML MARTE\/CCSL and PSL. In: Proceedings of the 18th TIME, pp. 141\u2013148. IEEE CS (2011)","DOI":"10.1109\/TIME.2011.10"},{"issue":"7","key":"27_CR9","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Mallet, F., Andr\u00e9, C.: On the semantics of UML\/MARTE clock constraints. In: Proceedings of ISORC, pp. 305\u2013312. IEEE CS (2009)","DOI":"10.1109\/ISORC.2009.27"},{"key":"27_CR11","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1016\/j.scico.2015.03.001","volume":"106","author":"F Mallet","year":"2015","unstructured":"Mallet, F., de Simone, R.: Correctness issues on MARTE\/CCSL constraints. Sci. Comput. Program. 106, 78\u201392 (2015)","journal-title":"Sci. Comput. Program."},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"6","key":"27_CR13","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nut\u0103, T.F.: An overview of the $$\\mathbb{K}$$ semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-40561-7_1","volume-title":"Software Engineering and Formal Methods","author":"J Suryadevara","year":"2013","unstructured":"Suryadevara, J., Seceleanu, C., Mallet, F., Pettersson, P.: Verifying MARTE\/CCSL mode behaviors using UPPAAL. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 1\u201315. Springer, Heidelberg (2013)"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Yin, L., Mallet, F., Liu, J.: Verification of MARTE\/CCSL time requirements in Promela\/SPIN. In: Proceedings of the 16th ICECCS, pp. 65\u201374. IEEE CS (2011)","DOI":"10.1109\/ICECCS.2011.14"},{"key":"27_CR16","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-29510-7_2","volume-title":"Formal Techniques for Safety-Critical Systems","author":"M Zhang","year":"2016","unstructured":"Zhang, M., Mallet, F.: An executable semantics of clock constraint specification language and its applications. In: Artho, C., et al. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 37\u201351. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-29510-7_2"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T11:53:49Z","timestamp":1568462029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}