规范和运行时验证模型的时间评估万博1manbetx

形式化的规范是一个关键的一步严格系统设计复杂的工程系统,如网络物理系统。时序逻辑是一个适合捕捉时间规范的表达形式。然而,由于工程师和专业人员往往不熟悉时序逻辑的符号和词汇,非正式的自然语言规范仍然在实践中大量使用。这个工具提出了时间评估特性仿真软件万博1manbetx^®测试™,力求达到两全其美。它为用户提供了图形用户界面和可视化例子交互式地创建时间规范而不需要作者逻辑公式,然而任何user-authored时间评估是一个有效的逻辑公式的内部表示。迭代折叠的条款使规范提交读英语句子。关键的特性以及时序逻辑规范的编写和运行时验证的例子。

这是作者的预印本。这篇论文发表在国际会议的程序运行时验证(RV) 2021。最后经过身份验证的版本网上。

阅读论文全文。