Simulink中时间评估的规范和运行时验证

规范的形式化是实现复杂工程系统(如网络物理系统)严格系统设计的关键步骤。时间逻辑是捕获时间规范的一种合适的表达形式。然而，由于工程师和实践者通常不熟悉时态逻辑的符号和词汇，非正式的自然语言规范在实践中仍然大量使用。本文介绍了Simulink中的时间评估功能^®测试™，努力实现两个世界的最佳。它为用户提供了图形用户界面和可视化示例，使用户可以交互式地创建时间规范，而不需要手工编写逻辑公式，但是任何用户编写的时间评估都是内部表示中的有效逻辑公式。对子句的迭代折叠使规范的表述读起来像英语句子。本文还介绍了该特性的主要亮点，以及编写时态逻辑规范和运行时验证的示例。

这是作者的预印本。该论文发表在《2021年运行时验证国际会议论文集》上。最终认证版本可在网上查阅https://doi.org/10.1007/978-3-030-88494-9_17．

阅读全文。