Исследовательская группа

Лаборатория языковых инструментов

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

April 24

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/

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