自动驾驶场景中存在着丰富的时空数据和动态行为交互,使得自动驾驶场景充满复杂性。系统的安全性面临着严重的挑战。近年来,人们尝试使用场景建模、仿真技术对自动驾驶场景的动态行为进行建模、分析,但自动驾驶场景的建模语言及支撑工具依然匮乏,同时也缺少使用形式化验证技术对模型进行验证分析。针对以上问题,本文提出一种面向汽车自动驾驶领域的场景建模语言（Scenario Modeling Language,SCML）,对驾驶场景中的动态行为进行抽象建模,构建系统的模型。此外,提出基于随机混成自动机网络（Network of Stochastic Hybrid Automata,NSHA）实现使用UPPAAL-SMC验证模型的安全性质。本文的主要工作包括:●提出一种面向汽车自动驾驶领域的场景建模语言SCML,能够构建驾驶场景的抽象模型。通过分析驾驶场景中的关键主体和状态变迁,抽象出驾驶场景动态行为的行为随机性、运动混成性等性质。基于标签迁移系统设计了SCML语言的形式化语法,基于模型驱动理论设计了SCML语言的元模型和图形化建模,最后按照进程代数的格式设计了SCML语言的形式化语义。●提出基于模型的转换方法,将SCML模型转换为随机混成自动机网络（NSHA）模型。基于元素转换和规则转换,给出了具体的模型转换规则和转换算法,最终实现使用验证引擎UPPAAL-SMC,验证驾驶场景SCML模型的安全性质。●实现了SCML模型构建和转换工具原型。基于SCML语言的元模型和图形化建模,设计工具原型的建模模块。利用模型的转换算法,将SCML模型文件转化成UPPAAL-SMC描述的NSHA模型文件,完成模型转换。●为了说明本文所提方法的有效性,使用两个经典场景案例:跟车场景和变道超车场景,分别给出了对应的SCML模型,并转化成NSHA模型,最后利用验证工具UPPAAL-SMC,使用统计模型检验算法对模型进行了验证分析。