CertiCAN certifying CAN analyses and their results

We present CertiCAN, a tool produced using the Coq proof assistant and based on the Prosa library for the formal verification of CAN analysis results. Result verification is a process that is lightweight and flexible compared to tool verification. Indeed, the formal verification of an industrial ana...

Full description

Saved in:
Bibliographic Details
Published in:Real-time systems 2023-06, Vol.59 (2), p.160-198
Main Authors: Fradet, Pascal, Guo, Xiaojie, Quinton, Sophie
Format: Article
Language:English
Subjects:
Communications Engineering
Computer Science
Computer Systems Organization and Communication Networks
Control
Experiments
Libraries
Mechatronics
Networks
Performance and Reliability
Robotics
Software
Source code
Special Purpose and Application-Based Systems
Systems analysis
Telematics
Usability
Verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present CertiCAN, a tool produced using the Coq proof assistant and based on the Prosa library for the formal verification of CAN analysis results. Result verification is a process that is lightweight and flexible compared to tool verification. Indeed, the formal verification 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 faster to check a result than to produce it. All these reasons make CertiCAN a practical choice for industrial purposes. CertiCAN is based on the formal verification and combined use of two well-known CAN analysis techniques completed with additional optimizations. Experiments demonstrate that CertiCAN is computationally 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.
ISSN:0922-6443
1573-1383
DOI:10.1007/s11241-023-09393-2