面向自动驾驶安全性分析的形式化建模与验证研究

发布时间：2022-02-21 02:37

　　随着信息科学技术的快速发展,新型复杂系统如信息物理融合系统（Cyber-Physical System,CPS）逐渐融入人类社会生活。自动驾驶作为CPS经典应用场景,它根据驾驶环境的感知并通过计算做出相应驾驶决策,且具备自主性、安全性等特性。然而,复杂多变的城市交通驾驶场景、大量实时时空数据、驾驶环境中的固有不确定性等,都为确保自动驾驶的安全性带来挑战。本文采用形式化方法研究分析自动驾驶的安全性。形式化方法采用数学（逻辑）证明的手段对计算机系统进行建模、规约、分析、推理和验证。鉴于其严谨性,该方法已被广泛运用到系统安全性研究中。然而,采用形式化方法研究分析自动驾驶系统安全性仍存在诸多挑战。比如,目前时空约束大多基于微分方程建模,并不利于时空约束的抽象分析,需要提出时空逻辑支持规约和推理时空约束;对于自动驾驶环境中的状态空间爆炸问题,需要提出抽象模型以及对不确定性的建模方法;在此基础上,还需将验证系统安全问题转化为基于形式模型的判定问题,并验证安全性质。本文基于上述自动驾驶系统的特点,结合形式化方法,以自动驾驶系统安全评估为研究目标,研究了基于时空抽象模型的自动驾驶系统的形式化建模与验证... 

【文章来源】：华东师范大学上海市211工程院校985工程院校教育部直属院校

【文章页数】：132 页

【学位级别】：博士

【文章目录】：
摘要
abstract
第一章 绪论
    1.1 研究背景与动机
    1.2 自动驾驶系统安全评估的挑战
    1.3 研究现状与相关工作
    1.4 本文研究内容与主要贡献
    1.5 组织结构
第二章 基本概念和预备知识
    2.1 自动驾驶背景知识
    2.2 形式化方法
    2.3 本章小结
第三章 基于场景的自动驾驶系统抽象模型
    3.1 抽象模型结构
    3.2 观测信息的抽象模型
        3.2.1 自动驾驶场景
        3.2.2 静态观测信息
        3.2.3 动态观测信息
    3.3 场景和基本场景结构
        3.3.1 场景定义
        3.3.2 基本场景结构
    3.4 估算信息的抽象模型
        3.4.1 基于场景的估算模型
        3.4.2 随机驾驶决策的概率计算
    3.5 本章小结
第四章 时空逻辑
    4.1 驾驶场景中的时空约束
    4.2 有界多维模态逻辑
        4.2.1 有界多维模态逻辑语法
        4.2.2 空间拓扑结构
        4.2.3 有界多维模态逻辑语义
    4.3 BMML时空性质
    4.4 本章小结
第五章 基于抽象模型的验证方法
    5.1 模型检验框架
    5.2 抽象模型到随机混成自动机的映射
    5.3 性质描述语言的映射
    5.4 基于场景的安全评估框架
    5.5 基本场景结构中的安全评估
    5.6 本章小结
第六章 自动驾驶案例研究
    6.1 多车道环岛驾驶任务模型
        6.1.1 自动机Period
        6.1.2 自动机CarSelf
        6.1.3 自动机CarC2InTargetSeg
        6.1.4 自动机CarC1InKeySegs
    6.2 基于多车道环岛驾驶任务模型的自动化验证
    6.3 多车道环岛驾驶任务中安全责任的探讨研究
    6.4 场景满足多种系统需求的拓展分析
    6.5 本章小结
第七章 总结与展望
    7.1 论文总结
    7.2 下一步工作
参考文献
致谢
攻读博士学位期间发表论文和科研情况



本文编号：3636326