基于参数逻辑时间约束的不确定任务模型的形式化分析与验证

发布时间：2023-08-29 23:25

　　随着物联网和实时和嵌入式系统等相关技术在汽车、轨道交通、航空航天以及智能工厂等场景下的广泛使用,其复杂性和安全性等相关问题受到人们的广泛关注。它们需要经过严格的建模、分析和验证来保证系统的安全性和正常的工作性能。同时,对于大多数物联网设备和实时与嵌入式系统来说,它们工作环境总是大相径庭的,既有能在冬季零下五十摄氏度和夏季五十度情况下工作的汽车,也有在太空中受到极端辐射或者极端高低温的航天器。它们时时刻刻都需要面对着各种极端环境的考验,但任然需要满足正常的工作需求,因此它们需要经过严格的验证以保证工作的稳定性。然而,在不同的工作环境下,这些系统的运行速度通常是不同的,我们称之为执行时间的不确定性。例如,CPU在温度适中时运行速度是最快的。同时,对于一些周期性的时序行为,在完成设计之前,它们的周期可能是不确定的,称之为周期的不确定性。在实时和嵌入式系统中,电压的上升沿和下降沿被用来确定时钟周期,但当电压存在瞬时变化时,时钟周期可能会存在误差,这被归纳总结为周期漂移和周期抖动。上述的执行时间的不确定性、周期的不确定性、周期漂移和周期抖动这些不确定的时序行为广泛存在于各种实时和嵌入式系统中,它...

【文章页数】：95 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
第一章 绪论
    1.1 研究背景与意义
    1.2 国内外研究现状
    1.3 研究方法和内容
    1.4 论文结构
第二章 基础知识
    2.1 逻辑时间与时钟
    2.2 时钟约束语言
    2.3 SMT介绍及其API
    2.4 本章小结
第三章 不确定任务模型
    3.1 任务模型
    3.2 不确定的任务模型
    3.3 不确定的任务模型的调度
    3.4 一个简单的生产者和消费者的任务模型的例子
    3.5 本章小结
第四章 不确定任务模型转化为参数化的CCSL
    4.1 参数化的CCSL
    4.2 不确定任务模型的转化为参数化的CCSL
    4.3 不确定任务模型转化为CCSL约束的算法
    4.4 本章小结
第五章 基于SMT的调度解决方案
    5.1 把参数化的CCSL约束转化为SMT公式
    5.2 SMT公式量词消去
    5.3 量词消去方法的性能评估
    5.4 本章小结
第六章 不确定任务模型的案例研究
    6.1 研究案例1:一个简单的生产者消费者模型
    6.2 研究案例2:FMTV挑战
    6.3 性能评估
    6.4 本章小结
第七章 总结和展望
    7.1 论文总结
    7.2 工作展望
参考文献
致谢
发表论文和科研情况



本文编号：3844493