LogFire: правило-базированная runtime-верификация для надежного системного мониторинга

Правило-базированные системы кажутся естественными для runtime-верификации (RV)/мониторинга программ. С точки нотации спецификации, правило-базированные системы выглядят довольно подходящими для выражения тех видов свойств, которые runtime-верификация сообщество обычно пишет. Спецификации, написанные в системе правил, имеют операционный вкус, который может рассматриваться как недостаток или преимущество, в зависимости от точки зрения. Операционный вкус делает спецификации длиннее, чем в декларативной темпоральной логике или регулярных выражениях; однако они естественны для написания. Как только основная идея освоена, написание правил становится простым, как программирование. Более декларативные спецификации могут быть сложнее для правильного получения. Это наблюдение похоже на наблюдение, что может быть легче сформулировать нетривиальное свойство как машину состояний, чем как формулу темпоральной логики или регулярное выражение.

Марсоходы и космические аппараты JPL производят телеметрические потоки при работе. Телеметрический поток — это по сути последовательность событий, которая хранится на земле как лог в постоянной памяти. Операции миссии нуждаются в производстве автоматизированных проверок того, что эти логи корректны. LogFire может быть использован для проверки этих логов. LogFire, например, позволяет операционным инженерам автоматически гарантировать, что марсоход выполняет правильные шаги.

LogFire читает файл лога и проверяет его против формальной спецификации. Спецификация может быть сформулирована в правило-базированном языке. Правило-базированный спецификационный язык реализован как API в языке программирования Scala. Это приводит к очень мощному спецификационному языку, так как можно смешивать правила и традиционное программирование.

Определение правило-базированного языка как API в Scala имеет внешний вид DSL (Domain-Specific Language) благодаря поддержке Scala для определения таких (внутренних) DSL. Движок правил, основанный на хорошо известном алгоритме RETE, дополнительно расширен понятием событий, которые мгновенны в противовес долгосуществующим фактам, с которыми движки правил обычно работают. Наконец, метод индексирования оптимизировал движок для обработки событий, несущих данные.

LogFire кроме того позволяет легко кодировать спецификационные паттерны для генерации правил. Относительно просто определить спецификационные паттерны как фрагменты темпоральной логики и временных линий — экземпляры которых переводятся в правила. Интересный нюанс в том, что эти шаблоны позволяют данные-параметризованные события. Эксперименты выполнялись, сравнивая получившуюся реализацию с шестью другими runtime-верификационными и правило-базированными системами.

NASA стремится свободно лицензировать это программное обеспечение и сделать его доступным для общего использования для открытых проектов. Пожалуйста, свяжитесь с лицензиарным консьержем NASA по адресу This email address is being protected from spambots. You need JavaScript enabled to view it., или позвоните нам по телефону 202-358-7432 для начала лицензионных переговоров.