Семинар по механизированному доказательству корректности оценки максимального времени ответа CAN-сообщения

Семинар по механизированному доказательству корректности оценки максимального времени ответа CAN-сообщения

Controller Area Network (CAN) широко используется в автомобильной промышленности. В 1994 году был разработан анализ планируемости (schedulability) для CAN, который показал, как можно рассчитать наихудшее время ответа CAN-сообщения, и, следовательно, предоставлял гарантии того, что время отклика сообщения не превысит его дедлайна. Это исследование было использовано в промышленности в виде коммерческих средств анализа планируемости работы CAN. Но спустя более чем десятилетие оказалось, что этот анализ может предоставлять гарантии для сообщений, которые в худшем случае пропускают дедлайны. Доклад посвящён доказательству корректности пересмотренного анализа планируемости CAN. Будет дан обзор некоторых видов планировщиков, классических результатов теории невытесняющих планировщиков с фиксированным приоритетом (classic non-preemptive fixed-priority scheduling results) и библиотеки Prosa -- набора определений и доказательств анализа планируемости систем реального времени (real-time schedulability analysis). В данном докладе будет подробно рассмотрено доказательство корректности оценки максимального времени ответа CAN-сообщений.

Материалы для доклада:

https://link.springer.com/article/10.1007/s11241-007-9012-7http://prosa.mpi-sws.org/

Докладчик: Сергей Божко

24.04.2017, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28