Crate banquo

source ·
Expand description

Why, by the verities on thee made good, may they not be my oracles as well, and set me up in hope

Banquo is an offline monitor for Signal Temporal Logic (STL). The name Banquo comes from a character in Shakespeare’s tragedy MacBeth who’s role is to observe in place of the audience.

This library provides expressions and operators to create temporal logic Formulas to evaluate timed sequences of system states called Traces. Temporal logic formulas are a system for the evaluation of logical propositions over time are are useful for evaluating the behaviors of complex systems over time. Behavioral requirements can be something as simple as The aircraft altitude should always be greater than zero or something more complex like The vehicle should always brake within 3 seconds if a pedestrian is detected inside of a 60 degree cone of the front of the vehicle. To determine if a system violates a behavioral requirement, we can provide a set of system states along with the times each state was recorded called a Trace, which the formula can evaluate into a metric value. This process is called monitoring, making Banquo a temporal logic monitor. The computed metric value is useful because it can not only indicate if the requirement was satisfied, it can also provide a measure of distance of the system from a violation. This enables the use of search-based testing techniques to find examples of violating inputs by trying to minimize the distance from violation. The most common type of metric value for evaluating formulas is called robustness, which is a real number representing the distance of the system state from the polytope representing the set of states that violate the requirement.

As an example, consider the automatic transmission system in a car. We might create the following requirement when testing the vehicle:

[] ((gear = 3 /\ rpm >= 4000) -> <>[0,3] gear = 4)

This formula reads At every time, if the gear is equal to 3 and the rpm is greater than or equal to 4000, then within the next 3 time-steps the gear should be equal to 4. With a requirement like this, we could attempt to find some combination of system inputs in which the system does not behave properly.

§Examples

A formula is constructed by combining expressions (like a Predicate), which evaluate states into metric values, and operators, which manipulate metric values. An example formula might look as follows:

use banquo::predicate;
use banquo::operators::{Always, Not, Or};

let p1 = predicate!{ x <= 10.0 };// Expression
let p2 = predicate!{ y <= 3.0 }; // Expression

let formula = Always::unbounded(Or::new(p1, Not::new(p2)));  // Operators

In order to evaluate a formula you must provide a Trace, which is a set of value where each value has an associated time. A trace is constructed like so:

use banquo::Trace;

let mut t1 = Trace::new();
t1.insert(0.0, 99);
t1.insert(1.0, 100);
t1.insert(2.0, 107);
t1.insert(3.0, 111);
t1.insert(4.0, 115);

let t2 = Trace::from([
    (0.0, 99),
    (1.0, 100),
    (2.0, 107),
    (3.0, 111),
    (4.0, 115),
]);

Given a Trace, the formula can be evaluated using the Formula::evaluate method into a Result containing either a Trace of metric values, or an error.

use std::collections::HashMap;

use banquo::{Formula, Trace, predicate};
use banquo::operators::Always;

// A predicate can only evaluate a named variable set, so we define a helper function to create
// hash maps for a single variable instead of repeating ourselves.
fn state(value: f64) -> HashMap<&'static str, f64> {
    HashMap::from([("x", value)])
}

let trace = Trace::from([
    (0.0, state(99.0)),
    (1.0, state(100.0)),
    (2.0, state(107.0)),
    (3.0, state(111.0)),
    (4.0, state(115.0)),
]);

let phi = Always::unbounded(predicate!{ x <= 110.0 });
let result: Result<Trace<f64>, _> = phi.evaluate(&trace);

Formulas can also be evaluated using the evaluate function, which returns the first metric in the output trace on successful evaluation.

use std::collections::HashMap;

use banquo::{EvaluationError, Trace, evaluate, predicate};
use banquo::operators::Always;

// A predicate can only evaluate a named variable set, so we define a helper function to create
// hash maps for a single variable instead of repeating ourselves.
fn state(value: f64) -> HashMap<&'static str, f64> {
    HashMap::from([("x", value)])
}

let trace = Trace::from([
    (0.0, state(99.0)),
    (1.0, state(100.0)),
    (2.0, state(107.0)),
    (3.0, state(111.0)),
    (4.0, state(115.0)),
]);

let phi = Always::unbounded(predicate!{ x <= 110.0 });
let result: Result<f64, EvaluationError> = evaluate(&trace, &phi);

Modules§

  • operators
    Combinatorial operators for constructing formulas.
  • predicate
    System requirements expressed as the inequality ax≤ b.
  • trace
    A set of values where each value is associated with a time.

Macros§

Structs§

  • EvaluationError
    Error produced while evaluating a Trace using the evaluate function.
  • Predicate
    System requirements expressed as the inequality ax≤ b.
  • Trace
    A set of values where each value is associated with a time.

Traits§

  • Bottom
    Trait representing a type with a global minimum.
  • Formula
    Trait representing a temporal logic formula that can evaluate a timed set of system states called a Trace.
  • Join
    Trait representing a type that can compute the supremum of two values.
  • Meet
    Trait representing a type that can compute the infimum of two values.
  • Top
    Trait representing a type with a global maximum.

Functions§