JetBrains Research unites scientists working in challenging new disciplines

Seminar on Mechanized proof of the correctness of bounding the maximum response time of a CAN message

Controller Area Network (CAN) is extensively used in automotive applications. In 1994 schedulability analysis was developed for CAN, showing how a worst-case response times of CAN messages could be calculated and hence guarantees provided that message response times would not exceed their deadlines. This seminal research has been transferred to industry in the form of commercial CAN schedulability analysis tools. But more than a decade later, it turned out that this analysis can provide guarantees for messages that, in the worst case, miss their deadlines. The report is devoted to proving the correctness of the revised CAN schedulability analisys. An overview of some types of schedulers, classical results of the theory of non-preemptive fixed-priority schedulers, and Prosa -- library of definitions and proofs for real-time schedulability analysis will be presented. In this report, the proof of the correctness of bounding the maximum response time of CAN messages will be considered in detail.

Supplementary materials:

Presenter: Sergey Bozhko

Date: April 24, 2017

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28