CertiCAN: Certifying CAN Analyses and Their Results

Autor: Pascal Fradet, Xiaojie Guo, Sophie Quinton
Přispěvatelé: Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Inria - Research Centre Grenoble – Rhône-Alpes, Fradet, Pascal, Institut National de Recherche en Informatique et en Automatique (Inria)
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Zdroj: [Research Report] RR-9443, Inria-Research Centre Grenoble – Rhône-Alpes. 2021, pp.1-32
[Research Report] RR-9443, Inria-Research Centre Grenoble – Rhône-Alpes. 2021
Real-Time Systems
Real-Time Systems, In press
ISSN: 0922-6443
1573-1383
Popis: We present CertiCAN, a tool produced using the Coq proof assistant for the formalcertification of CAN analysis results. Result certification is a process that is lightweight and flexiblecompared to tool certification. Indeed, the certification of an industrial analyzer needs access tothe source code, requires the proof of many optimizations or implementation tricks and new proofeffort at each software update. In contrast, CertiCAN only relies on the result provided by sucha tool and remains independent of the tool itself or its updates. Furthermore, it is usually moretime efficient to check a result than to produce it. All these reasons make CertiCAN a practicalchoice 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 theresults of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. This result pavesthe way for a broader acceptance of formal tools for the certification of real-time systems analysisresults.; Nous présentons CertiCAN, un outil produit à l’aide de l’assistant de preuvesCoq et permettant de certifier les résultats d’analyses de bus CAN. La certification de résultatsd’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, lapreuve 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 implantationet de ses mises à jour. De plus, il est toujours plus efficace de vérifier un résultat que de leproduire. Ces caractéristiques font de CertiCAN un choix pragmatique pour une utilisationindustrielle.CertiCAN est basé sur la certification et l’utilisation combinée de deux techniques classiquesd’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 lesrésultats de RTaW-Pegase, un analyseur industriel de bus CAN, et ce même pour des systèmescomplexes. 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.
Databáze: OpenAIRE
Externí odkaz: