{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:21:11Z","timestamp":1784182871012,"version":"3.55.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,3,14]],"date-time":"2023-03-14T00:00:00Z","timestamp":1678752000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,3,14]],"date-time":"2023-03-14T00:00:00Z","timestamp":1678752000000},"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":["Real-Time Syst"],"published-print":{"date-parts":[[2023,6]]},"DOI":"10.1007\/s11241-023-09393-2","type":"journal-article","created":{"date-parts":[[2023,3,14]],"date-time":"2023-03-14T17:03:14Z","timestamp":1678813394000},"page":"160-198","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["CertiCAN certifying CAN analyses and their results"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4961-9923","authenticated-orcid":false,"given":"Pascal","family":"Fradet","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaojie","family":"Guo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sophie","family":"Quinton","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,3,14]]},"reference":[{"key":"9393_CR1","unstructured":"Arcticus Systems AB (2022) Rubus ICE: integrated component model development environment. https:\/\/www.arcticus-systems.com\/products\/rubus-tool-suite\/"},{"issue":"1","key":"9393_CR2","first-page":"0:21","volume":"5","author":"K Bletsas","year":"2018","unstructured":"Bletsas K, Audsley NC, Huang W et al (2018) Errata for three papers (2004\u201305) on fixed-priority scheduling with self-suspensions. LITES 5(1):0:21-02:20","journal-title":"LITES"},{"key":"9393_CR3","unstructured":"Bosch (1991) CAN specification version 2.0"},{"key":"9393_CR4","doi-asserted-by":"crossref","unstructured":"Cerqueira F, Stutz F, Brandenburg BB (2016) Prosa: a case for readable mechanized schedulability analysis. In: 28th Euromicro conference on real-time systems (ECRTS), IEEE, pp 273\u2013284","DOI":"10.1109\/ECRTS.2016.28"},{"key":"9393_CR5","unstructured":"CertiCAN (2021) A Coq tool to certify CAN analyses and their results. https:\/\/team.inria.fr\/spades\/certican2\/"},{"key":"9393_CR6","unstructured":"CompCert (2021) The CompCert C compiler. https:\/\/www.absint.com\/compcert\/"},{"key":"9393_CR7","unstructured":"Coq (2021) The Coq proof assistant. http:\/\/coq.inria.fr"},{"key":"9393_CR8","doi-asserted-by":"crossref","unstructured":"Davis RI, Navet N (2012) Controller area network (can) schedulability analysis for messages with arbitrary deadlines in fifo and work-conserving queues. In: 2012 9th IEEE international workshop on factory communication systems, IEEE, pp 33\u201342","DOI":"10.1109\/WFCS.2012.6242538"},{"issue":"3","key":"9393_CR9","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s11241-007-9012-7","volume":"35","author":"RI Davis","year":"2007","unstructured":"Davis RI, Burns A, Bril RJ et al (2007) Controller Area Network (CAN) schedulability analysis: refuted, revisited and revised. Real-Time Syst 35(3):239\u2013272","journal-title":"Real-Time Syst"},{"key":"9393_CR10","doi-asserted-by":"crossref","unstructured":"Davis RI, Kollmann S, Pollex V, et\u00a0al (2011) Controller area network (can) schedulability analysis with fifo queues. In: 2011 23rd Euromicro conference on real-time systems, IEEE, pp 45\u201356","DOI":"10.1109\/ECRTS.2011.13"},{"issue":"1","key":"9393_CR11","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s11241-012-9167-8","volume":"49","author":"RI Davis","year":"2013","unstructured":"Davis RI, Kollmann S, Pollex V et al (2013) Schedulability analysis for controller area network (can) with fifo queues priority queues and gateways. Real-Time Syst 49(1):73\u2013116","journal-title":"Real-Time Syst"},{"key":"9393_CR12","doi-asserted-by":"crossref","unstructured":"Du L, Xu G (2009) Worst case response time analysis for can messages with offsets. In: 2009 IEEE International conference on vehicular electronics and safety (ICVES), IEEE, pp 41\u201345","DOI":"10.1109\/ICVES.2009.5400204"},{"key":"9393_CR13","doi-asserted-by":"crossref","unstructured":"Dutertre B (2000) Formal analysis of the priority ceiling protocol. In: 21st IEEE real-time systems symposium (RTSS), pp 151\u2013160","DOI":"10.1109\/REAL.2000.896005"},{"key":"9393_CR14","unstructured":"Dutertre B, Stavridou V (2000) Formal analysis for real-time scheduling. In: 19th digital avionics systems conference (DASC)"},{"key":"9393_CR15","doi-asserted-by":"crossref","unstructured":"Fradet P, Guo X, Monin JF, et\u00a0al (2018) A generalized digraph model for expressing dependencies. In: RTNS\u201918-26th international conference on real-time networks and systems, pp 1\u201311","DOI":"10.1145\/3273905.3273918"},{"key":"9393_CR16","doi-asserted-by":"crossref","unstructured":"Fradet P, Guo X, Monin JF, et\u00a0al (2019) Certican: a tool for the Coq certification of CAN analysis results. In: 25th IEEE real-time and embedded technology and applications symposium, RTAS 2019, Montreal, QC, Canada, Apr 16\u201318, pp 182\u2013191","DOI":"10.1109\/RTAS.2019.00023"},{"key":"9393_CR17","doi-asserted-by":"crossref","unstructured":"Guo X, Quinton S, Fradet P et al (2017) (2017) Work-in-progress: toward a Coq-certified tool for the schedulability analysis of tasks with offsets. In: Real-time systems symposium (RTSS). IEEE, IEEE, pp 387\u2013389","DOI":"10.1109\/RTSS.2017.00049"},{"key":"9393_CR18","unstructured":"Ha V, Rangarajan M, Cofer D, et\u00a0al (2004) Feature-based decomposition of inductive proofs applied to real-time avionics software: an experience report. In: 26th conference on software engineering (ICSE), pp 304\u2013313"},{"key":"9393_CR19","unstructured":"Isabelle (2021) The Isabelle proof assistant. https:\/\/isabelle.in.tum.de\/"},{"issue":"7","key":"9393_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107\u2013115","journal-title":"Commun ACM"},{"key":"9393_CR21","doi-asserted-by":"crossref","unstructured":"Mabille E, Boyer M, Fejoz L, et\u00a0al (2013) Towards certifying network calculus. In: Proceedings of interactive theorem proving - 4th international conference, ITP 2013, Rennes, France, 22\u201326 July, pp 484\u2013489","DOI":"10.1007\/978-3-642-39634-2_37"},{"key":"9393_CR22","unstructured":"Mentor Graphics (2006) Volcano network architect. https:\/\/theeshadow.com\/files\/volvo\/can\/VNA_Datasheet.pdf"},{"key":"9393_CR23","unstructured":"Monot A, Navet N, Bavoux B, et\u00a0al (2012) Fine-grained simulation in the design of automotive communication systems. In: ERTSS-embedded real time software and systems-2012"},{"key":"9393_CR24","doi-asserted-by":"crossref","unstructured":"Mubeen S, M\u00e4m-Turja J, Sj\u00f6din M (2011) Extending schedulability analysis of controller area network (can) for mixed (periodic\/sporadic) messages. In: ETFA2011, IEEE, pp 1\u201310","DOI":"10.1109\/ETFA.2011.6059010"},{"key":"9393_CR25","doi-asserted-by":"crossref","unstructured":"Mubeen S, M\u00e4ki-Turja J, Sj\u00f6din M (2012) Worst-case response-time analysis for mixed messages with offsets in controller area network. In: Proceedings of 2012 IEEE 17th international conference on emerging technologies & factory automation (ETFA 2012), IEEE, pp 1\u201310","DOI":"10.1109\/ETFA.2012.6489579"},{"key":"9393_CR26","doi-asserted-by":"crossref","unstructured":"Mubeen S, M\u00e4ki-Turja J, Sj\u00f6din M (2013) Extending offset-based response-time analysis for mixed messages in controller area network. In: 2013 IEEE 18th conference on emerging technologies & factory automation (ETFA), IEEE, pp 1\u201310","DOI":"10.1109\/ETFA.2013.6648056"},{"issue":"10","key":"9393_CR27","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1016\/j.sysarc.2014.05.001","volume":"60","author":"S Mubeen","year":"2014","unstructured":"Mubeen S, M\u00e4ki-Turja J, Sj\u00f6din M (2014) Mps-can analyzer: integrated implementation of response-time analyses for controller area network. J Syst Architect 60(10):828\u2013841","journal-title":"J Syst Architect"},{"key":"9393_CR28","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic, vol 2283. Lecture notes in computer science. Springer, New York"},{"key":"9393_CR29","unstructured":"Prosa (2017) A Library for formally proven schedulability analysis. http:\/\/prosa.mpi-sws.org\/"},{"key":"9393_CR30","doi-asserted-by":"crossref","unstructured":"Quinton S, Bone TT, Hennig J, et\u00a0al (2014) Typical worst case response-time analysis and its use in automotive network design. In: The 51st annual design automation conference 2014, DAC \u201914, San Francisco, CA, USA, 1\u20135 June, pp 44:1\u201344:6","DOI":"10.1109\/DAC.2014.6881371"},{"key":"9393_CR31","unstructured":"RTaW-Pegase (2021) RTaW-Pegase: a Tool for Modeling, Simulation and automated Configuration of communication networks. http:\/\/www.realtimeatwork.com\/software\/rtaw-pegase\/"},{"key":"9393_CR32","unstructured":"Sel4 (2018) The seL4 microkernel. https:\/\/sel4.systems\/"},{"issue":"6","key":"9393_CR33","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1007\/s11241-015-9220-5","volume":"51","author":"M Stigge","year":"2015","unstructured":"Stigge M, Yi W (2015) Combinatorial abstraction refinement for feasibility analysis of static priorities. Real-Time Syst 51(6):639\u2013674","journal-title":"Real-Time Syst"},{"key":"9393_CR34","doi-asserted-by":"crossref","unstructured":"Stigge M, Guan N, Yi W (2014) Refinement-based exact response-time analysis. In: 26th Euromicro Conference on Real-Time Systems, ECRTS 2014, Madrid, Spain, 8\u201311 July, pp 143\u2013152","DOI":"10.1109\/ECRTS.2014.29"},{"key":"9393_CR35","unstructured":"SymTAS (2004) SymTA\/S: model-based timing analysis and optimization. https:\/\/auto.luxoft.com\/uth\/timing-analysis-tools\/"},{"key":"9393_CR36","unstructured":"Tindell K (1992) Using offset information to analyse static priority pre-emptively scheduled task sets. Technical report YCS 182, University of York, Department of Computer Science"},{"key":"9393_CR37","volume-title":"Adding time-offsets to schedulability analysis","author":"K Tindell","year":"1994","unstructured":"Tindell K (1994) Adding time-offsets to schedulability analysis. University of York, Department of Computer Science, New York"},{"key":"9393_CR38","unstructured":"Tindell K, Burns A (1994) Guaranteeing message latencies on controller area network (CAN). In: Proceedings of 1st international CAN conference, pp 1\u201311"},{"key":"9393_CR39","doi-asserted-by":"crossref","unstructured":"Tindell K, Hanssmon H, Wellings AJ (1994) Analysing real-time communications: Controller area network (CAN). In: Proceedings of the 15th IEEE real-time systems symposium (RTSS \u201994), San Juan, Puerto Rico, 7\u20139 Dec, pp 259\u2013263","DOI":"10.1109\/REAL.1994.342710"},{"issue":"8","key":"9393_CR40","doi-asserted-by":"publisher","first-page":"1163","DOI":"10.1016\/0967-0661(95)00112-8","volume":"3","author":"K Tindell","year":"1995","unstructured":"Tindell K, Burns A, Wellings A (1995) Calculating controller area network (CAN) message response times. Control Eng Pract 3(8):1163\u20131169","journal-title":"Control Eng Pract"},{"key":"9393_CR41","unstructured":"Vector (2022) Analyzing ECUs and Networks with CANalyzer. https:\/\/www.vector.com\/int\/en\/products\/products-a-z\/software\/canalyzer\/#"},{"key":"9393_CR42","doi-asserted-by":"crossref","unstructured":"Yomsi PM, Bertrand D, Navet N, et\u00a0al (2012) Controller area network (CAN): response time analysis with offsets. In: 2012 9th IEEE international workshop on factory communication systems, pp 43\u201352","DOI":"10.1109\/WFCS.2012.6242539"}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11241-023-09393-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11241-023-09393-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11241-023-09393-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,12]],"date-time":"2023-06-12T12:11:52Z","timestamp":1686571912000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11241-023-09393-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,14]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["9393"],"URL":"https:\/\/doi.org\/10.1007\/s11241-023-09393-2","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"value":"0922-6443","type":"print"},{"value":"1573-1383","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,14]]},"assertion":[{"value":"16 January 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 March 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}