telo - Specifying temporal properties in Rust
With telo, you can specify temporal properties using linear-time temporal logic (LTL). Those specifications can be transformed into monitoring automata, which can detect violations of safety specifications during runtime.
How-to: Runtime monitoring
use ;
// Step 1: define predicates
const LIMIT: i32 = 123;
let mut builder = builder;
let above_limit = builder.new_predicate;
let predicates = builder.build;
// Step 2: define temporal specification
let property = never;
// Step 3: transform to monitoring automaton
let automaton = property.to_monitoring_automaton;
// Step 4: runtime monitoring
let mut monitor = new;
for value in 0..LIMIT
assert!; // the property is violated
From LTL to minimal and deterministic safety automata
- LTL over an arbitrary domain using self-defined predicates
- Translation to LTL in negation normal form
- Translation to alternating-time Büchi automaton
- Translation to non-deterministic Büchi automaton (via Miyano-Hayashi construction)
- Re-interpretation as non-deterministic safety automaton
- Determinize and minimize safety automaton
License
Licensed under either of
- Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
Contribution
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.