可检测实时系统的正确性的符号化模型

资料大小: 2.39 MB

所需积分: 0

下载次数:

用户评论: 0条评论,查看

上传日期: 2021-05-07

上 传 者: 他上传的所有资料

资料介绍

标签:离散(31)模型(921)算法(2654)

  实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提岀一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑( Real-TIme linearυ ynamic logic, RTLDL);然后使用类似程序控制流标记的方法为 RTLDI·公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的 RTLDI符号化模型检测算法;最后基于翻译的方法在模型检测器NuⅩmν上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑( Inearυyaπ ic logic,LDL)模型检测器MCMASLDLK进行实验比较。实验结果表明,无论对于IDL还是 RTLDI公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。

用户评论

查看全部 条评论

发表评论请先 , 还没有账号?免费注册

发表评论

用户评论
技术交流、我要发言! 发表评论可获取积分! 请遵守相关规定。
上传电子资料