В Linux ядре появятся LTL-спецификации для верификации поведения ядра: Монитор верификации времени выполнения — это метод верификации, который проверяет, что ядро следует спецификации. Это достигается с помощью точек трассировки для мониторинга трассировки выполнения ядра и проверки того, что трассировка выполнения соответствует спецификации. Изначально спецификация могла быть написана только в форме детерминированного автомата (ДА). Однако при попытке реализовать мониторы ДА для некоторых сложных спецификаций детерминированный автомат оказался неподходящим языком спецификации. Автомат сложен, труден для понимания и подвержен ошибкам. Поэтому были введены мониторы RV, основанные на линейной временной логике (LTL). Этот тип монитора использует LTL в качестве спецификации вместо ДА. В некоторых случаях запись спецификации в виде LTL более лаконична и интуитивна. Патчсет: https://lore.kernel.org/lkml/cover.1745390829.git.namcao@linutronix.de/
В Linux ядре появятся LTL-спецификации для верификации поведения ядра
8 августа 20258 авг 2025
~1 мин