{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:46:27Z","timestamp":1754484387072},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999326"},{"type":"electronic","value":"9783319999333"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99933-3_12","type":"book-chapter","created":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T12:33:39Z","timestamp":1535200419000},"page":"170-186","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Probabilistic Analysis of Timing Constraints in Autonomous Automotive Systems Using Simulink Design Verifier"],"prefix":"10.1007","author":[{"given":"Eun-Young","family":"Kang","sequence":"first","affiliation":[]},{"given":"Li","family":"Huang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,26]]},"reference":[{"key":"12_CR1","unstructured":"Automotive open system architecture. https:\/\/www.autosar.org\/"},{"key":"12_CR2","unstructured":"Simulink Design Verifier. https:\/\/www.mathworks.com\/help\/sldv"},{"key":"12_CR3","unstructured":"IEC 61508: Functional safety of electrical electronic programmable electronic safety related systems. International Organization for Standardization, Geneva (2010)"},{"key":"12_CR4","unstructured":"EAST-ADL specification v2.1.9. Technical report, MAENAD (2011). https:\/\/www.maenad.eu\/public\/EAST-ADL-Specification_M2.1.9.1.pdf"},{"key":"12_CR5","unstructured":"ISO 26262\u20136: Road vehicles functional safety part 6. Product development at the software level. International Organization for Standardization, Geneva (2011)"},{"key":"12_CR6","unstructured":"MAENAD (2011). http:\/\/www.maenad.eu\/"},{"key":"12_CR7","unstructured":"Simulink library of PrCCSL (2018). https:\/\/github.com\/huangl223\/PrCCSL"},{"key":"12_CR8","unstructured":"Andr\u00e9, C.: Syntax and semantics of the clock constraint specification language (CCSL). Ph.D. thesis, INRIA (2009)"},{"issue":"4","key":"12_CR9","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1109\/12.919277","volume":"50","author":"G Bernat","year":"2001","unstructured":"Bernat, G., Burns, A., Llamosi, A.: Weakly hard real-time systems. Trans. Comput. 50(4), 308\u2013321 (2001)","journal-title":"Trans. Comput."},{"key":"12_CR10","unstructured":"Blom, H., et al.: TIMMO-2-USE timing model, tools, algorithms, languages, methodology, use cases. Technical report, TIMMO-2-USE (2012)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-57666-4_8","volume-title":"Formal Aspects of Component Software","author":"D Du","year":"2017","unstructured":"Du, D., Huang, P., Jiang, K., Mallet, F., Yang, M.: MARTE\/pCCSL: modeling and refining stochastic behaviors of CPSs with probabilistic logical clocks. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 111\u2013133. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57666-4_8"},{"key":"12_CR12","unstructured":"Gholami, M.R.: Verifying timed LTL properties using Simulink Design Verifier. Ph.D. thesis, \u00c9cole Polytechnique de Montr\u00e9al (2016)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-39031-9_8","volume-title":"Software Architecture","author":"A Goknil","year":"2013","unstructured":"Goknil, A., Suryadevara, J., Peraldi-Frati, M.-A., Mallet, F.: Analysis support for TADL2 timing constraints on EAST-ADL models. In: Drira, K. (ed.) ECSA 2013. LNCS, vol. 7957, pp. 89\u2013105. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39031-9_8"},{"issue":"10","key":"12_CR14","first-page":"1151","volume":"77","author":"J-F Etienne","year":"2010","unstructured":"Etienne, J.-F., Fechter, S., Juppeaux, E.: Using simulink design verifier for proving behavioral properties on a complex safety critical system in the ground transportation domain. Sci. Comput. Program. 77(10), 1151\u20131177 (2010)","journal-title":"Sci. Comput. Program."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Kang, E.Y., Chen, J., Ke, L., Chen, S.: Statistical analysis of energy-aware real-time automotive systems in EAST-ADL\/Stateflow. In: ICIEA, pp. 1328\u20131333. IEEE (2016)","DOI":"10.1109\/ICIEA.2016.7603790"},{"issue":"12","key":"12_CR16","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.ress.2013.06.007","volume":"120","author":"EY Kang","year":"2013","unstructured":"Kang, E.Y., Enoiu, E.P., Marinescu, R., Seceleanu, C., Schobbens, P.Y., Pettersson, P.: A methodology for formal analysis and verification of EAST-ADL models. Reliab. Eng. Syst. Saf. 120(12), 127\u2013138 (2013)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"12_CR17","unstructured":"Kang, E.Y., Huang, L.: Formal specification & analysis of autonomous systems in PrCCSL\/Simulink Design Verifier. Technical report, SYSU (2018). https:\/\/sites.google.com\/site\/kangeu\/home\/publications"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Kang, E.Y., Huang, L., Mu, D.: Formal verification of energy and timed requirements for a cooperative automotive system. In: SAC, pp. 1492\u20131499. ACM (2018)","DOI":"10.1145\/3167132.3167291"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Kang, E.Y., Ke, L., Hua, M.Z., Wang, Y.X.: Verifying automotive systems in EAST-ADL\/Stateflow using UPPAAL. In: APSEC, pp. 143\u2013150. IEEE (2015)","DOI":"10.1109\/APSEC.2015.17"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Kang, E.Y., Mu, D., Huang, L., Lan, Q.: Model-based analysis of timing and energy constraints in an autonomous vehicle system. In: QRS, pp. 525\u2013532. IEEE (2017)","DOI":"10.1109\/QRS-C.2017.90"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Kang, E.Y., Mu, D., Huang, L., Lan, Q.: Verification and validation of a cyber-physical system in the automotive domain. In: QRS, pp. 326\u2013333. IEEE (2017)","DOI":"10.1109\/QRS-C.2017.62"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Kang, E.Y., Schobbens, P.Y.: Schedulability analysis support for automotive systems: from requirement to implementation. In: SAC, pp. 1080\u20131085. ACM (2014)","DOI":"10.1145\/2554850.2554929"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-24270-0_18","volume-title":"Computer Safety, Reliability, and Security","author":"E-Y Kang","year":"2011","unstructured":"Kang, E.-Y., Schobbens, P.-Y., Pettersson, P.: Verifying functional behaviors of automotive products in EAST-ADL2 using UPPAAL-PORT. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 243\u2013256. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24270-0_18"},{"key":"12_CR24","doi-asserted-by":"publisher","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":"12_CR25","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-17581-2_13","volume-title":"Formal Techniques for Safety-Critical Systems","author":"R Marinescu","year":"2015","unstructured":"Marinescu, R., Kaijser, H., Miku\u010dionis, M., Seceleanu, C., L\u00f6nn, H., David, A.: Analyzing industrial architectural models by simulation and model-checking. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 189\u2013205. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17581-2_13"},{"issue":"1","key":"12_CR26","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/272991.272995","volume":"8","author":"M Matsumoto","year":"1998","unstructured":"Matsumoto, M., Nishimura, T.: Mersenne Twister: a 623-dimensionally equidistributed uniform pseudo-random number generator. TOMACS 8(1), 3\u201330 (1998)","journal-title":"TOMACS"},{"key":"12_CR27","unstructured":"Nicolau, G.B.: Specification and analysis of weakly hard real-time systems. Trans. Comput. pp. 308\u2013321 (1988)"},{"key":"12_CR28","unstructured":"Object Management Group: UML profile for MARTE: modeling and analysis of real-time embedded systems. Technical report (2011)"},{"key":"12_CR29","unstructured":"Qureshi, T.N., Chen, D.J., Persson, M., T\u00f6rngren, M.: Towards the integration of UPPAAL for formal verification of EAST-ADL timing constraint specification. In: TiMoBD workshop (2011)"},{"issue":"4","key":"12_CR30","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10009-014-0350-1","volume":"17","author":"D Reijsbergen","year":"2015","unstructured":"Reijsbergen, D., Boer, P.T.D., Scheinhardt, W., Haverkort, B.: On hypothesis testing for statistical model checking. STTT 17(4), 377\u2013395 (2015)","journal-title":"STTT"},{"key":"12_CR31","unstructured":"Simulink and Stateflow. https:\/\/www.mathworks.com\/products.html"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Suryadevara, J.: Validating EAST-ADL timing constraints using UPPAAL. In: SEAA, pp. 268\u2013275. IEEE (2013)","DOI":"10.1109\/SEAA.2013.46"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-40561-7_1"},{"issue":"4","key":"12_CR34","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/3140582.3081035","volume":"52","author":"M Zhang","year":"2017","unstructured":"Zhang, M., Ying, Y.: Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems. ACM SIGPLAN Not. 52(4), 61\u201370 (2017)","journal-title":"ACM SIGPLAN Not."}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99933-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T23:48:18Z","timestamp":1571788098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99933-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999326","9783319999333"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99933-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}