Логфайр

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

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

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

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

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

НАСА стремится бесплатно лицензировать это программное обеспечение и сделать его доступным для общего использования в проектах с открытым исходным кодом. Пожалуйста, свяжитесь с консьержем НАСА по лицензированию:Этот адрес электронной почты защищен от спам-ботов. Для просмотра у вас должен быть включен JavaScript. Или позвоните нам по телефону 202-358-7432, чтобы начать обсуждение лицензирования.