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

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

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

阅读全文。