结合关注事件的时间自动机语言包含模型检测

摘要：

时间自动机是实时系统形式化建模和验证的主要手段,能够对系统各个组件能否正确交互及通信进行验证.系统模型和待验证属性都用时间自动机表示,时间自动机语言包含模型检测方法能够验证系统模型是否满足带有时间要求的属性.目前相关工作中没有完善的能够应用于实际的语言包含检测方法,因为该方法要求系统模型和验证属性具有相同的事件集合,但在实际问题中,系统模型往往包含大量事件,而属性模型一般只关注少数的事件.因此,本文改进了已有的时间自动机语言包含算法,使其在运行时只需考虑关注事件,并总结了时间自动机描述的常用属性模式,以帮助用户更好地建模.此外,本文将该方法用于一个水位控制系统的建模和验证,得出了有效结论.

关键词：时间自动机、语言包含、模型检测、属性模式

所属期刊栏目：40

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金项目61602412, U1509214, 61772026

在线出版日期：2020-01-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：2578-2584