日志火
基于规则的系统对于运行时验证 (RV)/程序监控来说似乎很自然。从规范符号的角度来看，基于规则的系统似乎非常适合表达运行时验证社区通常编写的那种属性。写在规则系统中的规范具有操作性，根据不同的观点，可以将其视为劣势或优势。操作风格使规范比声明性时间逻辑或正则表达式更长；但是，他们很自然地写作。一旦掌握了核心思想，编写规则就很简单了，就像编程一样。更多的声明性规范可能更难正确。这种观察类似于以下观察：将非平凡属性表示为状态机可能比作为时序逻辑公式或正则表达式更容易。
JPL 的漫游车和航天器在运行时会产生遥测流。遥测流本质上是一系列事件，作为日志存储在持久内存中。任务操作需要自动检查这些日志是否正确。 LogFire 可用于检查这些日志。例如，LogFire 允许操作工程师自动确保流动站执行正确的步骤。
LogFire 读入一个日志文件并根据正式规范对其进行检查。规范可以用基于规则的语言来制定。基于规则的规范语言在 Scala 编程语言中作为 API 实现。这导致了一种非常强大的规范语言，因为它可以混合规则和传统编程。
由于 Scala 支持定义此类（内部）DSL，因此在 Scala 中将基于规则的语言定义为 API 具有 DSL（域特定语言）的外观。基于众所周知的 RETE 算法的规则引擎还增加了事件的概念，与规则引擎通常使用的长期事实相比，事件是瞬时的。最后，一种索引方法优化了引擎以处理携带数据的事件。
此外，LogFire 还允许对规范模式进行轻松编码以生成规则。将规范模式定义为时间逻辑和时间线的片段相对简单——其中的实例被转换为规则。一个有趣的细微差别是这些模板允许数据参数化事件。已经进行了实验，将最终实现与其他六个运行时验证和基于规则的系统进行了比较。
NASA 寻求免费许可该软件并使其可用于开源项目的一般用途。请通过以下方式联系 NASA 的许可礼宾部 此电子邮件地址已受到垃圾邮件机器人的保护。您需要启用 JavaScript 才能查看它。或致电 202-358-7432 与我们联系以发起许可讨论。
传感器