巴诺克

为什么，凭借你的真实，它们不能成为我的先知，并给我带来希望

巴诺克是使用Rust编写的信号时态逻辑（STL）的离线监控器。巴诺克这个名字来源于莎士比亚悲剧《麦克白》中的一个角色，他的角色是代替观众进行观察。

什么是时态逻辑？

时态逻辑是一种高阶逻辑，它允许对时间中的命题进行推理。这在形式验证中很有用，因为在形式验证中，人们希望确定系统的属性在一段时间内是否成立。除了支持一阶逻辑运算符外，时态逻辑还引入了以下时态运算符及其语义

什么是STL

信号时态逻辑（STL）是时态逻辑的一种扩展，它允许对 实时 和 实值 约束进行操作。这意味着，尽管基本时态逻辑只允许离散（整数）时间和真/假命题，但STL可以处理十进制的时间和状态。这使得我们可以对具有连续状态变量的系统表达约束——这对于评估现实世界系统非常有用。

信号时态逻辑还结合了度量时态逻辑（MTL），这是时态逻辑的一种扩展，它引入了对有界时态运算符的支持。只有与所有时间内的状态相关的运算符才是有界的。一个特殊情况是，当有界运算符用于蕴涵的右侧时——在这种情况下，右侧界限的时间0是左侧为真的时间。

这两个扩展使我们能够以紧凑和明确的方式表达系统需求，如下所示

$$ \Box ((gear=2 \wedge speed \geq 30) \rightarrow \diamond{0,4}\ gear=3) $$

在英语中，此公式表示安全要求：当汽车在二挡时速度超过每小时30英里，那么在接下来的4秒内，档位将切换到三挡。

您可以在此处了解更多有关时态逻辑的信息：这里。

什么是监控器？

一旦我们有系统的需求，我们希望能够分析我们的系统以确保它不违反需求。要做到这一点，我们必须生成一个系统 跟踪，它是一个包含每个时间点的系统和状态的集合。给定一个跟踪，我们评估每个时间点的公式，以确定系统是否违反了需求。这种评估类型称为 监控，可以离线进行（当整个跟踪可用时）或在线进行（当跟踪被评估时）。评估跟踪的结果是一个单一值，表示系统满足需求的成功或失败。直观上，我们可能期望评估的结果是一个布尔值，表示成功或失败，但我们可以定义其他结果值，这些值可以传达除仅满足之外的额外语义。

目前Banquo仅支持离线监控，但计划在将来支持在线监控。

Banquo可以进行哪些类型的评估？

Banquo支持以下监控语义

鲁棒性

鲁棒性是衡量系统接近违反需求程度的一个指标，或者在违反的情况下，衡量系统违反需求的程度。这表示为浮点值，负值表示需求违反。例如，给定需求 $\square x \leq 10$ 和跟踪

我们可以看到，跟踪最接近违反需求的时间是在时间 2.0，并且违反的距离是 0.9。

混合距离

具有离散和连续状态的系统可以表示为混合自动机（HA），其中系统的状态是由离散状态和连续状态组成的对。HAs还有 守卫，这些守卫根据系统的连续状态变量限制离散状态之间的转换。可以作为HA表示的系统的一个例子是交通信号灯，它有离散状态 ${GREEN, RED, YELLOW}$ 以及一个实值内部计时器，用于测量何时在离散状态之间切换。交通信号灯的守卫如下

给定一个混合自动机，我们可以编写关于系统连续状态的需求，但我们需要指定需求有效的离散状态。因此，并不总是可以衡量需求的鲁棒性，我们需要开发另一个指标以确保我们可以在每个时间提供有效的评估。解决这个问题的方法是引入混合距离，它可以计算公式的鲁棒性，或者计算可以计算鲁棒性的最近离散状态的距离。混合距离表示为对，其中第一个组件是到目标状态的最短路径距离，第二个组件是如果第一个组件为0，则为鲁棒性，如果第一个组件非零，则为最近转换守卫的距离。

扩展Banquo

班柯公式被定义为特性，并且此软件包提供的实现尽可能通用，以允许用户定义自己的运算符或表达式。表达式是公式的终端部分，它评估为传递回公式链的具体值。以下是一个创建新表达式的示例：

use std::collections::HashMap;

use std::error::Error;
use std::fmt;

use banquo::{Formula, Trace};

#[derive(Debug)]
struct PropositionError {
    name: String,
}

impl fmt::Display for PropositionError {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "Missing proposition {}", &self.name)
    }
}

struct Proposition {
    name: String,
}

impl Formula<HashMap<String, bool>> for Proposition {
    type Metric = f64;
    type Error = PropositionError;

    fn evaluate(&self, trace: &Trace<HashMap<String, bool>>) -> Result<Trace<Self::Metric>, Self::Error> {
        let mut result = Trace::new();

        for (time, state) in trace {
            let prop = state
                .get(&self.name)
                .copied()
                .ok_or_else(|| PropositionError { name: self.name.clone() })?;

            result.insert(time, if prop { f64::INFINITY } else { f64::NEG_INFINITY });
        }

        Ok(result)
    }
}

运算符会转换其子公式的输出，这些子公式可以是表达式或其他运算符。以下是一个创建新运算符的示例：

use banquo::{Bottom, Formula, Trace};

struct Prev<F> {
    subformula: F,
}

impl<F, S, M> Formula<S> for Prev<F>
where
    F: Formula<S, Metric = M>,
    M: Bottom + Clone,
{
    type Metric = M;
    type Error = F::Error;

    fn evaluate(&self, trace: &Trace<S>) -> Result<Trace<Self::Metric>, F::Error> {
        let evaluated = self.subformula.evaluate(trace)?;
        let mut iter = evaluated.into_iter().rev().peekable();
        let mut result = Trace::new();

        while let Some((time, _)) = iter.next() {
            let prev = iter
                .peek()
                .map(|(_, metric)| metric.clone())
                .unwrap_or(M::bottom());

            result.insert(time, prev);
        }

        Ok(result)
    }
}

虽然表达式和运算符都实现了相同的特性，但重要的是要注意它们有不同的含义。有关Formula特性或其语义的更多信息，请参阅docs.rs上的文档。

安装Banquo

可以使用以下命令将Banquo添加到您的项目中：cargo add banquo。这将向您的Cargo.toml文件中插入一行，包含此库的最新版本。

构建Banquo

Banquo的依赖项很少，应该可以在Cargo支持的几乎所有系统上构建。可以使用以下命令进行构建：cargo build。