CertiCAN: Certifying CAN Analyses and Their Results - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2021

CertiCAN: Certifying CAN Analyses and Their Results

(1) , (1) , (1)
1

Abstract

We present CertiCAN, a tool produced using the Coq proof assistant for the formal certification of CAN analysis results. Result certification is a process that is lightweight and flexible compared to tool certification. Indeed, the certification of an industrial analyzer needs access to the source code, requires the proof of many optimizations or implementation tricks and new proof effort at each software update. In contrast, CertiCAN only relies on the result provided by such a tool and remains independent of the tool itself or its updates. Furthermore, it is usually more time efficient to check a result than to produce it. All these reasons make CertiCAN a practical choice for industrial purposes. CertiCAN is based on the certification and combined use of two well-known CAN analysis tech- niques completed with additional optimizations. Experiments demonstrate that CertiCAN is com- putationally efficient and faster than the underlying combined analysis. It is able to certify the results of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. This result paves the way for a broader acceptance of formal tools for the certification of real-time systems analysis results.
Nous présentons CertiCAN, un outil produit à l’aide de l’assistant de preuves Coq et permettant de certifier les résultats d’analyses de bus CAN. La certification de résultats d’analyses est un procédé moins coûteux et plus flexible que la certification des analyses elles- mêmes. En effet, la certification d’un analyseur industriel demande l’accès au code source, la preuve d’un code souvent complexe avec de nombreuses optimisations ou astuces de mise en œuvre sans compter le besoin de nouvelles preuves à chaque mise à jour. CertiCAN, de son côté, n’a besoin que du résultat de l’analyse ; il reste indépendant de l’analyseur, de son implantation et de ses mises à jour. De plus, il est toujours plus efficace de vérifier un résultat que de le produire. Ces caractéristiques font de CertiCAN un choix pragmatique pour une utilisation industrielle. CertiCAN est basé sur la certification et l’utilisation combinée de deux techniques classiques d’analyse complétée par une collection d’optimisations. Les expérimentations montrent que Cer- tiCAN est efficace et plus rapide que les analyses sous-jacentes. Il est capable de certifier les résultats de RTaW-Pegase, un analyseur industriel de bus CAN, et ce même pour des systèmes complexes. Ce résultat ouvre la voie à une utilisation plus large d’outils formels pour la certifi- cation des résultats d’analyse de systèmes temps-réels.
Fichier principal
Vignette du fichier
RR-9443.pdf (1.84 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03499968 , version 1 (21-12-2021)

Identifiers

  • HAL Id : hal-03499968 , version 1

Cite

Pascal Fradet, Xiaojie Guo, Sophie Quinton. CertiCAN: Certifying CAN Analyses and Their Results. [Research Report] RR-9443, Inria - Research Centre Grenoble – Rhône-Alpes. 2021, pp.1-32. ⟨hal-03499968⟩
70 View
68 Download

Share

Gmail Facebook Twitter LinkedIn More