(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202211218805.4 (22)申请日 2022.10.07 (71)申请人 大连理工大 学 地址 116024 辽宁省大连市甘井 子区凌工 路2号 (72)发明人 王天一　段凯璐　孙景昊　魏屹芃　 段孝友　刘超　吴星宇　 (74)专利代理 机构 大连理工大 学专利中心 21200 专利代理师 温福雪 (51)Int.Cl. G06F 9/48(2006.01) G06F 9/50(2006.01) (54)发明名称 一种基于SMT的自动驾驶系统实时性任务调 度分析方法 (57)摘要 本发明涉及自动驾驶、 有向无环图等多个领 域， 特别涉及一种基于SMT的自动驾驶系统实时 性任务调度分析方法。 本发明利用运筹学领域的 可满足性模理论SMT给出了一种可系统计算一般 DAG精确的最坏情况下的响应时间的方法， 以分 析自动驾驶系统中任务调度的实时性分析方法。 权利要求书1页 说明书7页 附图4页 CN 115509712 A 2022.12.23 CN 115509712 A 1.一种基于SMT的自动驾驶系统实时性任务调度分析方法， 其特征在于， 包括以下步 骤： 步骤一： 确定自动驾驶系统的数据流图 自动驾驶系统 的数据流传递从传感器端开始， 从外界环境采集所需信 息并生成原始数 据， 这些原 始数据传递给系统中的下游组件， 由下游处 理组件进行处 理， 生成数据流图； 步骤二： 根据数据流图确定多频率DAG 多频率DAG用于模拟异构系统中以不同频率工作的硬件组件， 其中的节点代表具有不 同激活频率的任务， 每个任务以固定频率周期性地释放作业， 边代表任务之 间的数据传递； 多频率DAG表示为G＝(V,E)， 其中V表示图的节点集， V中的各个节点v1,...,vn代表不同硬件 组件的任务， E为每个节点间的边集， E中的各条边e1,...,em表示以边相连接的两个任务在 工作时存在数据传递关系， 边的起始端节点是 数据生产者， 边的接收端节点是 数据接收者； 步骤三： 确定不同节点所分布的计算资源平台 将图G的任务映射在一个异构系统上， 每个任务被静态地映射到相应的处理单元， 自动 驾驶异构系统由DSP、 GPU、 CPU三种处理器组成； 然后将节 点集V根据节 点所执行任务的功能 划分为三个不相交的子集{V1,V2,V3}， 其中， V1中的节点执行传感数据 处理相关的任务， 映 射到DSP上执行； V2中的节点执行感知和定位任务， 映射到GPU上执行； V3中的节点执行规划 和控制任务， 映射到 CPU上执行； 步骤四： 根据多频率DAG生成相应的单 频率DAG 将多频率DAG转换为单频率DAG， 以分析任务链的可调度性和端到端延迟； 转换过程的 输入是由多频率DAG所表示的任务集， 输出是等价的单频率DAG； 在多频率DAG中， 任务被建 模为节点， 两个任务之间的数据传递关系被建模为边； 所输出的单频率DAG， 每个任务释放 的作业实例被建模为节点， 不同作业之间的优先约束被建模为边， 其整体的调度周期等于 输入的任务集中各个任务周期的最小公倍数， 称之为超周期； 多 频率DAG在一个超周期之中 释放的所有作业都被显示在单 频率DAG中； 步骤五： 确定可 行调度应满足的时间约束条件 为确定自动驾驶系统 的实时性， 所要满足的主要时间限制包括： 反应时间限制、 数据新 鲜度、 时间戳差值、 时间戳计算、 非抢占式调度、 隐式的截止时间和互斥执 行； 步骤六： 使用SMT方法确定满足约束的从源节点到终止节点的作业链 单频率DAG中的节点代表不同组件执行的相应任务， 任务以不同的频率被执行， 每一次 执行的任务实例被称为作业； DAG中具有数据依赖关系的任务释放的作业所组成的作业序 列， 称为作业链； 以源节点为起始， 以终止节点为结束， 且满足步骤五所述的时间约束的作 业相互连接所组成的作业链， 即为所要寻找的满足约束的作业链； 使用SMT方法， 即可满足 性模理论方法来 寻找符合要求的作业链； 步骤七： 分析系统的实时性 根据步骤六的方法以及步骤五的约束条件， 确定一个自动驾驶系统的静态调度方法， 由此可计算出系统中最大作业链长度即为端到端延迟， 以此为依据分析 该系统的实时性。权　利　要　求　书 1/1 页 2 CN 115509712 A 2一种基于SMT的 自动驾驶系统实时性 任务调度分析方 法 技术领域 [0001]本发明涉及自动驾驶、 有向无环图等多个领域， 特别涉及一种基于SMT的自动驾驶 系统实时性任务调度分析 方法。 背景技术 [0002]随着人工智能的发展， 自动驾驶领域不可避免地会 成为未来汽车领域发展的大方 向。 在自动驾驶过程中， 一旦车辆遭遇突发事件， 车辆必须在极短的时间内完成预测， 处理 相关数据， 并在一段时间限制内生成控制命令 。 [0003]数据流图(Dataflow  graph)， 是一种以图的方式来表达系统的逻辑功能， 数据在 系统内部的逻辑流向和逻辑变换过程的结构化系统分析方法。 根据自动驾驶系统的数据流 图， 可以得到任务之间的依赖关系和每 个任务的周期， 方便对数据进行进一 步处理。 [0004]有向无环图(Directed  Acyclic Graph,DAG)是实时系统领域中表达性非常强的 模型， 是一种常见 的对并行程序建模的模型。 在自动驾驶的过程中， 往往涉及不同种类、 不 同复杂度、 相互关联的多种模型， 多模 型的调度方法直接影响产品运行的可行性和实时性。 多模型调度方法主要是利用DAG描述任务间的前驱后继关系， 在DAG中， 各个节点对应自动 驾驶系统中各组件的任务， 确 定DAG中各节点所被分配的计算资源平 台， 将多频率DAG转换 为单频率DAG， 确定该系统中可 行的调度所应满足的时间约束。 [0005]SMT的全称是Sat isfiability  Modulo Theories， 可被翻译为 “可满足性模理论 ”， “多理论下的可满足性问题 ”或者“特定(背景)理论下的可满足性问题 ”， 其判定算法被称为 SMT求解器。 SMT是SAT(satisfiability)问题， 即命题逻辑公式的可满足性问题的扩展， 它 能更好地表达一些人工智能和形式化方法领域内的问题,比如在资源规划、 时序推理、 编译 器优化等很多方面用到了S MT。 简单地说， 一个SMT公 式是结合了理论背 景的逻辑 公式， 其中 的命题变量可以代表理论 公式。 对于S MT的研究起源于20世纪70年代末80年代初， 当时的一 些学者为形式化方法设计了一些判定算法， 这些算法可以看作最早的S MT求解器； 到了20世 纪90年代， 人们开始研究能处理大规模工业界问题的SMT求解技术。 最近几年在工业界和学 术界， 这类技术均得到了迅猛的发展。 而SMT求解器也被集成到一些大型工具中， 比如HOL/ Isabelle、 ESC/Java2、 ACL2、 UCL ID、 BLAS、 ureka、 CU TE和PEX等。 发明内容 [0006]为了确保车辆能在极短的时间内完成预测、 处理相关数据， 并在一定时间限制内 生成控制 命令， 本发明利用运筹学领域的可满足性模理论(SMT)给出了一种可系统计算一 般DAG精确的最坏情况下的响应时间(WCRT)的方法， 以分析自动驾驶系统中任务调度的实 时性分析 方法。 [0007]本发明的技 术方案： [0008]一种基于SMT的自动驾驶系统实时性任务调度分析 方法， 包括以下步骤： [0009]步骤一： 确定自动驾驶系统的数据流图说　明　书 1/7 页 3 CN 115509712 A 3