-
公开(公告)号：CN118536860A
公开(公告)日：2024-08-23
申请号：CN202410608298.8
申请日：2024-05-16
申请人： 中科南京软件技术研究院 , 中国科学院软件研究所
IPC分类号： G06Q10/0639 , G06Q50/40 , G06N3/04 , G06N3/08 , G06F3/01
摘要： 本发明提供了一种基于人机交互的自动驾驶接管绩效预测方法及系统，涉及自动驾驶测试领域。该方法针对自动驾驶接管人机交互数据采集，在仿真器中设计多种不同的交通场景，并在不同交通场景下采集接管时的车辆与驾驶员数据，丰富了接管发生的交通场景，使得后续由这些数据建立的预测模型能够更好的适应不同交通场景，得到更准确的预测结果。针对接管绩效预测，构建了新的深度神经网络模型结构，包含场景特征处理、人机特征处理两个子网络，提高接管绩效预测的准确性。综合多个角度的单一的接管绩效指标，设计综合性的接管绩效评价综合类别，提高了接管绩效类别的有效性，使得对接管绩效的预测分类结果更加具有综合性。
-
公开(公告)号：CN116701085B
公开(公告)日：2024-03-19
申请号：CN202310648072.6
申请日：2023-06-02
申请人： 中国科学院软件研究所
摘要： 本发明提供一种RISC‑V处理器Chisel设计指令集一致性的形式验证方法及装置，所述方法包括：在待验证处理器中引出该待验证处理器的输入信号和第一执行结果；将输入信号传递给指令集参考模型，以得到第二执行结果；将第一执行结果与第二执行结果一致作为待验证性质，并生成指令的验证范围约束；将包含参考模型、待验证性质和验证范围约束的待验证处理器转换为FIRRTL中间表示，并依据FIRRTL中间表示，得到迁移系统；基于迁移系统及其包含的性质和约束，得到待验证处理器的验证结果。本发明通过一个模块化、与原文对应、可参数化配置的参考模型描述RISC‑V指令集规范的行为，减轻了验证人员对形式化验证知识的需求，无需人工编写待验证的性质。
-
公开(公告)号：CN116701085A
公开(公告)日：2023-09-05
申请号：CN202310648072.6
申请日：2023-06-02
申请人： 中国科学院软件研究所
摘要： 本发明提供一种RISC‑V处理器Chisel设计指令集一致性的形式验证方法及装置，所述方法包括：在待验证处理器中引出该待验证处理器的输入信号和第一执行结果；将输入信号传递给指令集参考模型，以得到第二执行结果；将第一执行结果与第二执行结果一致作为待验证性质，并生成指令的验证范围约束；将包含参考模型、待验证性质和验证范围约束的待验证处理器转换为FIRRTL中间表示，并依据FIRRTL中间表示，得到迁移系统；基于迁移系统及其包含的性质和约束，得到待验证处理器的验证结果。本发明通过一个模块化、与原文对应、可参数化配置的参考模型描述RISC‑V指令集规范的行为，减轻了验证人员对形式化验证知识的需求，无需人工编写待验证的性质。
-
公开(公告)号：CN115496017A
公开(公告)日：2022-12-20
申请号：CN202211084241.X
申请日：2022-09-06
申请人： 中国科学院软件研究所
IPC分类号： G06F30/33 , G06F8/41 , G06F119/02
摘要： 本发明公开了一种Chisel断言语言的类SVA扩展及形式化验证方法，其步骤包括：1)将SVA支持的若干算子引入Chisel断言语言中，得到断言语言中对应的扩展算子；2)接收用户编写的算子序列；3)将Chisel硬件设计代码编译成FIRRTL，并利用FIRRTL生成设计代码的迁移系统；4)在FIRRTL层次生成相应的Büchi自动机；5)将结构调整后的自动机翻译到FIRRTL的迁移系统上，得到断言转换后的迁移系统；6)将转换后的迁移系统与硬件设计对应的迁移系统做同步得到一全局迁移系统；7)根据全局迁移系统生成btor2文件；8)对btor2文件进行模型检测，完成对断言所描述性质的形式化验证。
-
公开(公告)号：CN118428285B
公开(公告)日：2024-10-22
申请号：CN202410462685.5
申请日：2024-04-17
申请人： 中国科学院软件研究所
摘要： 本发明提出了一种Chisel高层电路设计的转换和验证方法及装置，涉及计算机技术领域，通过分析Chisel代码内容，生成内部语法树结构；分析内部语法树上的每个语句和语句块，识别涉及的信号和变量；基于识别的信号、变量和内部语法树结构，对内部语法树进行展开和变换；对经过展开和变换后的内部语法树，按照信号和变量间的依赖关系进行语句排序，生成排序后的内部语法树；根据排序后的内部语法树，通过软件建模模拟Chisel电路设计的行为，生成Scala模拟代码；使用生成的Scala模拟代码进行仿真测试和形式化验证。本发明可以保留Chisel高层电路设计的参数、结构信息，对Chisel电路设计进行更充分的验证。
-
公开(公告)号：CN117762816A
公开(公告)日：2024-03-26
申请号：CN202410024407.1
申请日：2024-01-08
申请人： 中科南京软件技术研究院 , 中国科学院软件研究所
IPC分类号： G06F11/36 , G06N3/084 , G06N3/0985
摘要： 本发明提供了一种自动驾驶系统仿真测试方法、系统、设备及存储介质，方法包括：确定场景参数与安全性指标；对场景参数进行随机采样，形成多组参数数值组合；将参数数值组合导入驾驶仿真器执行一次行驶任务，采集得到安全性指标；建立神经网络模型，用采集到的数据对神经网络模型进行训练；将形成的多组参数数值组合输入到训练后的模型中，输出近似的安全性指标，检验其是否满足安全要求：若不满足，则将其所属的参数数值组合作为潜在反例，放回驾驶仿真器中得到新的安全性指标，检验新的安全性指标是否满足安全要求：若不满足，则发现一个导致系统出现不安全行为的场景参数数值组合，输出告知测试者。该方法可以提高测试过程的效率。
-
公开(公告)号：CN116224834A
公开(公告)日：2023-06-06
申请号：CN202310392960.6
申请日：2023-04-13
申请人： 中国科学院软件研究所
IPC分类号： G05B17/02
摘要： 本发明提出一种基于Carla平台的仿真驾驶方法和系统。该方法主要包括：将三块显示屏拼接在一起，将服务器与三块显示屏连接，配置三块显示屏使其能够跨越显示画面；运行Carla模拟器并展示在Carla平台中的实时仿真驾驶画面，调试显示屏至能够通过第一视角展示模拟画面；在服务器上连接罗技方向盘，将罗技方向盘、刹车踏板装载在仿真座椅上，使用罗技方向盘进行模拟驾驶，运行python脚本使得方向盘能够操纵Carla中的模拟车辆；确定行驶过程的地图，设置当前模拟世界的参数，选择自动驾驶相关场景；在选定的地图场景中操纵模拟车辆在其中行驶，记录下产生碰撞的相关数据。本发明能进解决现有技术中仿真驾驶系统不完善、覆盖自动驾驶场景不足的问题。
-
公开(公告)号：CN114637664A
公开(公告)日：2022-06-17
申请号：CN202111171245.7
申请日：2021-10-08
申请人： 中国科学院软件研究所
IPC分类号： G06F11/36
摘要： 本发明公开了一种针对安卓应用程序性质的检测方法及装置，包括针对不同安卓设备中的每一应用程序，基于Activity信息及Activity之间的跳转信息构建状态图，并将各状态图作为智能体进行组合，得到概率多智能体系统；将目标性质刻画为概率认知逻辑公式；将概率多智能体系统及概率认知逻辑公式，输入模型检测工具，获取目标性质的检测结果。本发明能够证明性质被满足或者给出不被满足的反例，能够建模同一安卓应用运行在不同设备上的情况下的系统，验证与不同设备上运行的安卓应用之间的交互相关的性质；可以分析在多个设备上运行的安卓应用程序组成的系统的性质，对开发者调试程序，提高程序易用性、减少程序漏洞具有积极意义。
-
公开(公告)号：CN117075969B
公开(公告)日：2024-07-23
申请号：CN202311088711.4
申请日：2023-08-28
申请人： 中国科学院软件研究所
IPC分类号： G06F9/38 , G06F9/30 , G06F12/1009
摘要： 本发明公开了一种面向RISC‑V处理器特权指令集一致性的形式验证方法及装置，所述方法包括：在Chisel设计的待验证处理器中引出指令信号、通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号到信号同步模块；将指令信号作为特权指令集参考模型执行的指令输入，并将通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号与特权指令集参考模型的执行结果是否一致设为待验证性质；将特权指令集参考模型、待验证处理器、信号同步模块与待验证性质共同转换迁移系统模型；基于迁移系统模型，交由模型检测算法进行求解，得到待验证处理器的验证结果。本发明可以对RISC‑V特权指令集进行一致性验证。
-
公开(公告)号：CN117075969A
公开(公告)日：2023-11-17
申请号：CN202311088711.4
申请日：2023-08-28
申请人： 中国科学院软件研究所
IPC分类号： G06F9/38 , G06F9/30 , G06F12/1009
摘要： 本发明公开了一种面向RISC‑V处理器特权指令集一致性的形式验证方法及装置，所述方法包括：在Chisel设计的待验证处理器中引出指令信号、通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号到信号同步模块；将指令信号作为特权指令集参考模型执行的指令输入，并将通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号与特权指令集参考模型的执行结果是否一致设为待验证性质；将特权指令集参考模型、待验证处理器、信号同步模块与待验证性质共同转换迁移系统模型；基于迁移系统模型，交由模型检测算法进行求解，得到待验证处理器的验证结果。本发明可以对RISC‑V特权指令集进行一致性验证。
-
-
-
-
-
-
-
-
-
搜索结果
18 条记录 (耗时 0.04 秒)
