CertiCAN: A Tool for the Coq Certification of CAN Analysis Results
| Autor: | Sophie Quinton, Jean-François Monin, Pascal Fradet, Xiaojie Guo |
|---|---|
| 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 ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), ANR-17-CE25-0016,RT-proofs,Preuves formelles pour systèmes temps-réel(2017) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Process (engineering)
Computer science business.industry 05 social sciences Proof assistant Combined use ComputerApplications_COMPUTERSINOTHERSYSTEMS 02 engineering and technology Certification 020202 computer hardware & architecture CAN bus Systems analysis 0502 economics and business 0202 electrical engineering electronic engineering information engineering 050211 marketing [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Software engineering business Formal verification |
| Zdroj: | RTAS 2019-25th IEEE Real-Time and Embedded Technology and Applications Symposium RTAS 2019-25th IEEE Real-Time and Embedded Technology and Applications Symposium, Apr 2019, Montreal, Canada. pp.1-10, ⟨10.1109/RTAS.2019.00023⟩ RTAS |
| Popis: | International audience; This paper introduces 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, which makes it a practical choice for industrial purposes. The analysis underlying CertiCAN, which is based on a combined use of two well-known CAN analysis techniques, is computationally efficient. Experiments demonstrate that Certi-CAN is faster than the corresponding certified combined analysis. More importantly, 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|