telo - 在Rust中指定时间属性

使用telo，您可以使用线性时序逻辑（LTL）指定时间属性。这些规范可以转换为监控自动机，可以在运行时检测安全性规范的违反。

如何：运行时监控

use telo::{*, predicate::*, monitor::*};

// Step 1: define predicates
const LIMIT: i32 = 123;

let mut builder = Predicates::builder();
let above_limit = builder.new_predicate(ClosurePredicate::new(
    |val: &i32| *val >= LIMIT,
     "value is above LIMIT",
));
let predicates = builder.build();

// Step 2: define temporal specification
let property = Property::never(Property::atomic(above_limit));

// Step 3: transform to monitoring automaton
let automaton = property.to_monitoring_automaton(&predicates);

// Step 4: runtime monitoring
let mut monitor = Monitor::new(predicates, automaton);
for value in 0..LIMIT {
  assert!(monitor.next_state(&value));
}
assert!(!monitor.next_state(&LIMIT)); // the property is violated

从LTL到最小化和确定性的安全自动机

• 使用自定义谓词的任意域上的LTL
• 转换为否定范式下的LTL
• 转换为交替时间Büchi自动机
• 通过Miyano-Hayashi构造转换为非确定性Büchi自动机
• 作为非确定性安全自动机重新解释
• 确定化和最小化安全自动机

许可证

根据您的选择，许可方式为以下之一

• Apache许可证，版本2.0 (LICENSE-APACHE 或 http://www.apache.org/licenses/LICENSE-2.0)
• MIT许可证 (LICENSE-MIT 或 http://opensource.org/licenses/MIT)

。

贡献

除非您明确声明，否则根据Apache-2.0许可证定义的，您提交给作品的所有贡献将根据上述方式双重许可，不附加任何额外条款或条件。