LogFire：基于规则的运行时验证 保障系统可靠监控
基于规则的系统似乎天然适合运行时验证（RV）/程序监控。从规范符号角度看，基于规则系统颇适合表达运行时验证社区常写的属性类型。规则系统编写的规范有操作风味，视角不同可视为劣势或优势。操作风味使规范比声明式时序逻辑或正则表达式长；但编写自然。掌握核心思想后，写规则如编程般直观。更声明式规范反而更难写对。此观察类似：用状态机表达非平凡属性比用时序逻辑公式或正则表达式更容易。
JPL探测器和航天器运行时产生遥测流。遥测流本质是事件序列，存储于地面持久内存日志。任务运营需自动化检查日志正确性。LogFire可用于检查日志。例如，LogFire让运营工程师自动确保探测器执行正确步骤。
LogFire读取日志文件并对照形式化规范检查。规范可用基于规则语言表达。基于规则的规范语言作为API实现于Scala编程语言。这造就极强大规范语言，因可混合规则和传统编程。
规则语言在Scala中定义为API，因Scala支持定义此类（内部）DSL，呈现DSL（领域特定语言）外观。规则引擎基于著名RETE算法，并增强事件概念——事件即时发生，区别于规则引擎通常处理的长生命周期事实。最后，索引方法优化引擎处理携带数据的事件。
LogFire还允许轻松编码规范模式生成规则。相对直观地将规范模式定义为时序逻辑和时间线片段——实例翻译为规则。有趣细微点：这些模板允许数据参数化事件。实验比较了生成实现与其他六个运行时验证和基于规则系统。
NASA寻求免费许可此软件并向开源项目公开。请联系NASA许可礼宾：This email address is being protected from spambots. You need JavaScript enabled to view it.，或致电202-358-7432启动许可讨论。
传感器