模型网络测速工具
网络测速工具 时间:2021-05-20 阅读:()
软件学报ISSN10009825,CODENRUXUEWJournalofSoftware,[doi:10.
13328/j.
cnki.
jos.
006272]中国科学院软件研究所版权所有.
不确定环境下人机物融合系统的形式化安冬冬1,刘静2,陈小红2,孙海英21(上海师范大学信息与机电工程学院,上海200234)2(华东师范大学软件工程学院,上海200062)通讯作者:刘静,Email:jliu@sei.
ecnu.
edu.
cn摘要:随着科技的进步,新型复杂系统例如人机物融合系统人类社会生活越来越密不可分.
软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决能、安全的人机物融合系统已经成为软件行业不可回避的挑战确感知其所处的运行环境.
感知的不确定性将导致系统的误判设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约形式化规约是保证系统安全的首要条件.
为了应对规约的不确定性的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模动态验证的方式保证系统的安全,从而构建统一安全的理论框架与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用关键词:人机物融合系统;机器学习;不确定性建模;形式化验证中图法分类号:TP311中文引用格式:安冬冬,刘静,陈小红,孙海英.
不确定环境下人机物融合系统的http://www.
jos.
org.
cn/10009825/6272.
htm英文引用格式:AnDD,LiuJ,ChenXH,SunHY.
Formalmodelingandunderuncertainenvironment.
RuanJianXueBao/JournalofSoftware,206272.
htmFormalModelingandDynamicVerificationforHumanCyberPhysicalSystemsunderUncertainEnvironmentANDongDong1,LIUJing2,CHENXiaoHong2,SUN1(TheCollegeofInformation,MechanicalandElectricalEngineering2(ShanghaiKeyLaboratoryofTrustworthyComputing,EastChinaNormalAbstract:Withthedevelopmentoftechnology,newcomplexsystemssuchasHumanCyberindistinguishablefromsociallife.
Thecyberspacewherethesoftwaresystemlocatedpeople'sdailylife.
Theuncertainfactorssuchasthedynamicspatiotemporaldataaswellastheunpredictablehumanbehaviorincreasingsecurityrequirements,thescaleandcomplexityofthesystemaretaatremainunresolved.
Therefore,developingintelligentandsafehumancyberbecomingtheinevitablechallengeforthesoftwareindustry.
Itisdifficultforthehumancyber基金项目:国家重点研发计划项目(2019YFA0706404);国家自然科学基金技计划项目(20ZR1416000)收稿时间:20200917;修改时间:20201026;采用时间:2020Email:jos@iscas.
ac.
cnhttp://www.
jos.
org.
cnTel:+861062562563形式化建模与动态验证新型复杂系统例如人机物融合系统(HumanCyberPhysicalSystems,HCPS)已经与软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.
物理空间时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.
由于系统安系统的规模和复杂度随之增加所带来的一系列问题亟待解决.
因此,在不确定性环境下,构造智安全的人机物融合系统已经成为软件行业不可回避的挑战.
环境不确定性使得人机物融合系统软件无法准感知的不确定性将导致系统的误判,从而影响系统的安全性.
环境不确定性使得系统合系统软件的运行环境提供准确的形式化规约.
而对于安全要求较高的系统,准确的为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合基于环境中时空数据对环境进行建模.
根据安全软件的典型特征,采用从而构建统一安全的理论框架.
为了展示方案的可行性,本文以自动驾驶车辆的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.
形式化验证;统计模型检测不确定环境下人机物融合系统的形式化建模与动态验证.
软件学报.
odelinganddynamicverificationforhumancyberphysicalsystemsJournalofSoftware,2021(inChinese).
http://www.
jos.
org.
cn/10009825/FormalModelingandDynamicVerificationforHumanCyberPhysicalSystemsunderHaiYing2TheCollegeofInformation,MechanicalandElectricalEngineering,ShanghaiNormalUniversity,Shanghai200234,China),EastChinaNormalUniversity,Shanghai200062,China)oftechnology,newcomplexsystemssuchasHumanCyberPhysicalSystems(HCPS)havebecomespacewherethesoftwaresystemlocatedisincreasinglyintegratedwiththephysicalspaceofdynamicenvironmentinthephysicalspace,theexplosivegrowthoftheunpredictablehumanbehaviorareallcompromisethesecurityofthesystem.
Asaresultofthethescaleandcomplexityofthesystemarealsoincreaseing.
ThissituationleadstoaseriesofproblemsTherefore,developingintelligentandsafehumancyberphysicalsystemsunderuncertainenvironmentistisdifficultforthehumancyberphysicalsystemstoperceivetheruntime国家自然科学基金(61972150);上海市知识服务平台(ZF1213);上海市科:20201214;jos在线出版时间:202101222JournalofSoftware软件学报environmentaccuratelyunderuncertainsurroundings.
Theuncertainperceptionwillleadtothesystem'smisinterpretation,thusaffectingthesecurityofthesystem.
Itisdifficultforthesystemdesignerstoconstructformalspecificationsforthehumancyberphysicalsystemsunderuncertainenvironment.
Forsafetycriticalsystems,formalspecificationsaretheprerequisitestoensuresystemsecurity.
Tocopewiththeuncertaintyofthespecifications,weproposeacombinationofdatadrivenandmodeldrivenmodelingmethodology,thatis,weusethemachinelearningbasedalgorithmstomodeltheenvironmentbasedonspatiotemporaldata.
Weintroduceanapproachtointegratemachinelearningmethodandruntimeverificationtechnologyasaunifiedframeworktoensurethesafetyofthehumancyberphysicalsystems.
Weillustrateourapproachbymodelingandanalyzingascenariooftheinteractionofanautonomousvehicleandahumandrivenmotorbike.
Keywords:humancyberphysicalsystem;machinelearning;uncertaintymodeling;formalverification;statisticalmodelchecking随着计算机科学技术的发展,各种新型复杂系统快速涌现,尤其是与人类社会交互和协作的复杂系统越来越受到人们的关注.
信息物理融合系统(CyberPhysicalSystems,CPS)是一种综合计算、网络和物理环境的多维复杂系统,通过3C技术,即计算(Computation)、通信(Communication)和控制(Control)的有机融合与深度协作,实现大型工程系统的实时感知、动态控制和信息服务[1].
CPS系统的本质就是以"人机物"的融合为目标的计算技术,以实现人的控制在时间、空间等方面的延伸.
人机物融合系统(HumanCyberPhysicalSystems,HCPS)是具有深度集成的人、网络和物理元素的智能联网系统[2],是在信息物理系统CPS的基础上,重点考虑系统所处的不确定环境以及环境中人的因素.
例如与驾驶员和行人交互的自动驾驶系统,与医生合作的智慧医疗系统以及与用户互动的智能家居系统等.
作为人机物系统的核心,HCPS软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.
作为人机物融合系统主体的智能体(Agent)在与所处的环境(Environment)不断进行交互的过程中,智能体需要要像人一样具有学习能力,拥有"智能性"来应对各种环境.
"智能性"主要指计算智能,是以数据为基础,通过训练建立联系进行问题求解,人工神经网络、遗传算法、模糊系统、进化程序设计等都属于计算智能.
由于环境与过程的时空特性,HCPS系统行为的响应不仅与所经历的时间有关,同时也和所处的空间相关,具体表现为计算过程要求严格的时间约束,而物理过程具有空间依赖性.
同样,随着万物互联的发展,人成为HCPS系统中的重要组成部分.
由于许多HCPS都发挥着至关重要的作用(例如在能源、医疗保健、国防安全、智能驾驶等方面),因此这些系统的"安全性"也同样至关重要.
"安全性"是系统所在环境的函数,是对任何环境下系统零风险程度的度量[3].
Sun等人[4]指出"确保软件的安全性是指在任何环境中各种软件的运行不会导致系统出现不可预测的风险,具有避免灾难事故发生的能力".
物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统的安全性.
智能体如何准确感知并捕获不确定环境中的有效信息并及时做出准确且安全地决策是目前研究人员重点关注的问题.
由于人机物融合系统所涉及的研究系统比较广泛,不同系统所涉及的人的因素各不相同,本文中我们以无人驾驶系统作为人机物融合系统的典型案例进行分析和研究.
无人驾驶是典型的HCPS应用领域,未来将是人机共驾、有人无人驾驶车辆共存的局面.
在这样的混合交通场景中,无人驾驶车辆作为智能体不可避免地需要与所处环境中的其他车辆以及车辆内部和外部的人进行交互[5].
这对无人驾驶系统的设计提出了更高的要求,一方面,系统需要有应对环境的"智能性",拥有迅速准确的决策能力,可以自主应对驾驶过程中常常遇到的、偶发的各种各样的不确定性事件.
我们知道,人类驾驶员在突发事件情况下,会因为情绪失控而导致不理性决策产生.
对于人来说,这类事故是小概率事件,因而很难通过对事故的"练习"来帮助驾驶员积累处理经验.
而机器学习(MachineLearning,ML)技术可以帮助自动驾驶系统应用所感知到的时空数据进行及时有效地计算,从而分析周边环境来产生决策.
因而无人驾驶系统可以在事故发生时,精准理性地应对,从而最大限度地减少事故的发生.
机器学习可以帮助提高系统的"智能性",但是并不能保证系统的"安全性".
数据驱动的方式可能会由于某个数据的变化导致学习出的结果是错误的,从而产生无法预料的后果,这对安全的系统是不可接受的[6][7][8].
该方案显示出了对于数据的敏感性,由于机器学习算法本身可解释性较差的缺点导致系统无法预知所学习的结果.
所以仅仅依靠机器学习的方法无法保证无人驾驶系统的安全性.
目前无人驾驶由于安全问题的不断出现仍然面临巨大挑战.
2016年,一辆特斯拉的汽车由于传感器失灵而没有及时感知前方的障碍物而与之发生碰撞安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证3[9].
2018年,Uber的无人驾驶车由于夜间识别能力较差没有及时感知到前方的行人进行避让而发生车祸事故,导致行人的死亡[10].
城市交通环境日趋复杂,面对自动驾驶场景复杂多变、时空数据的爆发以及其他人工驾驶车辆的主观驾驶行为所导致了环境中不确定性的增加,如何避免事故的产生,来保证系统的"安全性"仍是目前的研究难点.
随着HCPS的应用空间的增长,开发具有安全保证的设计框架至关重要.
在对HCPS建模过程中,需要重点考虑HCPS动态行为的三个特性:(1)混成性:HCPS依赖行为离散的计算系统,同时也依赖行为连续的物理环境(例如:连续的温度变化、时间及空间的变化等),其异构的本质导致其行为具有混成性;(2)随机性:HCPS系统处在开放的环境中,不确定的环境(例如:环境中人的行为不确定、用户的行为不确定以及天气的变化等),造成HCPS的行为具有随机性;(3)安全性:HCPS经常被用于安全攸关的系统(例如:智慧医疗系统、列车控制系统和智能驾驶系等),所以需保证HCPS的行为必须是安全可信的.
形式化方法(FormalMethod,FM)是基于严谨的数学(逻辑)语言和精确的数学语义的方法学,主要应用于对系统软件进行建模分析和验证等工作,保证系统的正确运行[11].
面对系统规模的增长和复杂度的增加,形式化方法越来越频繁地被应用于安全攸关软件的验证,以此来保证其安全性[12][13].
模型检测(ModelChecking,MC)是通过对系统的状态空间进行全遍历,从而对系统的安全性进行自动验证[14],其本质思路是将一个过程或系统抽象成一个有穷状态机模型加以分析验证.
传统的模型检测由于状态爆炸的问题,增大了对系统进行分析验证的难度.
统计模型检测技术(StatisticalModelChecking,SMC)[15]可以通过评估系统所满足的概率区间对系统进行定量分析,从而有效解决状态过多而难以验证的问题[16][17][18].
统计模型检测是一种高效的验证技术,常用于复杂的随机系统的验证.
该工具所采用的技术主要是参数估计式和假设检验.
其中,参数估计是基于所收集到足够的样本,给出模型满足给定性质的近似概率,属于定量的结果;而假设检验是基于样本给出模型是否满足给定的性质,属于定性的结果.
本文主要考虑人类驾驶车辆和自动驾驶车辆共存的混合交通流下的驾驶环境,由于人的行为以及物理环境导致不确定性因素的增加.
而UPPAALSMC具有定性和定量分析的能力,能够分析验证出自动驾驶车辆的相对安全性,因此,本文选用UPPAALSMC作为自动验证工具.
本文采用时空数据驱动的方法来处理环境的不确定性,针对安全攸关HCPS建模与验证缺乏统一系统的理论、方法.
围绕"不确定环境下的人机物融合系统的建模与验证"关键科学问题,提出了以数据驱动和模型驱动相结合的创新方式构建不确定环境下的HCPS,并对其关键支撑技术进行创新性研究.
(1)针对系统所处的物理环境的不确定性,应用机器学习技术,以环境中的时空数据为驱动,环境感知计算为切入点,提出了不确定环境下的基于朴素贝叶斯的人类行为分类模型.
(2)为了应对大规模系统的结构化建模,构建了不确定环境场景下的HCPS系统模型,使用验证工具UPPAALSMC实现对模型的动态验证.
(3)提出基于统计模型验证的运行时动态验证技术,采取线下和线上验证相结合的方法,即通过比较参数即可快速得出验证结果,从而达到动态实时的验证效果,进而保障系统在复杂环境中安全运行.
本文以构建安全智能的人机物融合系统的理论框架及应用作为主要的研究目标.
第1节主要介绍所涉及的一些背景知识,包括其概念及其主要应用.
第2节介绍了不确定环境下的感知模型,针对系统所处的物理环境的不确定性,应用机器学习算法,以环境的时空数据为驱动,提出了不确定环境下的基于朴素贝叶斯的人类驾驶行为分类模型.
第3节提出了线下与线上验证相结合的动态验证方法即通过验证工具UPPAALSMC实现对模型的动态验证,从而定量评估不确定性环境以及人的行为对系统安全性的影响.
第4节对相关工作进行了比较,最后总结全文,并对未来值得关注的研究方向进行初步探讨.
4JournalofSoftware软件学报1预备知识1.
1朴素贝叶斯算法朴素贝叶斯或简单贝叶斯分类器广泛应用于数据分析.
朴素贝叶斯分类器[19],基于关键的约束假设,即属性之间彼此独立,也就是类别|特征1,特征2,…,特征N=P(类别)P(特征1,特征2,…,特征N)P(特征1,特征2,…,特征N)以上公式是朴素贝叶斯分类器的原理,即在给定n个特征的情况下,计算事件属于某个类别的概率,概率最大的那个类别即为该事件所属的类别.
虽然贝叶斯分类原理很简单,但却有着高效地学习效率和准确地分类效果.
原因是由于我们不需要知道类别概率的精确值P(θ∈1,2,…,k),而只需要分类器对它们进行正确的分类.
朴素贝叶斯算法被广泛应用于在机器学习中,相较于其他监督学习分类算法,其所需考虑的参数更少也更简单高效.
朴素贝叶斯的算法主要包括三个阶段:准备阶段,学习阶段和预测阶段.
在准备阶段,需要进行数据预处理,指定特征属性和类别,获取训练数据.
在学习阶段,首先要估计每个类别出现的概率,估计每个类别下每个特征属性出现的概率,然后对于每个属性组合,分别计算其归属于每个类别的概率.
在预测阶段,针对输入的特征属性集合,挑选最大概率所属的类别作为最终的分类结果.
1.
2随机混成自动机SHA考虑到我们的模型中含有时间,速度等连续变量,信号灯表示属于离散变量.
同时驾驶员状态的迁移以及行人对于来往车辆的关注行为都带有不确定的特性.
因此我们用随机混成自动机来构建模型.
随机混成自动机(StochasticHybridAutomata,SHA)[20]是混成自动机带有随机行为的版本.
用于实现对带有随机混成行为的系统建模,即包含离散和连续变化的变量,同时状态之间迁移带有随机行为.
本文关注的不确定环境下的人机物系统包含混成行为和随机行为,且对时间约束高度敏感.
因此本文将无人驾驶系统特征映射到随机混成自动机,实现自动化的模型验证.
SHA是对混成自动机HA进行了随机语义扩展,状态之间的迁移可基于离散概率分布[21].
随机混成自动机是一个八元组M=(L,l,C,Act,inv,enab,prob,F),其中表示位置的有限集合;表示初始位置,l∈L;表示时钟的有限集合;表示动作的有限集合;inv:L→CC(C)表示不变式的有限集合,表示时钟约束函数;enab:L*Act→CC(C)表示迁移触发的条件;prob:L*Act→Dist2*L表示概率迁移函数;F:L→2表示将每个位置映射到原子命题集合的标签函数.
1.
3概率计算树逻辑PCTL概率计算树逻辑(ProbabilisticComputationTreeLogic,PCTL)是对计算树逻辑的扩展(ComputationTreeLogic,CTL)的概率扩展,用概率运算符定量扩展了CTL的路径量词"所有"(All,A)和"存在"(Exists,E)PCTL的详细语义参见[22][23].
PCTL的语法的状态公式和路径公式ψ定义如下:true|ap|∧||P(ψ)ψU^{≤k}|X其中表示原子命题集合,ap∈AP,p∈[0,1],k∈N,时序操作符表示Next,表示Until.
状态公式中每个状态的被评估为true或false.
状态满足关系定义如下:s|=true,s|=apiffap∈inv(s)安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证5s|=iffss|=∧iffs|=ands|=s|=P(ψ)iffPr(s|=ψ)ps|=P(ψ)中表示在起始状态为s的路径集合中满足路径公式的概率,比较得出的概率P与给定的概率值p的对比结果是true还是false.
给定一个路径公式,第i个状态和初始状态分别定义为[i]和[0].
对于路径公式$\psi$的满足关系定义如下:ψ|=Xiffψ[1]|=ψ|=Uiffi,0≤i≤kψ[i]|=_2(i,0≤i≤kψ[i]|=1.
4统计模型检测统计模型检测(StatisticalModelChecking,SMC)问题可以描述为:给定一个随机系统模型和一个性质规约公式Φ,"统计模型检测技术建立在蒙特卡洛模拟(MonteCarlo)技术之上,它能够有效评估系统模型满足目标约束的概率区间,对系统进行验证分析".
SMC算法主要分为定性和定量两种类型,其中定性算法用来验证"系统M满足约束的概率是否大于或者等于某个概率阈值p,p∈[0,1],即s|=P(ψ)"包括:SingleSamplingPlan(SSP),SequentialProbabilityRatio(SPRT)和BayesianHypothesisTesting(BHT).
定量算法用来验证"系统M满足约束的概率是多少,即s|=Pψ"包括BayesianIntervalEstimation(BIE)和ApproximateProbabilisticModelChecking(APMC).
不同类型的SMC算法的主要区别在于统计参数的计算和置信度满足条件的判断这两方面.
2基于朴素贝叶斯分类器的人工驾驶风格分类模型在HCPS软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合的情况下.
作为人机物融合系统主体的智能体(Agent)在与所处的环境(Environment)不断进行交互的过程中,智能体需要像人一样具有学习能力,拥有"智能性"来应对各种环境.
无人驾驶系统作为HCPS的典型应用系统,无人驾驶汽车是集感知、决策和控制等功能于一体的自主交通工具,其中,感知系统代替人类驾驶人的视、听、触等功能,融合摄像机、雷达等传感器采集的海量交通环境数据,精确识别各类交通元素,为自动驾驶汽车决策系统提供支撑.
在无人驾驶和人工驾驶的混合交通场景中,由于人类驾驶员在驾驶过程中会疲劳、累或者会分心,这就使得人类驾驶行为是很随机的.
无人驾驶系统由于高精度的传感、执行、控制,它的技术是规定好的,不会退化,在交互过程中,智能化的技术对于未知环境的理解,认知理解能力是有限的.
而目前的一些无人驾驶设计是基于规则驾驶的一些模式设定的,有相关的一些逻辑参数,在自适应方面包括人性化方面做的很不到位,这就导致无人驾驶和人工驾驶有可能产生一定的冲突.
如何保证系统在不确定的复杂环境下智能运行仍是目前无人驾驶系统设计所面临的挑战.
在本节中,为了提高系统的"智能性",我们提出了基于朴素贝叶斯分类器的人工驾驶行为的分类模型(DrvingStyleClassification,DSC).
本章将重点介绍人工驾驶行为的分类模型,一方面从环境中接收数据,将环境数据和智能体自身的相关数据作为模型输入,基于朴素贝叶斯的分类算法对周边人工驾驶车辆的驾驶行为进行分类,学习器的学习结果将作为参数输入到后续的系统模型中.
无人驾驶车辆在行驶过程中要面对大量的不确定因素,在与人工驾驶的车辆交互的过程中,由于人类驾驶员在驾驶过程中的驾驶行为具有很强的主观性,所以在无人驾驶车辆的视角,驾驶员的行为状态具有一定的不确定性,例如面对相同的驾驶环境,不同的驾驶员可能会产生不同的驾驶行为.
如果无人驾驶车辆不能及时准确地判定周围人类驾驶员的驾驶行为,势必会导致本车进入不安全的状态.
因此需要对周边车辆的驾驶行为进行分析.
本节将重点聚焦于对人工驾驶车辆的驾驶风格进行分类.
本节的目标是通过无人驾驶与人工驾驶交互所产生的数据进行分类学习,构建人类驾驶员的驾驶行为分类模型,无人驾驶车辆根据周围人工驾驶车辆的当前状态来对其驾驶行为进行分类,并预测周边车辆的未来状态.
从而指导无人驾驶车辆做出智能决策.
为了实现该目标,本文提出了基于朴素贝叶斯的驾驶行为分类模型,使用有监督的机器学习训练模型以对数据进行分类,该模型的分类准确率将作为概率参数输入到下一节的模型中.
6Fig.
1Drivingstyleclassificationmodelbasedonnavebayes图1基于朴素贝叶斯分类器的驾驶行为分类模型2.
1分类流程图1展示了基于朴素贝叶斯分类器的驾驶行为分类模型练样本,第二部分是朴素贝叶斯分类器的线下训练阶段块(DataPreprocess),该模块是用来从提取特征数据并且形成驾驶行为的特征数据集的数据包括无人驾驶车辆自身的行车数据以及与周边人工驾驶车辆的关系数据取预处理器中后,特征样本存储器会存储特征样本,同时进入线下训练阶段习(BayesbasedLearning)中,使用所得的数据来训练状态预测模型下训练阶段中,第一步是估计每个类别出现的概率,接着估计每个类别条件下每个属性值出现的概率对每个属性组合计算所属于每个类别的概率p(x|y)P推测结果输出.
在第三阶段中,将实时收集到的时空数据输入训练好的分类模型中行为预测的结果.
下面详细介绍分类器线下训练流程:(1)将已知的输入数据(观测值或示例)和对数据的已知响应(2)选择参与训练的特征或者使用PCA降维,默认不降维(3)设定误分类代价,即类别准确率优先级,哪些类别一定要分对(4)选择训练模型并进行模型参数配置;(5)输入样本数据来训练模型,采用并行训练的方式可同时训练多个分类器模型该训练模型可以对新数据的响应生成预测;(6)分类器效果评价结果包括散点图、混淆矩阵(7)导出训练结果和模型文件,为接下来的线上训练提供准备2.
2模型评价指标针对一个二分类问题,我们将实例分为如下两类:JournalofSoftware软件学报classificationmodelbasedonnavebayes基于朴素贝叶斯分类器的驾驶行为分类模型展示了基于朴素贝叶斯分类器的驾驶行为分类模型,总共分为三部分,第一部分是数据预处理,获取训第二部分是朴素贝叶斯分类器的线下训练阶段,最后部分是在线测试阶段.
第一个模块是数据预处理模该模块是用来从提取特征数据并且形成驾驶行为的特征数据集.
在数据预处理阶段,带标签的数据包括无人驾驶车辆自身的行车数据以及与周边人工驾驶车辆的关系数据,将带标签的数据输入样本选同时进入线下训练阶段.
接着在第二个模块基于贝叶斯的学使用所得的数据来训练状态预测模型,通过该模型,可以判断驾驶行为的类别.
在线接着估计每个类别条件下每个属性值出现的概率p(y),并且)P(y),最后选择最大概率值p(x|y)P(y)作为该条件数据的将实时收集到的时空数据输入训练好的分类模型中,进行模型评估,最后输出对和对数据的已知响应(标签或类别)作为数据集输入;默认不降维,使用全部特征;哪些类别一定要分对,哪些类别可接受一定的误差范围;采用并行训练的方式可同时训练多个分类器模型,提高训练效率,混淆矩阵、ROC曲线等;为接下来的线上训练提供准备.
:正类(Positive)和负类(Negative).
安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证那么在实际分类中,会出现如下四种情况:(1)真正类(TruePositive,TP),即被预测为正类,实际为正类(2)假正类(FalsePositive,FP),即被预测为正类,实际为负类(3)真负类(TrueNegative,TN),即被预测为负类,实际为负类(4)假负类(FlaseNegative,FN),即被预测为负类,实际为正类正确率(Precision):Precision=真阳性率(TruePositiveRate,TPR),灵敏度(Sensitivity),真阴性率(TrueNegativeRate,TNR),特异度(Specificity)假阴性率(FalseNegativeRate,FNR):FNR=假阳性率(FalsePositiveRate,FPR):FPR=F1score:F1score=2.
3案例研究Fig.
2Senario:Humandrivevehiclechangetothelanewhere图2驾驶场景:无人驾驶车辆(黑色)变道至如图2所示:人工驾驶的车辆(蓝色、红色)在直行道上行驶向行驶.
在该驾驶场景中,无人驾驶车辆(黑色)需要变道至S,S,…,S表示不同时刻T,T,…,T车辆所在的不同位置不确定环境下人机物融合系统的形式化建模与动态验证7实际为正类;实际为负类;实际为负类;实际为正类.
(Sensitivity),召回率(Recall):TPR=Sensitivity=Recall=(Specificity):TNR=Speciicity=drivevehiclechangetothelanewhereautonomousvehicleoccupied变道至人工驾驶车辆(蓝色、红色)所在的车道上在直行道上行驶,旁边的车道上由一辆无人驾驶车辆(黑色)同需要变道至人工驾驶的车辆(蓝色、红色)所在的车道上.
图中车辆所在的不同位置.
上半部分表示场景一:蓝色人工驾驶车辆减速行驶,8JournalofSoftware软件学报黑色无人驾驶车辆通过加速后超车后完成变道.
下半部分表示场景二:红色人工驾驶车辆加速行驶,黑色无人驾驶车辆减速后跟在人工驾驶车辆后方完成变道.
2.
3.
1数据采集及预处理首先,需要从传感器获取时空数据,我们将智能体采集到的数据划分为以下三种类型,如表1所示:(1)自身驾驶数据以及与周边人所驾驶的车辆的关系数据,主要包括自动驾驶车辆的速度、加速度,与周边车辆的相对速度、相对距离等;(2)周边人所驾驶的车辆的驾驶数据,主要包括车灯使用是否正确,刹车次数以及是否存在其他不规范的行车行为等;(3)周边环境中与车辆无关的信息数据,主要包括天气(例如:雨天、雾天、晴天等),时间(例如:白天、晚上、早晚高峰等),道路情况(例如:高速公路、城市道路、乡村道路等)等.
由于缺少实验条件,我们采用仿真的方式生成了近200条数据,https://github.
com/DongdongAn/DrivingStyleClassification.
git在此场景中,人的行为是间接通过车辆的行驶数据来体现的,所以我们对人类所驾驶车辆的行车行为分类即为对人工驾驶员的驾驶行为分类.
Table1Theinputdataset表1输入分类器的数据集类别数据1.
与周边车辆的相关数据1)自动驾驶车辆的速度2)相对距离3)相对速度4)周边车辆的速度5)速度差百分比0120km/h1m20m15km/h15km/h0120km/h10%2.
周边车辆其他数据1)车灯使用是否正确2)刹车次数3)其他不合规行为0使用正确;1使用错误0无刹车;1有刹车0无;1有3.
周围环境1)天气情况2)所处时间0雨天;1晴天;2雾天0夜晚;1白天驾驶行为分类正常Normal;轻度激进SlightlyAggressive;激进Aggressive2.
3.
2分类器效果评价如图3所示,散点图表示了不同驾驶行为的分类情况,不同颜色的点表示不同的分类结果.
如图4所示,在人工智能中,混淆矩阵(ConfusionMatrix)是可视化工具,特别用于监督学习.
混淆矩阵是通过将每个实测像元的位置和分类与分类图像中的相应位置和分类像比较计算的,从而刻画一个分类器的分类准确程度来验证分类结果的有效性.
如图5所示,平行坐标图(ParallelCoordinatesPlot)为一种数据可视化的方式.
横坐标的每个标记表示样本中的一个属性,如车速、相对距离、相对速度等.
纵坐标表示每个样本中该属性的值,相连而得的一个折线表示该样本.
蓝色红色黄色分别表示激进驾驶行为、危险驾驶行为和正常驾驶行为.
直线表示分类结果与输入时样本的预分类结果一致,虚线表示模型的分类结果与输入时样本的预分类结果不一致.
如图6所示,ROC(ReceiverOperatingCharacteristic)曲线的横坐标表示:1Specificity,伪正类率(Falsepositiverate,FPR),预测为安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证9正但实际为负的样本占所有负例样本的比例;纵坐标表示:Sensitivity,真正类率(Truepositiverate,TPR),预测为正且实际为正的样本占所有正例样本的比例.
表2给出了线下训练结果,每个模型训练后的准确率及其他相关信息都会被显示出来.
训练方法主要包括决策树(DecisionTrees),朴素贝叶斯(NaiveBayesClassifiers),支持向量机(SupportVectorMachines),最近邻KNN(NearestNeighborClassifiers)和组合分类器.
最终的结果显示,训练准确度较高的是朴素贝叶斯分类器.
对于训练好的模型,我们可以输入新的数据进行分类,采用样本预测,将线下训练好的模型将模型导出到工作空间,这样就可以利用模型来测试新的数据.
Fig.
3DifferentDrivingStyleClassificationResultFig.
4ConfusionMatrixoftheClassificationResult图3不同驾驶行为的分类情况图4混淆矩阵结果Fig.
5ParallelCoordinatesPlotResultFig.
6ROC(ReceiverOperatingCharacteristic)图5分类结果的平行坐标图图6ROC曲线结果3线下与线上验证相结合的动态验证方法在上一节我们得到UPPAALSMC可以验证的模型后,通过写入要验证的性质(Query),即可对模型进行验证.
但是,目前使用UPPAALSMC进行验的时间成本较高,通常需要十几秒钟甚至更多,对于复杂的系统很可能10JournalofSoftware软件学报由于要检测的状态过多而产生状态爆炸的问题.
由于本文所研究的无人驾驶系统的物理车辆是行驶在不确定且复杂多变的场景中,十几秒钟后才能出现的验证结果对于系统来说是难以接受的,若车辆不能及时地对周边环境做出反应,那对于无人驾驶车辆来说将造成无法承担的后果.
所以我们从机器学习流程中线下训练和线上学习的过程中得到启发,通过采取线下验证和线上验证相结合的方法,通过比较参数即可快速得出验证结果,从而达到动态实时的验证效果,进而保障系统在复杂环境中安全运行.
Table2Thelearningresultoftheclassificationlearner表2分类器学习结果统计模型准确率分类错误数量预测速度训练时间精细树中等树粗略树83.
7%83.
7%81.
6%2424272600obs/sec1700obs/sec1700obs/sec1.
1363sec5.
1248sec5.
0357sec精细KNN中等KNN粗略KNN余弦KNN三次KNN加权KNN79.
6%78.
9%76.
2%78.
9%76.
9%83.
7%3031353134241300obs/sec1900obs/sec1800obs/sec2200obs/sec2800obs/sec2400obs/sec4.
8949sec2.
0646sec2.
35sec3.
3747sec3.
2652sec3.
714sec朴素贝叶斯85.
5%22760obs/sec1.
6165sec线性SVM二次SVM三次SVM精细高斯SVM78.
9%81.
6%85.
0%76.
2%312722351200obs/sec960obs/sec1100obs/sec1400obs/sec3.
7311sec3.
8418sec4.
7813sec4.
6623sec装袋树子空间判别子空间KNNRUSBooosted树85.
0%82.
3%79.
6%76.
9%22263034200obs/sec170obs/sec130obs/sec230obs/sec11.
638sec12.
516sec12.
403sec12.
846sec图7显示了线下与线上结合的动态验证方法示意图.
上半部分显示的是线下的验证过程,下半部分是线上验证的过程.
在线下验证过程中,统计模型检测工具UPPAALSMC接受的是属性和NSHA模型,其中所要验证的属性基于不同场景下的安全需求进行形式化描述产生,而NSHA模型由上一节提出的环境感知模型和线下训练场景共同建模得到.
不断加入新的线下场景进行验证.
这样在线上验证过程中,通过对比相关安全数据,在验证结果库中查询之前线下已经验证出的结果,从而及时给系统反馈,达到实时地动态验证的效果,使得HCPS系统可以智能安全又及时应对复杂多变的不确定性环境.
对于训练好的驾驶行为分类模型,通过数据两组新的环境数据和人工驾驶车辆的行车数据,我们得到的人工驾驶行为预测结果为:在场景一时刻,_=的概率为85%,在场景二时刻,_=的概率是87%.
将以上结果作为参数集输入到后续的NSHA模型中.
安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证Fig.
7Offlineandonlineverificationmethod图7线下与线上验证相结合的动态验证方法3.
1构建NSHA模型将无人驾驶车辆进行建模,UPPAALSMC可以进行验证的型组成,分别是组合模型Composite,开始模型Start,风险模型型Autodrive.
因此随机混成自动机网络可以表示成:ChangeLane=Composite∪Start图8表示复合状态抽象成的SHA模型,主要包括个Urgent状态,在Urgent状态中时间不流失,会跳转到下一个状态见https://github.
com/DongdongAn/DrivingStyleClassification.
git3.
2采用UPPAALSMC对NSHA模型进行验证建立好NSHA模型后,接下来是对其进行验证.
首先需要结合(1)P1表示在15个时间单位内人工驾驶车辆允许无人驾驶车辆通过的概率预测结果为normaldriver时,图9表示在模拟了其中置信度为0.
97.
其中概率密度分布和累积分布概率密度和概率.
图11表示当人工驾驶风格分类模型预测结果为和累积分布的情况.
(2)P2表示在30个时间单位内无人驾驶车辆完成变道的概率driver时,P2性质的概率密度分布和累积分布情况aggressivedriver时,P2性质的概率密度分布Table表3变道案例中验证的安全性质列表序号P1Pr[HumanDrive.
LET_PASS)P2Pr[AutoDrive.
CHANGE_LANE)不确定环境下人机物融合系统的形式化建模与动态验证11Fig.
8CompositeStateofSHAmodel图8复合状态抽象成的SHA模型可以进行验证的NSHA模型.
所构建出的NSHA模型由五个子模风险模型EnvRisk,人工驾驶模型HumanDrive和无人驾驶模:∪EnvRisk∪HumanDrive∪Autodrive主要包括STOP,STRAIGHT和CHANGE_LANE三个状态和两会跳转到下一个状态.
由于篇幅限制,其他SHA模型建立过程详https://github.
com/DongdongAn/DrivingStyleClassification.
git,在此不一一列举.
首先需要结合PCTL公式定义所要验证的性质,如表3所示.
个时间单位内人工驾驶车辆允许无人驾驶车辆通过的概率.
当人工驾驶风格分类模型表示在模拟了1305次之后,所得的概率区间是[0.
549862,0.
609859],和累积分布如图10所示.
图中的x轴表示时间,y轴分别表示人工驾驶风格分类模型预测结果为aggressivedriver时,概率密度分布个时间单位内无人驾驶车辆完成变道的概率.
图12表示当学习出的结果是normal和累积分布情况.
图13表示当人工驾驶风格分类模型预测结果为分布和累积分布情况.
Table3Propertylist变道案例中验证的安全性质列表性质](HumanDrive.
LET_PASS)0](AutoDrive.
CHANGE_LANE)12Fig.
9Theverification图9当学习出的结果是normalFig.
10Theprobabilitydistributionandcumulativedistribution图10当学习出的结果是normaldriverFig.
11Theprobabilitydistributionandcumulativedistribution图11当学习出的结果是aggressivedriverJournalofSoftware软件学报verificationresultofP1fornormaldrivernormaldriver时性质P1的验证结果cumulativedistributionofP1fornormaldriverdriver时,P1性质的概率密度分布和累积分布情况cumulativedistributionofP1foraggressivedriveraggressivedriver时,P1性质的概率密度分布和累积分布情况安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证Fig.
12Theprobabilitydistributionandcumulativedistribution图12当学习出的结果是normaldriverFig.
13Theprobabilitydistributionandcumulativedistribution图13当学习出的结果是aggressivedriver3.
3采用参数比较法进行动态验证在上一节我们得到UPPAALSMC可以验证的模型后证.
上一小节的验证都是线上验证的,通过设置不同的参数结果.
由于在风险等级较高的环境中,需要保证车辆的安全说是难以接受的.
若车辆不能及时地对周边环境做出反应于场景A,Probabilityuncertainty参数为0.
01,我们得到了验证结果实时运行在场景B中,如果场景B的大部分指标与A量相对于场景A较少.
那么,我们则不再需要对场景BA的验证结果即可.
这样参数对比的方法,大大节省了线上验证的时间统在复杂环境中安全运行.
在得到验证结果后,接下来就是决策阶段了据验证结果来决定是否改变车道.
不确定环境下人机物融合系统的形式化建模与动态验证13cumulativedistributionofP2fornormaldriverdriver时,P2性质的概率密度分布和累积分布情况cumulativedistributionofP2foraggressivedriveraggressivedriver时,P2性质的概率密度分布和累积分布情况可以验证的模型后,通过写入要验证的性质(Query),即可对模型进行验通过设置不同的参数,可以对同一个模型进行多次验证,得到不同的验证需要保证车辆的安全,但是验证时间在二十几秒之后才能得到对于系统来出反应,那对于无人驾驶车辆来说将造成无法承担的后果.
对我们得到了验证结果.
那么我们将其存入我们的场景库中.
在车辆A相同,个别项比场景A还要宽松,例如在相同环境下,人流B进行耗时的线上验证,只要参考场景比B更严格的场景大大节省了线上验证的时间,达到动态实时的验证效果,进而保障系接下来就是决策阶段了,基于不同的驾驶环境,无人驾驶车辆根14JournalofSoftware软件学报(1)当车辆行驶在高速公路上,车速大于80km/h时,车辆换道的概率大于95%.
(2)当车辆行驶在城区,车速小于30km/h时,车辆换道的概率大于80%.
例如,上面案例中P1的结果为90%,如果所处的场景为高速公路,90%80%,可以进行变道.
可见不同场景下指定不同的动作阈值可保证系统在更安全的情况下进行决策并决定未来状态.
本节以无人驾驶车辆与人工驾驶车辆交互过程中变道过程为案例,首先基于上一节提出的基于机器学习的环境感知模型得到驾驶风格分类结果,接着基于SHA模型对无人驾驶汽车的运动状态进行了建模,并使用统计模型检测工具UPPAALSMC来验证所建立的NSHA模型.
4相关工作比较对于驾驶风格识别目前的研究尚处于起步阶段.
人和机器最大的不同在于人是有情绪的,有些驾驶员比较激进,有些比较稳重.
2016年,谷歌的自动驾驶汽车在换道时和迎面而来的巴士相撞,原因就是自动驾驶汽车以为巴士会减速,而巴士司机却加速了.
如果能事先知道司机的驾驶风格,并结合进行预测,这场事故也许是可以避免的.
当然,驾驶风格目前还没有一个准确的定义,因此分类的依据也有很多种,比如油耗,均速,跟车行为等.
将驾驶风格识别成功应用到真实的自动驾驶系统的目前还没有相关报道,但是这些研究可能是未来自动驾驶发展的一个方向.
2011年11月15日,首个适用于汽车电子电器相关的产品的功能安全标准ISO26262正式发布.
功能安全的设计议题在汽车领域开始受到重视.
为了更好地来量化驾驶场景的不确定性和风险水平来提高自动驾驶系统的安全性.
Geng等人[24]提出了利用贝叶斯方法来量化深度神经网络的不确定性的方法.
Gadepally等人[25]设计了一个贝叶斯深度学习框架,并在模拟场景中展示了它相对于传统方法的优势.
该方法是每个模块在系统中的传递和输入都服从概率分布函数,而不是一个精确的结果.
另一种方法是单独评估驾驶场景下的风险水平,可以理解为前者是从系统内部评估,后者是从系统外部评估.
Yamazaki等人[26]将传感器数据输入到一个风险推理框架中,利用隐马尔科夫模型(HiddenMarkovModels,HMMs)和语言模型检测不安全的车道变更事件.
Yurtsever[27]引入了一个深度时空网络来推断驾驶场景的总体风险水平,来评估车道变更的风险水平.
牛津大学的Wu等人[28]提出了基于双方回合博弈的(Twoplayerturnbasedgame)框架来对神经网络的验证,用于评估安全攸关自动驾驶系统对交通标志识别的准确性.
Wicke等人[29]研究了对抗性输入扰动下的贝叶斯神经网络BNN的概率安全性,基于非凸优化的技术,开发了用于计算概率安全性的算法框架,从而验证具有数千个神经元的概率安全性并应用于自动驾驶系统.
Huang等人[30]出了可以表达社会信任概念(如能力,性格和依赖性)的算子来扩展逻辑PCTL*为概率理性时间逻辑PRTL*,建立一个基于人的信任度的模型验证框架,可用于自动驾驶系统根据行人的反应进行决策.
Sun等人[31]通过将覆盖率指导的神经网络测试工具DeepConcolic与车辆跟踪系统集成,对深度神经网络(DeepNeuralNetworks,DNN)的进行了验证.
伯克利大学的Sanjit等人[32]提出了一种通过深度强化学习来改善布尔逻辑回溯搜索算法的方法,对使用ML进行感知的系统进行形式分析的方法.
在基于深度神经网络的感知组件的上显示了该技术的有效性.
实际环境中的自动驾驶决策还有周围驾驶员的意图与行为相关.
目前该技术在自动驾驶领域尚不常见.
Geng等人[33]用隐马尔可夫模型(HMM)对目标车辆的未来行为进行了预测,通过学习人类驾驶特征,将预测时间范围延长了56%.
这里主要是利用了预定义的移动行为来标记观测值,然后再使用HMM以数据位中心学习每种类型的特征.
除此之外,还有一些其他的方法,比如贝叶斯网络分类器,混合高斯模型和隐马尔科夫模型相结合[34],支持向量机等.
这一类评估的主要问题在于观测时间短,实时计算量要求高,大多数情况下,自动驾驶系统只能观测周围车辆几秒钟,因此不能使用需要较长观察周期的复杂模型.
针对不确定性的模型检测技术,关于随机模型检验的研究开始于20世纪80年代初,Harts等人[35]使用离散时间马尔科夫过程建模概率程序,研究概率并发程序的终止性质和概率程序性质的证明方法.
Vardi等人[26][37]提出基于自动机理论的定性线性时间性质的验证方法,Courcoubetis和Yannakakis[38]研究了线性时间安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证15框架下的定性、定量验证理算时间马尔科夫链.
英国牛津大学的Kwiatkowska团队开发出图形化随机模型检验工具PRISM[39],该工具可以验证包括DTMC,CTMC,MDP,PA,PTA及其reward扩展模型等多种类型的随机系统模型,其性质规约包括PCTL,CSL,概率LTL,PCTL*及其reward扩展等定量性质规约语言.
PRISM基于BDD(BinaryDecisionDiagrams)和MTBDD(MultiTerminalBinaryDecisionDiagrams)的符号数据结构和算法[40],通过离散事件模拟引擎来实现定量抽象精化和系统归约等验证技术,支持多目标定量性质的随机模型检验和统计随机模型检验[41].
德国亚琛工业大学Hartmanns等人提出了支持验证随机混成自动机、随机时间自动机的工具集MODEST[42].
通过为现有语言提供导入和导出功能,允许重复使用现有模型;并通过将它们集成在统一的建模和分析环境中来允许重复使用现有工具.
MRMC(MarkovRewardModelChecker)采用基于系数矩阵的数据结构和算法[43],支持精确的onthefly稳态检查和互模拟最小化等验证技术,其优势在于验证规模较小的连续时间随机系统的稳态性质效率较高.
Katoen等人近年来开发的工具Storm[44]支持对马尔可夫链和马尔可夫决策过程的离散和连续时间变体进行分析,支持包括JANI和PRISM建模语言,动态故障树,广义随机Petri网和概率保护的命令语言.
模块化设置可轻松交换求解器和符号引擎,通过封装PythonAPI使得Storm工具可以使用扩展的算法来实现快速原型制作.
丹麦乌普萨拉大学的研究人员Larsen和David等人基于随机混成自动机SHA,开发了统计模型验证工具UPPAALSMC[46],统计模型检测是一种高效的验证技术,常用于复杂的随机系统的验证.
该工具所采用的技术主要是参数估计式和假设检验.
目前使用上述工具所进行建模的系统需要设计人员在建模初期就确定好参数,以便验证.
但在不确定性环境中,参数是不断变化的,采用此种验证方法无法满足时效性的要求.
目前结合机器学习的统计验证模型框架的相关工作比较少,缺乏统一的理论框架.
5总结与展望为了提高无人驾驶系统面对不确定环境的"智能性",本文提出了时空数据驱动的基于朴素贝叶斯分类器的周边人工驾驶行为分类模型DSC.
基于朴素贝叶斯的分类算法对周边人工驾驶车辆的驾驶行为进行分类并将学习器的学习结果作为参数输入到后续的系统模型中.
为了提高无人驾驶系统面对不确定环境的"安全性",我们从模型驱动的角度出发,构建结合了人工驾驶行为分类模型的计算结果的NSHA模型.
通过将NSHA模型和需要验证的性质共同输入进统计模型验证工具UPPAALSMC来对系统模型进行验证.
为了提高验证模型的效率,我们从机器学习流程中线下训练和线上学习的过程中得到启发,采用线下验证和线上验证相结合的方法,通过比较参数可快速得出验证结果,实现动态验证,从而帮助HCPS系统面对复杂多变的不确定性环境可以更及时地进行决策.
综上,我们对机器学习和形式化方法的交叉领域展开了探索研究.
整个过程展现了从机器学习、模型构建到统计模型验证.
在接下来的工作中,我们需要从以下几点进行拓展:由于条件限制,目前大多研究关注于无人驾驶车本身的数据采集,对周边车辆的监控数据通过识别或者对比来判断危险情况,存在一定的风险.
目前无人驾驶车辆还没有"智能"到可以预判周边人类驾驶员的行为.
近一年已经有学者在对相关问题展开研究,例如卡内基梅隆大学相关学者对周边车辆的相关数据进行了采集但是还未开放.
在今后的工作中,我们需要模拟不同情况下的危险驾驶行为的相关数据,从而帮助建立更完善的模型.
目前我们使用的是统计模型检测的工具UPPAALSMC.
暂时没有与其他高效率的验证工具进行对比,例如概率模型检测工具PRISM.
在接下来的工作中,我们考虑使用不同的工具进行验证.
目前的工作是基于监督学习的,由于强化学习在交互方面表现良好,未来我们考虑建立基于强化学习的人工驾驶行为分类模型,从而帮助无人驾驶车辆更智能地应对复杂的环境.
References:[1]LeeEA.
Cyberphysicalsystems:Designchallenges.
InProcofthe11thIEEEInternationalSymposiumonObjectandComponentOrientedRealTimeDistributedComputing(ISORC).
2008:363369.
[DOI:10.
1109/ISORC.
2008.
25][2]RobinsonRM,ScobeeDRR,BurdenSA,etal.
Dynamicinversemodelsinhumancyberphysicalsystems.
ProceedingsofSPIE,2016,9836.
[DOI:10.
1117/12.
2223176]16JournalofSoftware软件学报[3]LevesonNG.
Softwaresafety:why,what,andhow[J].
ACMComputingSurveys,1986,18(2):125163.
[DOI:10.
1145/7474.
7528][4]SunHY.
SafetySoftwareTestingBasedonMultiformClocksInputOutputTransitionSystem[Ph.
D.
Thesis].
Shanghai:EastChinaNormalUniversity,2017(inChinesewithEnglishabstract).
[5]SchirnerG,ErdogmusD,ChowdhuryKR,etal.
Thefutureofhumanintheloopcyberphysicalsystems[J].
IEEEComputer,2013,46(1):3645.
[DOI:10.
1109/MC.
2013.
31][6]GeigerA,LenzP,UrtasunR.
Arewereadyforautonomousdrivingthekittivisionbenchmarksuite.
ProceedingoftheIEEEconferenceonComputerVisionandPatternRecoginition(CVPR)2012:33543361.
[7]ElsayedGF,ShankarS,CheungB,etal.
Adversarialexamplesthatfoolbothcomputervisionandtimelimitedhumans.
AnnualConferenceonNeuralInformationProcessingSystems,NeurIPS2018,39143924.
[8]Finlayson,S.
G.
,Bowers,J.
D.
,Ito,J.
,Zittrain,J.
L.
,Beam,A.
L.
,Kohane,I.
S.
Adversarialattacksonmedicalmachinelearning.
Science,2019363(6433),12871289.
[DOI:10.
1126/science.
aaw4399][9]BanksVA,PlantKL,StantonNA.
Drivererrorordesignererror:Usingtheperceptualcyclemodeltoexplorethecircumstancessurroundingthefatalteslacrashon7thmay2016.
SafetyScience,2017,108:278285.
[DOI:10.
1016/j.
ssci.
2017.
12.
023][10]KohliP,ChadhaA.
Enablingpedestriansafetyusingcomputervisiontechniques:Acasestudyofthe2018uberinc.
selfdrivingcarcrash.
FutureofInformationandCommunicationConference,2019:261279.
[DOI:10.
1007/9783030123888_19][11]WoodcockJ,LarsenPG,BicarreguiJ,etal.
Formalmethods:Practiceandexperience.
ACMComputingSurveys,2009,41(4):19.
[DOI:10.
1145/1592434.
1592436][12]AbrialJ.
Formalmethods:Theorybecomingpractice.
JournalofUniversalComputerScience,2007,13:619628.
[13]BicarreguiJC,FitzgeraldJS,LarsenPG,etal.
Industrialpracticeinformalmethods:AreviewInternationalSymposiumonFormalMethods.
Springer,2009:810813.
[DOI:10.
1007/9783642050893_52][14]ClarkeJrEM,GrumbergO,KroeningD,etal.
Modelchecking[M].
MITpress,2018.
[15]LegayA,DelahayeB,BensalemS.
Statisticalmodelchecking:anoverview.
InInternationalconferenceonruntimeverificationSpringer,Berlin,Heidelberg.
2010.
122135.
[DOI:10.
1007/9783642166129_11][16]DuDH,ChengB,LiuJ.
Statisticalmodelcheckingforrareeventinsafetycriticalsystem.
RuanJianXueBao/JournalofSoftware,2015,26(2):305320(inChinese).
[17]ZulianiP,PlatzerA,ClarkeEM.
Bayesianstatisticalmodelcheckingwithapplicationtostateflow/simulinkverification.
FormalMethodsinSystemDesign,2013,43(2):338367.
[DOI:10.
1145/1755952.
1755987][18]DuDH,ZanH,JiangKQ,ChengB.
SelfAdaptivestatisticalmodelcheckingapproachforCPS.
RuanJianXueBao/JournalofSoftware,2017,28(5):11281143(inChinese)[19]DavarzaniS,NagahiM,TidwellM,etal.
Patternrecognitionusingmachinelearningforcornandsoybeanyieldprediction.
proceedingofthe2020IISE,NewOrleans,LA,USA,2020.
[20]JuliusAA,PappasGJ.
Approximationsofstochastichybridsystems.
IEEETransactionsonAutomaticControl,2009,54(6):11931203.
[DOI:10.
1109/TAC.
2009.
2019791][21]DavidA,LarsenKG,LegayA,etal.
Statisticalmodelcheckingofdynamicnetworksofstochastichybridautomata.
FranciscoJavierFuenteFernández,2014,66:91104.
[DOI:10.
14279/tuj.
eceasst.
66.
893.
878][22]LlerenaYRS,SuG,RosenblumDS.
ProbabilisticmodelcheckingofperturbedmdpswithapplicationstocloudcomputingProceedingsofthe201711thJointMeetingonFoundationsofSoftwareEngineering.
ACM,2017:454464.
[DOI:10.
1145/3106237.
3106301][23]ZhaoX,RobuV,FlynnD,etal.
Probabilisticmodelcheckingofrobotsdeployedinextremeenvironments.
ProceedingsoftheAAAIConferenceonArtificialIntelligence:2019(33):80668074.
[DOI:10.
1609/aaai.
v33i01.
33018066][24]GalY.
Uncertaintyindeeplearning.
[Ph.
D.
Thesis]UniversityofCambridge,2016.
[25]McAllisterR,GalY,KendallA,etal.
Concreteproblemsforautonomousvehiclesafety:Advantagesofbayesiandeeplearning:InternationalJointConferencesonArtificialIntelligence,2017.
[DOI:10.
24963/ijcai.
2017/661]安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证17[26]YamazakiS,MiyajimaC,YurtseverE,etal.
Integratingdrivingbehaviorandtrafficcontextthroughsignalsymbolization.
IEEEIntelligentVehiclesSymposium(IV).
IEEE,2016:642647.
[DOI:10.
1109/IVS.
2016.
7535455][27]YurtseverE,LiuY,LambertJ,etal.
Riskyactionrecognitioninlanechangevideoclipsusingdeepspatiotemporalnetworkswithsegmentationmasktransfer.
IEEEIntelligentTransportationSystemsConference(ITSC).
IEEE,2019:31003107.
[DOI:10.
1109/ITSC.
2019.
8917362][28]WuM,WickerM,RuanW,etal.
Agamebasedapproximateverificationofdeepneuralnetworkswithprovableguarantees.
TheoryComputerScience,2020,807:298329.
[DOI:10.
1016/j.
tcs.
2019.
05.
046][29]WickerM,LaurentiL,PataneA,etal.
Probabilisticsafetyforbayesianneuralnetworks.
CoRR,2020,abs/2004.
10281.
[30]HuangX,KwiatkowskaM,OlejnikM.
Reasoningaboutcognitivetrustinstochasticmultiagentsystems.
ACMTransactionsonCompututationLogic.
2019,20(4):21:121:64.
[DOI:10.
1145/3329123][31]SunY,ZhouY,MaskellS,etal.
Reliabilityvalidationoflearningenabledvehicletracking.
IEEEInternationalConferenceonRoboticsandAutomation(ICRA)2020.
93909396[DOI:10.
1109/ICRA40945.
2020.
9196932][32]LedermanG,RabeMN,SeshiaS,etal.
Learningheuristicsforquantifiedbooleanformulasthroughreinforcementlearning.
InternationalConferenceonLearningRepresentations,ICLR.
2020.
[33]DreossiT,DonzéA,SeshiaSA.
Compositionalfalsificationofcyberphysicalsystemswithmachinelearningcomponents.
JournalofAutomatedReasoning,2019,63(4):10311053.
[DOI:10.
1007/s10817018095095][34]GengX,LiangH,YuB,etal.
Ascenarioadaptivedrivingbehaviorpredictionapproachtourbanautonomousdriving.
AppliedSciences,2017,7(4):426.
[DOI:10.
3390/app7040426][35]AugustynowiczA.
Preliminaryclassificationofdrivingstylewithobjectiverankmethod.
Internationaljournalofautomotivetechnology,2009,10(5):607610.
[DOI:10.
1007/s1223900900718][36]HartS,SharirM,PnueliA.
Terminationofprobabilisticconcurrentprograms:(extendedabstract)Symposiumonprinciplesofprogramminglanguages.
1982:16.
[DOI:10.
1145/582153.
582154][37]VardiMY.
Automaticverificationofprobabilisticconcurrentfinitestateprograms.
Foundationsofcomputerscience.
1985:327338.
[DOI:10.
1109/SFCS.
1985.
12][38]VardiMY,WolperP.
Anautomatatheoreticapproachtoautomaticprogramverification.
ProceedingsoftheFirstSymposiumonLogicinComputerScience.
IEEEComputerSociety,1986:322331.
[39]CourcoubetisC,YannakakisM.
Thecomplexityofprobabilisticverification.
JournaloftheACM,1995,42(4):857907.
[DOI:10.
1145/210332.
210339][40]KwiatkowskaM,NormanG,ParkerD.
PRISM4.
0:Verificationofprobabilisticrealtimesystems.
InternationalConferenceonComputerAidedVerification(CAV).
2011:585591.
[DOI:10.
1007/9783642221101_47][41]KwiatkowskaM,NormanG,ParkerD.
Probabilisticsymbolicmodelcheckingwithprism:ahybridapproachInternationalJournalonSoftwareToolsforTechnologyTransfer.
SpringerVerlag,2001.
[DOI:10.
1007/s1000900401402][42]KwiatkowskaM.
Quantitativeverification:modelstechniquesandtools.
Proceedingsofthethe6thjointmeetingoftheEuropeansoftwareengineeringconferenceandtheACMSIGSOFTsymposiumonThefoundationsofsoftwareengineering.
2007:449458.
[DOI:10.
1145/1295014.
1295018][43]HartmannsA,HermannsH.
Themodesttoolset:Anintegratedenvironmentforquantitativemodellingandverification.
InternationalConferenceonToolsandAlgorithmsfortheConstructionandAnalysisofSystems.
Springer,2014:593598.
[DOI:10.
1007/9783642548628_51][44]KatoenJP,ZapreevIS,HahnEM,etal.
Theinsandoutsoftheprobabilisticmodelcheckermrmc.
PerformanceEvaluation,2011,68(2):90104.
[DOI:10.
1016/j.
peva.
2010.
04.
001][45]HenselC,JungesS,KatoenJ,etal.
Theprobabilisticmodelcheckerstorm.
CoRR,2020,abs/2002.
07080.
[46]DehnertC.
,JungesS.
,KatoenJP.
,VolkM.
AStormisComing:AModernProbabilisticModelChecker.
InternationalConferenceonComputerAidedVerification(CAV)2017[DOI:10.
1007/9783319633909_31]18JournalofSoftware软件学报附中文参考文献:[4]孙海英.
基于多形态时钟输入输出迁移系统的安全软件测试研究[博士学位论文].
华东师范大学,2017.
[16]杜德慧,程贝,刘静.
面向安全攸关系统中小概率事件的统计模型检测.
软件学报,2015,26(2):305320.
[18]杜德慧,昝慧,姜凯强,程贝.
一种面向CPS的自适应统计模型检测方法.
软件学报,2017,28(5):11281143.
13328/j.
cnki.
jos.
006272]中国科学院软件研究所版权所有.
不确定环境下人机物融合系统的形式化安冬冬1,刘静2,陈小红2,孙海英21(上海师范大学信息与机电工程学院,上海200234)2(华东师范大学软件工程学院,上海200062)通讯作者:刘静,Email:jliu@sei.
ecnu.
edu.
cn摘要:随着科技的进步,新型复杂系统例如人机物融合系统人类社会生活越来越密不可分.
软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决能、安全的人机物融合系统已经成为软件行业不可回避的挑战确感知其所处的运行环境.
感知的不确定性将导致系统的误判设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约形式化规约是保证系统安全的首要条件.
为了应对规约的不确定性的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模动态验证的方式保证系统的安全,从而构建统一安全的理论框架与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用关键词:人机物融合系统;机器学习;不确定性建模;形式化验证中图法分类号:TP311中文引用格式:安冬冬,刘静,陈小红,孙海英.
不确定环境下人机物融合系统的http://www.
jos.
org.
cn/10009825/6272.
htm英文引用格式:AnDD,LiuJ,ChenXH,SunHY.
Formalmodelingandunderuncertainenvironment.
RuanJianXueBao/JournalofSoftware,206272.
htmFormalModelingandDynamicVerificationforHumanCyberPhysicalSystemsunderUncertainEnvironmentANDongDong1,LIUJing2,CHENXiaoHong2,SUN1(TheCollegeofInformation,MechanicalandElectricalEngineering2(ShanghaiKeyLaboratoryofTrustworthyComputing,EastChinaNormalAbstract:Withthedevelopmentoftechnology,newcomplexsystemssuchasHumanCyberindistinguishablefromsociallife.
Thecyberspacewherethesoftwaresystemlocatedpeople'sdailylife.
Theuncertainfactorssuchasthedynamicspatiotemporaldataaswellastheunpredictablehumanbehaviorincreasingsecurityrequirements,thescaleandcomplexityofthesystemaretaatremainunresolved.
Therefore,developingintelligentandsafehumancyberbecomingtheinevitablechallengeforthesoftwareindustry.
Itisdifficultforthehumancyber基金项目:国家重点研发计划项目(2019YFA0706404);国家自然科学基金技计划项目(20ZR1416000)收稿时间:20200917;修改时间:20201026;采用时间:2020Email:jos@iscas.
ac.
cnhttp://www.
jos.
org.
cnTel:+861062562563形式化建模与动态验证新型复杂系统例如人机物融合系统(HumanCyberPhysicalSystems,HCPS)已经与软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.
物理空间时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.
由于系统安系统的规模和复杂度随之增加所带来的一系列问题亟待解决.
因此,在不确定性环境下,构造智安全的人机物融合系统已经成为软件行业不可回避的挑战.
环境不确定性使得人机物融合系统软件无法准感知的不确定性将导致系统的误判,从而影响系统的安全性.
环境不确定性使得系统合系统软件的运行环境提供准确的形式化规约.
而对于安全要求较高的系统,准确的为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合基于环境中时空数据对环境进行建模.
根据安全软件的典型特征,采用从而构建统一安全的理论框架.
为了展示方案的可行性,本文以自动驾驶车辆的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.
形式化验证;统计模型检测不确定环境下人机物融合系统的形式化建模与动态验证.
软件学报.
odelinganddynamicverificationforhumancyberphysicalsystemsJournalofSoftware,2021(inChinese).
http://www.
jos.
org.
cn/10009825/FormalModelingandDynamicVerificationforHumanCyberPhysicalSystemsunderHaiYing2TheCollegeofInformation,MechanicalandElectricalEngineering,ShanghaiNormalUniversity,Shanghai200234,China),EastChinaNormalUniversity,Shanghai200062,China)oftechnology,newcomplexsystemssuchasHumanCyberPhysicalSystems(HCPS)havebecomespacewherethesoftwaresystemlocatedisincreasinglyintegratedwiththephysicalspaceofdynamicenvironmentinthephysicalspace,theexplosivegrowthoftheunpredictablehumanbehaviorareallcompromisethesecurityofthesystem.
Asaresultofthethescaleandcomplexityofthesystemarealsoincreaseing.
ThissituationleadstoaseriesofproblemsTherefore,developingintelligentandsafehumancyberphysicalsystemsunderuncertainenvironmentistisdifficultforthehumancyberphysicalsystemstoperceivetheruntime国家自然科学基金(61972150);上海市知识服务平台(ZF1213);上海市科:20201214;jos在线出版时间:202101222JournalofSoftware软件学报environmentaccuratelyunderuncertainsurroundings.
Theuncertainperceptionwillleadtothesystem'smisinterpretation,thusaffectingthesecurityofthesystem.
Itisdifficultforthesystemdesignerstoconstructformalspecificationsforthehumancyberphysicalsystemsunderuncertainenvironment.
Forsafetycriticalsystems,formalspecificationsaretheprerequisitestoensuresystemsecurity.
Tocopewiththeuncertaintyofthespecifications,weproposeacombinationofdatadrivenandmodeldrivenmodelingmethodology,thatis,weusethemachinelearningbasedalgorithmstomodeltheenvironmentbasedonspatiotemporaldata.
Weintroduceanapproachtointegratemachinelearningmethodandruntimeverificationtechnologyasaunifiedframeworktoensurethesafetyofthehumancyberphysicalsystems.
Weillustrateourapproachbymodelingandanalyzingascenariooftheinteractionofanautonomousvehicleandahumandrivenmotorbike.
Keywords:humancyberphysicalsystem;machinelearning;uncertaintymodeling;formalverification;statisticalmodelchecking随着计算机科学技术的发展,各种新型复杂系统快速涌现,尤其是与人类社会交互和协作的复杂系统越来越受到人们的关注.
信息物理融合系统(CyberPhysicalSystems,CPS)是一种综合计算、网络和物理环境的多维复杂系统,通过3C技术,即计算(Computation)、通信(Communication)和控制(Control)的有机融合与深度协作,实现大型工程系统的实时感知、动态控制和信息服务[1].
CPS系统的本质就是以"人机物"的融合为目标的计算技术,以实现人的控制在时间、空间等方面的延伸.
人机物融合系统(HumanCyberPhysicalSystems,HCPS)是具有深度集成的人、网络和物理元素的智能联网系统[2],是在信息物理系统CPS的基础上,重点考虑系统所处的不确定环境以及环境中人的因素.
例如与驾驶员和行人交互的自动驾驶系统,与医生合作的智慧医疗系统以及与用户互动的智能家居系统等.
作为人机物系统的核心,HCPS软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.
作为人机物融合系统主体的智能体(Agent)在与所处的环境(Environment)不断进行交互的过程中,智能体需要要像人一样具有学习能力,拥有"智能性"来应对各种环境.
"智能性"主要指计算智能,是以数据为基础,通过训练建立联系进行问题求解,人工神经网络、遗传算法、模糊系统、进化程序设计等都属于计算智能.
由于环境与过程的时空特性,HCPS系统行为的响应不仅与所经历的时间有关,同时也和所处的空间相关,具体表现为计算过程要求严格的时间约束,而物理过程具有空间依赖性.
同样,随着万物互联的发展,人成为HCPS系统中的重要组成部分.
由于许多HCPS都发挥着至关重要的作用(例如在能源、医疗保健、国防安全、智能驾驶等方面),因此这些系统的"安全性"也同样至关重要.
"安全性"是系统所在环境的函数,是对任何环境下系统零风险程度的度量[3].
Sun等人[4]指出"确保软件的安全性是指在任何环境中各种软件的运行不会导致系统出现不可预测的风险,具有避免灾难事故发生的能力".
物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统的安全性.
智能体如何准确感知并捕获不确定环境中的有效信息并及时做出准确且安全地决策是目前研究人员重点关注的问题.
由于人机物融合系统所涉及的研究系统比较广泛,不同系统所涉及的人的因素各不相同,本文中我们以无人驾驶系统作为人机物融合系统的典型案例进行分析和研究.
无人驾驶是典型的HCPS应用领域,未来将是人机共驾、有人无人驾驶车辆共存的局面.
在这样的混合交通场景中,无人驾驶车辆作为智能体不可避免地需要与所处环境中的其他车辆以及车辆内部和外部的人进行交互[5].
这对无人驾驶系统的设计提出了更高的要求,一方面,系统需要有应对环境的"智能性",拥有迅速准确的决策能力,可以自主应对驾驶过程中常常遇到的、偶发的各种各样的不确定性事件.
我们知道,人类驾驶员在突发事件情况下,会因为情绪失控而导致不理性决策产生.
对于人来说,这类事故是小概率事件,因而很难通过对事故的"练习"来帮助驾驶员积累处理经验.
而机器学习(MachineLearning,ML)技术可以帮助自动驾驶系统应用所感知到的时空数据进行及时有效地计算,从而分析周边环境来产生决策.
因而无人驾驶系统可以在事故发生时,精准理性地应对,从而最大限度地减少事故的发生.
机器学习可以帮助提高系统的"智能性",但是并不能保证系统的"安全性".
数据驱动的方式可能会由于某个数据的变化导致学习出的结果是错误的,从而产生无法预料的后果,这对安全的系统是不可接受的[6][7][8].
该方案显示出了对于数据的敏感性,由于机器学习算法本身可解释性较差的缺点导致系统无法预知所学习的结果.
所以仅仅依靠机器学习的方法无法保证无人驾驶系统的安全性.
目前无人驾驶由于安全问题的不断出现仍然面临巨大挑战.
2016年,一辆特斯拉的汽车由于传感器失灵而没有及时感知前方的障碍物而与之发生碰撞安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证3[9].
2018年,Uber的无人驾驶车由于夜间识别能力较差没有及时感知到前方的行人进行避让而发生车祸事故,导致行人的死亡[10].
城市交通环境日趋复杂,面对自动驾驶场景复杂多变、时空数据的爆发以及其他人工驾驶车辆的主观驾驶行为所导致了环境中不确定性的增加,如何避免事故的产生,来保证系统的"安全性"仍是目前的研究难点.
随着HCPS的应用空间的增长,开发具有安全保证的设计框架至关重要.
在对HCPS建模过程中,需要重点考虑HCPS动态行为的三个特性:(1)混成性:HCPS依赖行为离散的计算系统,同时也依赖行为连续的物理环境(例如:连续的温度变化、时间及空间的变化等),其异构的本质导致其行为具有混成性;(2)随机性:HCPS系统处在开放的环境中,不确定的环境(例如:环境中人的行为不确定、用户的行为不确定以及天气的变化等),造成HCPS的行为具有随机性;(3)安全性:HCPS经常被用于安全攸关的系统(例如:智慧医疗系统、列车控制系统和智能驾驶系等),所以需保证HCPS的行为必须是安全可信的.
形式化方法(FormalMethod,FM)是基于严谨的数学(逻辑)语言和精确的数学语义的方法学,主要应用于对系统软件进行建模分析和验证等工作,保证系统的正确运行[11].
面对系统规模的增长和复杂度的增加,形式化方法越来越频繁地被应用于安全攸关软件的验证,以此来保证其安全性[12][13].
模型检测(ModelChecking,MC)是通过对系统的状态空间进行全遍历,从而对系统的安全性进行自动验证[14],其本质思路是将一个过程或系统抽象成一个有穷状态机模型加以分析验证.
传统的模型检测由于状态爆炸的问题,增大了对系统进行分析验证的难度.
统计模型检测技术(StatisticalModelChecking,SMC)[15]可以通过评估系统所满足的概率区间对系统进行定量分析,从而有效解决状态过多而难以验证的问题[16][17][18].
统计模型检测是一种高效的验证技术,常用于复杂的随机系统的验证.
该工具所采用的技术主要是参数估计式和假设检验.
其中,参数估计是基于所收集到足够的样本,给出模型满足给定性质的近似概率,属于定量的结果;而假设检验是基于样本给出模型是否满足给定的性质,属于定性的结果.
本文主要考虑人类驾驶车辆和自动驾驶车辆共存的混合交通流下的驾驶环境,由于人的行为以及物理环境导致不确定性因素的增加.
而UPPAALSMC具有定性和定量分析的能力,能够分析验证出自动驾驶车辆的相对安全性,因此,本文选用UPPAALSMC作为自动验证工具.
本文采用时空数据驱动的方法来处理环境的不确定性,针对安全攸关HCPS建模与验证缺乏统一系统的理论、方法.
围绕"不确定环境下的人机物融合系统的建模与验证"关键科学问题,提出了以数据驱动和模型驱动相结合的创新方式构建不确定环境下的HCPS,并对其关键支撑技术进行创新性研究.
(1)针对系统所处的物理环境的不确定性,应用机器学习技术,以环境中的时空数据为驱动,环境感知计算为切入点,提出了不确定环境下的基于朴素贝叶斯的人类行为分类模型.
(2)为了应对大规模系统的结构化建模,构建了不确定环境场景下的HCPS系统模型,使用验证工具UPPAALSMC实现对模型的动态验证.
(3)提出基于统计模型验证的运行时动态验证技术,采取线下和线上验证相结合的方法,即通过比较参数即可快速得出验证结果,从而达到动态实时的验证效果,进而保障系统在复杂环境中安全运行.
本文以构建安全智能的人机物融合系统的理论框架及应用作为主要的研究目标.
第1节主要介绍所涉及的一些背景知识,包括其概念及其主要应用.
第2节介绍了不确定环境下的感知模型,针对系统所处的物理环境的不确定性,应用机器学习算法,以环境的时空数据为驱动,提出了不确定环境下的基于朴素贝叶斯的人类驾驶行为分类模型.
第3节提出了线下与线上验证相结合的动态验证方法即通过验证工具UPPAALSMC实现对模型的动态验证,从而定量评估不确定性环境以及人的行为对系统安全性的影响.
第4节对相关工作进行了比较,最后总结全文,并对未来值得关注的研究方向进行初步探讨.
4JournalofSoftware软件学报1预备知识1.
1朴素贝叶斯算法朴素贝叶斯或简单贝叶斯分类器广泛应用于数据分析.
朴素贝叶斯分类器[19],基于关键的约束假设,即属性之间彼此独立,也就是类别|特征1,特征2,…,特征N=P(类别)P(特征1,特征2,…,特征N)P(特征1,特征2,…,特征N)以上公式是朴素贝叶斯分类器的原理,即在给定n个特征的情况下,计算事件属于某个类别的概率,概率最大的那个类别即为该事件所属的类别.
虽然贝叶斯分类原理很简单,但却有着高效地学习效率和准确地分类效果.
原因是由于我们不需要知道类别概率的精确值P(θ∈1,2,…,k),而只需要分类器对它们进行正确的分类.
朴素贝叶斯算法被广泛应用于在机器学习中,相较于其他监督学习分类算法,其所需考虑的参数更少也更简单高效.
朴素贝叶斯的算法主要包括三个阶段:准备阶段,学习阶段和预测阶段.
在准备阶段,需要进行数据预处理,指定特征属性和类别,获取训练数据.
在学习阶段,首先要估计每个类别出现的概率,估计每个类别下每个特征属性出现的概率,然后对于每个属性组合,分别计算其归属于每个类别的概率.
在预测阶段,针对输入的特征属性集合,挑选最大概率所属的类别作为最终的分类结果.
1.
2随机混成自动机SHA考虑到我们的模型中含有时间,速度等连续变量,信号灯表示属于离散变量.
同时驾驶员状态的迁移以及行人对于来往车辆的关注行为都带有不确定的特性.
因此我们用随机混成自动机来构建模型.
随机混成自动机(StochasticHybridAutomata,SHA)[20]是混成自动机带有随机行为的版本.
用于实现对带有随机混成行为的系统建模,即包含离散和连续变化的变量,同时状态之间迁移带有随机行为.
本文关注的不确定环境下的人机物系统包含混成行为和随机行为,且对时间约束高度敏感.
因此本文将无人驾驶系统特征映射到随机混成自动机,实现自动化的模型验证.
SHA是对混成自动机HA进行了随机语义扩展,状态之间的迁移可基于离散概率分布[21].
随机混成自动机是一个八元组M=(L,l,C,Act,inv,enab,prob,F),其中表示位置的有限集合;表示初始位置,l∈L;表示时钟的有限集合;表示动作的有限集合;inv:L→CC(C)表示不变式的有限集合,表示时钟约束函数;enab:L*Act→CC(C)表示迁移触发的条件;prob:L*Act→Dist2*L表示概率迁移函数;F:L→2表示将每个位置映射到原子命题集合的标签函数.
1.
3概率计算树逻辑PCTL概率计算树逻辑(ProbabilisticComputationTreeLogic,PCTL)是对计算树逻辑的扩展(ComputationTreeLogic,CTL)的概率扩展,用概率运算符定量扩展了CTL的路径量词"所有"(All,A)和"存在"(Exists,E)PCTL的详细语义参见[22][23].
PCTL的语法的状态公式和路径公式ψ定义如下:true|ap|∧||P(ψ)ψU^{≤k}|X其中表示原子命题集合,ap∈AP,p∈[0,1],k∈N,时序操作符表示Next,表示Until.
状态公式中每个状态的被评估为true或false.
状态满足关系定义如下:s|=true,s|=apiffap∈inv(s)安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证5s|=iffss|=∧iffs|=ands|=s|=P(ψ)iffPr(s|=ψ)ps|=P(ψ)中表示在起始状态为s的路径集合中满足路径公式的概率,比较得出的概率P与给定的概率值p的对比结果是true还是false.
给定一个路径公式,第i个状态和初始状态分别定义为[i]和[0].
对于路径公式$\psi$的满足关系定义如下:ψ|=Xiffψ[1]|=ψ|=Uiffi,0≤i≤kψ[i]|=_2(i,0≤i≤kψ[i]|=1.
4统计模型检测统计模型检测(StatisticalModelChecking,SMC)问题可以描述为:给定一个随机系统模型和一个性质规约公式Φ,"统计模型检测技术建立在蒙特卡洛模拟(MonteCarlo)技术之上,它能够有效评估系统模型满足目标约束的概率区间,对系统进行验证分析".
SMC算法主要分为定性和定量两种类型,其中定性算法用来验证"系统M满足约束的概率是否大于或者等于某个概率阈值p,p∈[0,1],即s|=P(ψ)"包括:SingleSamplingPlan(SSP),SequentialProbabilityRatio(SPRT)和BayesianHypothesisTesting(BHT).
定量算法用来验证"系统M满足约束的概率是多少,即s|=Pψ"包括BayesianIntervalEstimation(BIE)和ApproximateProbabilisticModelChecking(APMC).
不同类型的SMC算法的主要区别在于统计参数的计算和置信度满足条件的判断这两方面.
2基于朴素贝叶斯分类器的人工驾驶风格分类模型在HCPS软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合的情况下.
作为人机物融合系统主体的智能体(Agent)在与所处的环境(Environment)不断进行交互的过程中,智能体需要像人一样具有学习能力,拥有"智能性"来应对各种环境.
无人驾驶系统作为HCPS的典型应用系统,无人驾驶汽车是集感知、决策和控制等功能于一体的自主交通工具,其中,感知系统代替人类驾驶人的视、听、触等功能,融合摄像机、雷达等传感器采集的海量交通环境数据,精确识别各类交通元素,为自动驾驶汽车决策系统提供支撑.
在无人驾驶和人工驾驶的混合交通场景中,由于人类驾驶员在驾驶过程中会疲劳、累或者会分心,这就使得人类驾驶行为是很随机的.
无人驾驶系统由于高精度的传感、执行、控制,它的技术是规定好的,不会退化,在交互过程中,智能化的技术对于未知环境的理解,认知理解能力是有限的.
而目前的一些无人驾驶设计是基于规则驾驶的一些模式设定的,有相关的一些逻辑参数,在自适应方面包括人性化方面做的很不到位,这就导致无人驾驶和人工驾驶有可能产生一定的冲突.
如何保证系统在不确定的复杂环境下智能运行仍是目前无人驾驶系统设计所面临的挑战.
在本节中,为了提高系统的"智能性",我们提出了基于朴素贝叶斯分类器的人工驾驶行为的分类模型(DrvingStyleClassification,DSC).
本章将重点介绍人工驾驶行为的分类模型,一方面从环境中接收数据,将环境数据和智能体自身的相关数据作为模型输入,基于朴素贝叶斯的分类算法对周边人工驾驶车辆的驾驶行为进行分类,学习器的学习结果将作为参数输入到后续的系统模型中.
无人驾驶车辆在行驶过程中要面对大量的不确定因素,在与人工驾驶的车辆交互的过程中,由于人类驾驶员在驾驶过程中的驾驶行为具有很强的主观性,所以在无人驾驶车辆的视角,驾驶员的行为状态具有一定的不确定性,例如面对相同的驾驶环境,不同的驾驶员可能会产生不同的驾驶行为.
如果无人驾驶车辆不能及时准确地判定周围人类驾驶员的驾驶行为,势必会导致本车进入不安全的状态.
因此需要对周边车辆的驾驶行为进行分析.
本节将重点聚焦于对人工驾驶车辆的驾驶风格进行分类.
本节的目标是通过无人驾驶与人工驾驶交互所产生的数据进行分类学习,构建人类驾驶员的驾驶行为分类模型,无人驾驶车辆根据周围人工驾驶车辆的当前状态来对其驾驶行为进行分类,并预测周边车辆的未来状态.
从而指导无人驾驶车辆做出智能决策.
为了实现该目标,本文提出了基于朴素贝叶斯的驾驶行为分类模型,使用有监督的机器学习训练模型以对数据进行分类,该模型的分类准确率将作为概率参数输入到下一节的模型中.
6Fig.
1Drivingstyleclassificationmodelbasedonnavebayes图1基于朴素贝叶斯分类器的驾驶行为分类模型2.
1分类流程图1展示了基于朴素贝叶斯分类器的驾驶行为分类模型练样本,第二部分是朴素贝叶斯分类器的线下训练阶段块(DataPreprocess),该模块是用来从提取特征数据并且形成驾驶行为的特征数据集的数据包括无人驾驶车辆自身的行车数据以及与周边人工驾驶车辆的关系数据取预处理器中后,特征样本存储器会存储特征样本,同时进入线下训练阶段习(BayesbasedLearning)中,使用所得的数据来训练状态预测模型下训练阶段中,第一步是估计每个类别出现的概率,接着估计每个类别条件下每个属性值出现的概率对每个属性组合计算所属于每个类别的概率p(x|y)P推测结果输出.
在第三阶段中,将实时收集到的时空数据输入训练好的分类模型中行为预测的结果.
下面详细介绍分类器线下训练流程:(1)将已知的输入数据(观测值或示例)和对数据的已知响应(2)选择参与训练的特征或者使用PCA降维,默认不降维(3)设定误分类代价,即类别准确率优先级,哪些类别一定要分对(4)选择训练模型并进行模型参数配置;(5)输入样本数据来训练模型,采用并行训练的方式可同时训练多个分类器模型该训练模型可以对新数据的响应生成预测;(6)分类器效果评价结果包括散点图、混淆矩阵(7)导出训练结果和模型文件,为接下来的线上训练提供准备2.
2模型评价指标针对一个二分类问题,我们将实例分为如下两类:JournalofSoftware软件学报classificationmodelbasedonnavebayes基于朴素贝叶斯分类器的驾驶行为分类模型展示了基于朴素贝叶斯分类器的驾驶行为分类模型,总共分为三部分,第一部分是数据预处理,获取训第二部分是朴素贝叶斯分类器的线下训练阶段,最后部分是在线测试阶段.
第一个模块是数据预处理模该模块是用来从提取特征数据并且形成驾驶行为的特征数据集.
在数据预处理阶段,带标签的数据包括无人驾驶车辆自身的行车数据以及与周边人工驾驶车辆的关系数据,将带标签的数据输入样本选同时进入线下训练阶段.
接着在第二个模块基于贝叶斯的学使用所得的数据来训练状态预测模型,通过该模型,可以判断驾驶行为的类别.
在线接着估计每个类别条件下每个属性值出现的概率p(y),并且)P(y),最后选择最大概率值p(x|y)P(y)作为该条件数据的将实时收集到的时空数据输入训练好的分类模型中,进行模型评估,最后输出对和对数据的已知响应(标签或类别)作为数据集输入;默认不降维,使用全部特征;哪些类别一定要分对,哪些类别可接受一定的误差范围;采用并行训练的方式可同时训练多个分类器模型,提高训练效率,混淆矩阵、ROC曲线等;为接下来的线上训练提供准备.
:正类(Positive)和负类(Negative).
安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证那么在实际分类中,会出现如下四种情况:(1)真正类(TruePositive,TP),即被预测为正类,实际为正类(2)假正类(FalsePositive,FP),即被预测为正类,实际为负类(3)真负类(TrueNegative,TN),即被预测为负类,实际为负类(4)假负类(FlaseNegative,FN),即被预测为负类,实际为正类正确率(Precision):Precision=真阳性率(TruePositiveRate,TPR),灵敏度(Sensitivity),真阴性率(TrueNegativeRate,TNR),特异度(Specificity)假阴性率(FalseNegativeRate,FNR):FNR=假阳性率(FalsePositiveRate,FPR):FPR=F1score:F1score=2.
3案例研究Fig.
2Senario:Humandrivevehiclechangetothelanewhere图2驾驶场景:无人驾驶车辆(黑色)变道至如图2所示:人工驾驶的车辆(蓝色、红色)在直行道上行驶向行驶.
在该驾驶场景中,无人驾驶车辆(黑色)需要变道至S,S,…,S表示不同时刻T,T,…,T车辆所在的不同位置不确定环境下人机物融合系统的形式化建模与动态验证7实际为正类;实际为负类;实际为负类;实际为正类.
(Sensitivity),召回率(Recall):TPR=Sensitivity=Recall=(Specificity):TNR=Speciicity=drivevehiclechangetothelanewhereautonomousvehicleoccupied变道至人工驾驶车辆(蓝色、红色)所在的车道上在直行道上行驶,旁边的车道上由一辆无人驾驶车辆(黑色)同需要变道至人工驾驶的车辆(蓝色、红色)所在的车道上.
图中车辆所在的不同位置.
上半部分表示场景一:蓝色人工驾驶车辆减速行驶,8JournalofSoftware软件学报黑色无人驾驶车辆通过加速后超车后完成变道.
下半部分表示场景二:红色人工驾驶车辆加速行驶,黑色无人驾驶车辆减速后跟在人工驾驶车辆后方完成变道.
2.
3.
1数据采集及预处理首先,需要从传感器获取时空数据,我们将智能体采集到的数据划分为以下三种类型,如表1所示:(1)自身驾驶数据以及与周边人所驾驶的车辆的关系数据,主要包括自动驾驶车辆的速度、加速度,与周边车辆的相对速度、相对距离等;(2)周边人所驾驶的车辆的驾驶数据,主要包括车灯使用是否正确,刹车次数以及是否存在其他不规范的行车行为等;(3)周边环境中与车辆无关的信息数据,主要包括天气(例如:雨天、雾天、晴天等),时间(例如:白天、晚上、早晚高峰等),道路情况(例如:高速公路、城市道路、乡村道路等)等.
由于缺少实验条件,我们采用仿真的方式生成了近200条数据,https://github.
com/DongdongAn/DrivingStyleClassification.
git在此场景中,人的行为是间接通过车辆的行驶数据来体现的,所以我们对人类所驾驶车辆的行车行为分类即为对人工驾驶员的驾驶行为分类.
Table1Theinputdataset表1输入分类器的数据集类别数据1.
与周边车辆的相关数据1)自动驾驶车辆的速度2)相对距离3)相对速度4)周边车辆的速度5)速度差百分比0120km/h1m20m15km/h15km/h0120km/h10%2.
周边车辆其他数据1)车灯使用是否正确2)刹车次数3)其他不合规行为0使用正确;1使用错误0无刹车;1有刹车0无;1有3.
周围环境1)天气情况2)所处时间0雨天;1晴天;2雾天0夜晚;1白天驾驶行为分类正常Normal;轻度激进SlightlyAggressive;激进Aggressive2.
3.
2分类器效果评价如图3所示,散点图表示了不同驾驶行为的分类情况,不同颜色的点表示不同的分类结果.
如图4所示,在人工智能中,混淆矩阵(ConfusionMatrix)是可视化工具,特别用于监督学习.
混淆矩阵是通过将每个实测像元的位置和分类与分类图像中的相应位置和分类像比较计算的,从而刻画一个分类器的分类准确程度来验证分类结果的有效性.
如图5所示,平行坐标图(ParallelCoordinatesPlot)为一种数据可视化的方式.
横坐标的每个标记表示样本中的一个属性,如车速、相对距离、相对速度等.
纵坐标表示每个样本中该属性的值,相连而得的一个折线表示该样本.
蓝色红色黄色分别表示激进驾驶行为、危险驾驶行为和正常驾驶行为.
直线表示分类结果与输入时样本的预分类结果一致,虚线表示模型的分类结果与输入时样本的预分类结果不一致.
如图6所示,ROC(ReceiverOperatingCharacteristic)曲线的横坐标表示:1Specificity,伪正类率(Falsepositiverate,FPR),预测为安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证9正但实际为负的样本占所有负例样本的比例;纵坐标表示:Sensitivity,真正类率(Truepositiverate,TPR),预测为正且实际为正的样本占所有正例样本的比例.
表2给出了线下训练结果,每个模型训练后的准确率及其他相关信息都会被显示出来.
训练方法主要包括决策树(DecisionTrees),朴素贝叶斯(NaiveBayesClassifiers),支持向量机(SupportVectorMachines),最近邻KNN(NearestNeighborClassifiers)和组合分类器.
最终的结果显示,训练准确度较高的是朴素贝叶斯分类器.
对于训练好的模型,我们可以输入新的数据进行分类,采用样本预测,将线下训练好的模型将模型导出到工作空间,这样就可以利用模型来测试新的数据.
Fig.
3DifferentDrivingStyleClassificationResultFig.
4ConfusionMatrixoftheClassificationResult图3不同驾驶行为的分类情况图4混淆矩阵结果Fig.
5ParallelCoordinatesPlotResultFig.
6ROC(ReceiverOperatingCharacteristic)图5分类结果的平行坐标图图6ROC曲线结果3线下与线上验证相结合的动态验证方法在上一节我们得到UPPAALSMC可以验证的模型后,通过写入要验证的性质(Query),即可对模型进行验证.
但是,目前使用UPPAALSMC进行验的时间成本较高,通常需要十几秒钟甚至更多,对于复杂的系统很可能10JournalofSoftware软件学报由于要检测的状态过多而产生状态爆炸的问题.
由于本文所研究的无人驾驶系统的物理车辆是行驶在不确定且复杂多变的场景中,十几秒钟后才能出现的验证结果对于系统来说是难以接受的,若车辆不能及时地对周边环境做出反应,那对于无人驾驶车辆来说将造成无法承担的后果.
所以我们从机器学习流程中线下训练和线上学习的过程中得到启发,通过采取线下验证和线上验证相结合的方法,通过比较参数即可快速得出验证结果,从而达到动态实时的验证效果,进而保障系统在复杂环境中安全运行.
Table2Thelearningresultoftheclassificationlearner表2分类器学习结果统计模型准确率分类错误数量预测速度训练时间精细树中等树粗略树83.
7%83.
7%81.
6%2424272600obs/sec1700obs/sec1700obs/sec1.
1363sec5.
1248sec5.
0357sec精细KNN中等KNN粗略KNN余弦KNN三次KNN加权KNN79.
6%78.
9%76.
2%78.
9%76.
9%83.
7%3031353134241300obs/sec1900obs/sec1800obs/sec2200obs/sec2800obs/sec2400obs/sec4.
8949sec2.
0646sec2.
35sec3.
3747sec3.
2652sec3.
714sec朴素贝叶斯85.
5%22760obs/sec1.
6165sec线性SVM二次SVM三次SVM精细高斯SVM78.
9%81.
6%85.
0%76.
2%312722351200obs/sec960obs/sec1100obs/sec1400obs/sec3.
7311sec3.
8418sec4.
7813sec4.
6623sec装袋树子空间判别子空间KNNRUSBooosted树85.
0%82.
3%79.
6%76.
9%22263034200obs/sec170obs/sec130obs/sec230obs/sec11.
638sec12.
516sec12.
403sec12.
846sec图7显示了线下与线上结合的动态验证方法示意图.
上半部分显示的是线下的验证过程,下半部分是线上验证的过程.
在线下验证过程中,统计模型检测工具UPPAALSMC接受的是属性和NSHA模型,其中所要验证的属性基于不同场景下的安全需求进行形式化描述产生,而NSHA模型由上一节提出的环境感知模型和线下训练场景共同建模得到.
不断加入新的线下场景进行验证.
这样在线上验证过程中,通过对比相关安全数据,在验证结果库中查询之前线下已经验证出的结果,从而及时给系统反馈,达到实时地动态验证的效果,使得HCPS系统可以智能安全又及时应对复杂多变的不确定性环境.
对于训练好的驾驶行为分类模型,通过数据两组新的环境数据和人工驾驶车辆的行车数据,我们得到的人工驾驶行为预测结果为:在场景一时刻,_=的概率为85%,在场景二时刻,_=的概率是87%.
将以上结果作为参数集输入到后续的NSHA模型中.
安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证Fig.
7Offlineandonlineverificationmethod图7线下与线上验证相结合的动态验证方法3.
1构建NSHA模型将无人驾驶车辆进行建模,UPPAALSMC可以进行验证的型组成,分别是组合模型Composite,开始模型Start,风险模型型Autodrive.
因此随机混成自动机网络可以表示成:ChangeLane=Composite∪Start图8表示复合状态抽象成的SHA模型,主要包括个Urgent状态,在Urgent状态中时间不流失,会跳转到下一个状态见https://github.
com/DongdongAn/DrivingStyleClassification.
git3.
2采用UPPAALSMC对NSHA模型进行验证建立好NSHA模型后,接下来是对其进行验证.
首先需要结合(1)P1表示在15个时间单位内人工驾驶车辆允许无人驾驶车辆通过的概率预测结果为normaldriver时,图9表示在模拟了其中置信度为0.
97.
其中概率密度分布和累积分布概率密度和概率.
图11表示当人工驾驶风格分类模型预测结果为和累积分布的情况.
(2)P2表示在30个时间单位内无人驾驶车辆完成变道的概率driver时,P2性质的概率密度分布和累积分布情况aggressivedriver时,P2性质的概率密度分布Table表3变道案例中验证的安全性质列表序号P1Pr[HumanDrive.
LET_PASS)P2Pr[AutoDrive.
CHANGE_LANE)不确定环境下人机物融合系统的形式化建模与动态验证11Fig.
8CompositeStateofSHAmodel图8复合状态抽象成的SHA模型可以进行验证的NSHA模型.
所构建出的NSHA模型由五个子模风险模型EnvRisk,人工驾驶模型HumanDrive和无人驾驶模:∪EnvRisk∪HumanDrive∪Autodrive主要包括STOP,STRAIGHT和CHANGE_LANE三个状态和两会跳转到下一个状态.
由于篇幅限制,其他SHA模型建立过程详https://github.
com/DongdongAn/DrivingStyleClassification.
git,在此不一一列举.
首先需要结合PCTL公式定义所要验证的性质,如表3所示.
个时间单位内人工驾驶车辆允许无人驾驶车辆通过的概率.
当人工驾驶风格分类模型表示在模拟了1305次之后,所得的概率区间是[0.
549862,0.
609859],和累积分布如图10所示.
图中的x轴表示时间,y轴分别表示人工驾驶风格分类模型预测结果为aggressivedriver时,概率密度分布个时间单位内无人驾驶车辆完成变道的概率.
图12表示当学习出的结果是normal和累积分布情况.
图13表示当人工驾驶风格分类模型预测结果为分布和累积分布情况.
Table3Propertylist变道案例中验证的安全性质列表性质](HumanDrive.
LET_PASS)0](AutoDrive.
CHANGE_LANE)12Fig.
9Theverification图9当学习出的结果是normalFig.
10Theprobabilitydistributionandcumulativedistribution图10当学习出的结果是normaldriverFig.
11Theprobabilitydistributionandcumulativedistribution图11当学习出的结果是aggressivedriverJournalofSoftware软件学报verificationresultofP1fornormaldrivernormaldriver时性质P1的验证结果cumulativedistributionofP1fornormaldriverdriver时,P1性质的概率密度分布和累积分布情况cumulativedistributionofP1foraggressivedriveraggressivedriver时,P1性质的概率密度分布和累积分布情况安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证Fig.
12Theprobabilitydistributionandcumulativedistribution图12当学习出的结果是normaldriverFig.
13Theprobabilitydistributionandcumulativedistribution图13当学习出的结果是aggressivedriver3.
3采用参数比较法进行动态验证在上一节我们得到UPPAALSMC可以验证的模型后证.
上一小节的验证都是线上验证的,通过设置不同的参数结果.
由于在风险等级较高的环境中,需要保证车辆的安全说是难以接受的.
若车辆不能及时地对周边环境做出反应于场景A,Probabilityuncertainty参数为0.
01,我们得到了验证结果实时运行在场景B中,如果场景B的大部分指标与A量相对于场景A较少.
那么,我们则不再需要对场景BA的验证结果即可.
这样参数对比的方法,大大节省了线上验证的时间统在复杂环境中安全运行.
在得到验证结果后,接下来就是决策阶段了据验证结果来决定是否改变车道.
不确定环境下人机物融合系统的形式化建模与动态验证13cumulativedistributionofP2fornormaldriverdriver时,P2性质的概率密度分布和累积分布情况cumulativedistributionofP2foraggressivedriveraggressivedriver时,P2性质的概率密度分布和累积分布情况可以验证的模型后,通过写入要验证的性质(Query),即可对模型进行验通过设置不同的参数,可以对同一个模型进行多次验证,得到不同的验证需要保证车辆的安全,但是验证时间在二十几秒之后才能得到对于系统来出反应,那对于无人驾驶车辆来说将造成无法承担的后果.
对我们得到了验证结果.
那么我们将其存入我们的场景库中.
在车辆A相同,个别项比场景A还要宽松,例如在相同环境下,人流B进行耗时的线上验证,只要参考场景比B更严格的场景大大节省了线上验证的时间,达到动态实时的验证效果,进而保障系接下来就是决策阶段了,基于不同的驾驶环境,无人驾驶车辆根14JournalofSoftware软件学报(1)当车辆行驶在高速公路上,车速大于80km/h时,车辆换道的概率大于95%.
(2)当车辆行驶在城区,车速小于30km/h时,车辆换道的概率大于80%.
例如,上面案例中P1的结果为90%,如果所处的场景为高速公路,90%80%,可以进行变道.
可见不同场景下指定不同的动作阈值可保证系统在更安全的情况下进行决策并决定未来状态.
本节以无人驾驶车辆与人工驾驶车辆交互过程中变道过程为案例,首先基于上一节提出的基于机器学习的环境感知模型得到驾驶风格分类结果,接着基于SHA模型对无人驾驶汽车的运动状态进行了建模,并使用统计模型检测工具UPPAALSMC来验证所建立的NSHA模型.
4相关工作比较对于驾驶风格识别目前的研究尚处于起步阶段.
人和机器最大的不同在于人是有情绪的,有些驾驶员比较激进,有些比较稳重.
2016年,谷歌的自动驾驶汽车在换道时和迎面而来的巴士相撞,原因就是自动驾驶汽车以为巴士会减速,而巴士司机却加速了.
如果能事先知道司机的驾驶风格,并结合进行预测,这场事故也许是可以避免的.
当然,驾驶风格目前还没有一个准确的定义,因此分类的依据也有很多种,比如油耗,均速,跟车行为等.
将驾驶风格识别成功应用到真实的自动驾驶系统的目前还没有相关报道,但是这些研究可能是未来自动驾驶发展的一个方向.
2011年11月15日,首个适用于汽车电子电器相关的产品的功能安全标准ISO26262正式发布.
功能安全的设计议题在汽车领域开始受到重视.
为了更好地来量化驾驶场景的不确定性和风险水平来提高自动驾驶系统的安全性.
Geng等人[24]提出了利用贝叶斯方法来量化深度神经网络的不确定性的方法.
Gadepally等人[25]设计了一个贝叶斯深度学习框架,并在模拟场景中展示了它相对于传统方法的优势.
该方法是每个模块在系统中的传递和输入都服从概率分布函数,而不是一个精确的结果.
另一种方法是单独评估驾驶场景下的风险水平,可以理解为前者是从系统内部评估,后者是从系统外部评估.
Yamazaki等人[26]将传感器数据输入到一个风险推理框架中,利用隐马尔科夫模型(HiddenMarkovModels,HMMs)和语言模型检测不安全的车道变更事件.
Yurtsever[27]引入了一个深度时空网络来推断驾驶场景的总体风险水平,来评估车道变更的风险水平.
牛津大学的Wu等人[28]提出了基于双方回合博弈的(Twoplayerturnbasedgame)框架来对神经网络的验证,用于评估安全攸关自动驾驶系统对交通标志识别的准确性.
Wicke等人[29]研究了对抗性输入扰动下的贝叶斯神经网络BNN的概率安全性,基于非凸优化的技术,开发了用于计算概率安全性的算法框架,从而验证具有数千个神经元的概率安全性并应用于自动驾驶系统.
Huang等人[30]出了可以表达社会信任概念(如能力,性格和依赖性)的算子来扩展逻辑PCTL*为概率理性时间逻辑PRTL*,建立一个基于人的信任度的模型验证框架,可用于自动驾驶系统根据行人的反应进行决策.
Sun等人[31]通过将覆盖率指导的神经网络测试工具DeepConcolic与车辆跟踪系统集成,对深度神经网络(DeepNeuralNetworks,DNN)的进行了验证.
伯克利大学的Sanjit等人[32]提出了一种通过深度强化学习来改善布尔逻辑回溯搜索算法的方法,对使用ML进行感知的系统进行形式分析的方法.
在基于深度神经网络的感知组件的上显示了该技术的有效性.
实际环境中的自动驾驶决策还有周围驾驶员的意图与行为相关.
目前该技术在自动驾驶领域尚不常见.
Geng等人[33]用隐马尔可夫模型(HMM)对目标车辆的未来行为进行了预测,通过学习人类驾驶特征,将预测时间范围延长了56%.
这里主要是利用了预定义的移动行为来标记观测值,然后再使用HMM以数据位中心学习每种类型的特征.
除此之外,还有一些其他的方法,比如贝叶斯网络分类器,混合高斯模型和隐马尔科夫模型相结合[34],支持向量机等.
这一类评估的主要问题在于观测时间短,实时计算量要求高,大多数情况下,自动驾驶系统只能观测周围车辆几秒钟,因此不能使用需要较长观察周期的复杂模型.
针对不确定性的模型检测技术,关于随机模型检验的研究开始于20世纪80年代初,Harts等人[35]使用离散时间马尔科夫过程建模概率程序,研究概率并发程序的终止性质和概率程序性质的证明方法.
Vardi等人[26][37]提出基于自动机理论的定性线性时间性质的验证方法,Courcoubetis和Yannakakis[38]研究了线性时间安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证15框架下的定性、定量验证理算时间马尔科夫链.
英国牛津大学的Kwiatkowska团队开发出图形化随机模型检验工具PRISM[39],该工具可以验证包括DTMC,CTMC,MDP,PA,PTA及其reward扩展模型等多种类型的随机系统模型,其性质规约包括PCTL,CSL,概率LTL,PCTL*及其reward扩展等定量性质规约语言.
PRISM基于BDD(BinaryDecisionDiagrams)和MTBDD(MultiTerminalBinaryDecisionDiagrams)的符号数据结构和算法[40],通过离散事件模拟引擎来实现定量抽象精化和系统归约等验证技术,支持多目标定量性质的随机模型检验和统计随机模型检验[41].
德国亚琛工业大学Hartmanns等人提出了支持验证随机混成自动机、随机时间自动机的工具集MODEST[42].
通过为现有语言提供导入和导出功能,允许重复使用现有模型;并通过将它们集成在统一的建模和分析环境中来允许重复使用现有工具.
MRMC(MarkovRewardModelChecker)采用基于系数矩阵的数据结构和算法[43],支持精确的onthefly稳态检查和互模拟最小化等验证技术,其优势在于验证规模较小的连续时间随机系统的稳态性质效率较高.
Katoen等人近年来开发的工具Storm[44]支持对马尔可夫链和马尔可夫决策过程的离散和连续时间变体进行分析,支持包括JANI和PRISM建模语言,动态故障树,广义随机Petri网和概率保护的命令语言.
模块化设置可轻松交换求解器和符号引擎,通过封装PythonAPI使得Storm工具可以使用扩展的算法来实现快速原型制作.
丹麦乌普萨拉大学的研究人员Larsen和David等人基于随机混成自动机SHA,开发了统计模型验证工具UPPAALSMC[46],统计模型检测是一种高效的验证技术,常用于复杂的随机系统的验证.
该工具所采用的技术主要是参数估计式和假设检验.
目前使用上述工具所进行建模的系统需要设计人员在建模初期就确定好参数,以便验证.
但在不确定性环境中,参数是不断变化的,采用此种验证方法无法满足时效性的要求.
目前结合机器学习的统计验证模型框架的相关工作比较少,缺乏统一的理论框架.
5总结与展望为了提高无人驾驶系统面对不确定环境的"智能性",本文提出了时空数据驱动的基于朴素贝叶斯分类器的周边人工驾驶行为分类模型DSC.
基于朴素贝叶斯的分类算法对周边人工驾驶车辆的驾驶行为进行分类并将学习器的学习结果作为参数输入到后续的系统模型中.
为了提高无人驾驶系统面对不确定环境的"安全性",我们从模型驱动的角度出发,构建结合了人工驾驶行为分类模型的计算结果的NSHA模型.
通过将NSHA模型和需要验证的性质共同输入进统计模型验证工具UPPAALSMC来对系统模型进行验证.
为了提高验证模型的效率,我们从机器学习流程中线下训练和线上学习的过程中得到启发,采用线下验证和线上验证相结合的方法,通过比较参数可快速得出验证结果,实现动态验证,从而帮助HCPS系统面对复杂多变的不确定性环境可以更及时地进行决策.
综上,我们对机器学习和形式化方法的交叉领域展开了探索研究.
整个过程展现了从机器学习、模型构建到统计模型验证.
在接下来的工作中,我们需要从以下几点进行拓展:由于条件限制,目前大多研究关注于无人驾驶车本身的数据采集,对周边车辆的监控数据通过识别或者对比来判断危险情况,存在一定的风险.
目前无人驾驶车辆还没有"智能"到可以预判周边人类驾驶员的行为.
近一年已经有学者在对相关问题展开研究,例如卡内基梅隆大学相关学者对周边车辆的相关数据进行了采集但是还未开放.
在今后的工作中,我们需要模拟不同情况下的危险驾驶行为的相关数据,从而帮助建立更完善的模型.
目前我们使用的是统计模型检测的工具UPPAALSMC.
暂时没有与其他高效率的验证工具进行对比,例如概率模型检测工具PRISM.
在接下来的工作中,我们考虑使用不同的工具进行验证.
目前的工作是基于监督学习的,由于强化学习在交互方面表现良好,未来我们考虑建立基于强化学习的人工驾驶行为分类模型,从而帮助无人驾驶车辆更智能地应对复杂的环境.
References:[1]LeeEA.
Cyberphysicalsystems:Designchallenges.
InProcofthe11thIEEEInternationalSymposiumonObjectandComponentOrientedRealTimeDistributedComputing(ISORC).
2008:363369.
[DOI:10.
1109/ISORC.
2008.
25][2]RobinsonRM,ScobeeDRR,BurdenSA,etal.
Dynamicinversemodelsinhumancyberphysicalsystems.
ProceedingsofSPIE,2016,9836.
[DOI:10.
1117/12.
2223176]16JournalofSoftware软件学报[3]LevesonNG.
Softwaresafety:why,what,andhow[J].
ACMComputingSurveys,1986,18(2):125163.
[DOI:10.
1145/7474.
7528][4]SunHY.
SafetySoftwareTestingBasedonMultiformClocksInputOutputTransitionSystem[Ph.
D.
Thesis].
Shanghai:EastChinaNormalUniversity,2017(inChinesewithEnglishabstract).
[5]SchirnerG,ErdogmusD,ChowdhuryKR,etal.
Thefutureofhumanintheloopcyberphysicalsystems[J].
IEEEComputer,2013,46(1):3645.
[DOI:10.
1109/MC.
2013.
31][6]GeigerA,LenzP,UrtasunR.
Arewereadyforautonomousdrivingthekittivisionbenchmarksuite.
ProceedingoftheIEEEconferenceonComputerVisionandPatternRecoginition(CVPR)2012:33543361.
[7]ElsayedGF,ShankarS,CheungB,etal.
Adversarialexamplesthatfoolbothcomputervisionandtimelimitedhumans.
AnnualConferenceonNeuralInformationProcessingSystems,NeurIPS2018,39143924.
[8]Finlayson,S.
G.
,Bowers,J.
D.
,Ito,J.
,Zittrain,J.
L.
,Beam,A.
L.
,Kohane,I.
S.
Adversarialattacksonmedicalmachinelearning.
Science,2019363(6433),12871289.
[DOI:10.
1126/science.
aaw4399][9]BanksVA,PlantKL,StantonNA.
Drivererrorordesignererror:Usingtheperceptualcyclemodeltoexplorethecircumstancessurroundingthefatalteslacrashon7thmay2016.
SafetyScience,2017,108:278285.
[DOI:10.
1016/j.
ssci.
2017.
12.
023][10]KohliP,ChadhaA.
Enablingpedestriansafetyusingcomputervisiontechniques:Acasestudyofthe2018uberinc.
selfdrivingcarcrash.
FutureofInformationandCommunicationConference,2019:261279.
[DOI:10.
1007/9783030123888_19][11]WoodcockJ,LarsenPG,BicarreguiJ,etal.
Formalmethods:Practiceandexperience.
ACMComputingSurveys,2009,41(4):19.
[DOI:10.
1145/1592434.
1592436][12]AbrialJ.
Formalmethods:Theorybecomingpractice.
JournalofUniversalComputerScience,2007,13:619628.
[13]BicarreguiJC,FitzgeraldJS,LarsenPG,etal.
Industrialpracticeinformalmethods:AreviewInternationalSymposiumonFormalMethods.
Springer,2009:810813.
[DOI:10.
1007/9783642050893_52][14]ClarkeJrEM,GrumbergO,KroeningD,etal.
Modelchecking[M].
MITpress,2018.
[15]LegayA,DelahayeB,BensalemS.
Statisticalmodelchecking:anoverview.
InInternationalconferenceonruntimeverificationSpringer,Berlin,Heidelberg.
2010.
122135.
[DOI:10.
1007/9783642166129_11][16]DuDH,ChengB,LiuJ.
Statisticalmodelcheckingforrareeventinsafetycriticalsystem.
RuanJianXueBao/JournalofSoftware,2015,26(2):305320(inChinese).
[17]ZulianiP,PlatzerA,ClarkeEM.
Bayesianstatisticalmodelcheckingwithapplicationtostateflow/simulinkverification.
FormalMethodsinSystemDesign,2013,43(2):338367.
[DOI:10.
1145/1755952.
1755987][18]DuDH,ZanH,JiangKQ,ChengB.
SelfAdaptivestatisticalmodelcheckingapproachforCPS.
RuanJianXueBao/JournalofSoftware,2017,28(5):11281143(inChinese)[19]DavarzaniS,NagahiM,TidwellM,etal.
Patternrecognitionusingmachinelearningforcornandsoybeanyieldprediction.
proceedingofthe2020IISE,NewOrleans,LA,USA,2020.
[20]JuliusAA,PappasGJ.
Approximationsofstochastichybridsystems.
IEEETransactionsonAutomaticControl,2009,54(6):11931203.
[DOI:10.
1109/TAC.
2009.
2019791][21]DavidA,LarsenKG,LegayA,etal.
Statisticalmodelcheckingofdynamicnetworksofstochastichybridautomata.
FranciscoJavierFuenteFernández,2014,66:91104.
[DOI:10.
14279/tuj.
eceasst.
66.
893.
878][22]LlerenaYRS,SuG,RosenblumDS.
ProbabilisticmodelcheckingofperturbedmdpswithapplicationstocloudcomputingProceedingsofthe201711thJointMeetingonFoundationsofSoftwareEngineering.
ACM,2017:454464.
[DOI:10.
1145/3106237.
3106301][23]ZhaoX,RobuV,FlynnD,etal.
Probabilisticmodelcheckingofrobotsdeployedinextremeenvironments.
ProceedingsoftheAAAIConferenceonArtificialIntelligence:2019(33):80668074.
[DOI:10.
1609/aaai.
v33i01.
33018066][24]GalY.
Uncertaintyindeeplearning.
[Ph.
D.
Thesis]UniversityofCambridge,2016.
[25]McAllisterR,GalY,KendallA,etal.
Concreteproblemsforautonomousvehiclesafety:Advantagesofbayesiandeeplearning:InternationalJointConferencesonArtificialIntelligence,2017.
[DOI:10.
24963/ijcai.
2017/661]安冬冬等:不确定环境下人机物融合系统的形式化建模与动态验证17[26]YamazakiS,MiyajimaC,YurtseverE,etal.
Integratingdrivingbehaviorandtrafficcontextthroughsignalsymbolization.
IEEEIntelligentVehiclesSymposium(IV).
IEEE,2016:642647.
[DOI:10.
1109/IVS.
2016.
7535455][27]YurtseverE,LiuY,LambertJ,etal.
Riskyactionrecognitioninlanechangevideoclipsusingdeepspatiotemporalnetworkswithsegmentationmasktransfer.
IEEEIntelligentTransportationSystemsConference(ITSC).
IEEE,2019:31003107.
[DOI:10.
1109/ITSC.
2019.
8917362][28]WuM,WickerM,RuanW,etal.
Agamebasedapproximateverificationofdeepneuralnetworkswithprovableguarantees.
TheoryComputerScience,2020,807:298329.
[DOI:10.
1016/j.
tcs.
2019.
05.
046][29]WickerM,LaurentiL,PataneA,etal.
Probabilisticsafetyforbayesianneuralnetworks.
CoRR,2020,abs/2004.
10281.
[30]HuangX,KwiatkowskaM,OlejnikM.
Reasoningaboutcognitivetrustinstochasticmultiagentsystems.
ACMTransactionsonCompututationLogic.
2019,20(4):21:121:64.
[DOI:10.
1145/3329123][31]SunY,ZhouY,MaskellS,etal.
Reliabilityvalidationoflearningenabledvehicletracking.
IEEEInternationalConferenceonRoboticsandAutomation(ICRA)2020.
93909396[DOI:10.
1109/ICRA40945.
2020.
9196932][32]LedermanG,RabeMN,SeshiaS,etal.
Learningheuristicsforquantifiedbooleanformulasthroughreinforcementlearning.
InternationalConferenceonLearningRepresentations,ICLR.
2020.
[33]DreossiT,DonzéA,SeshiaSA.
Compositionalfalsificationofcyberphysicalsystemswithmachinelearningcomponents.
JournalofAutomatedReasoning,2019,63(4):10311053.
[DOI:10.
1007/s10817018095095][34]GengX,LiangH,YuB,etal.
Ascenarioadaptivedrivingbehaviorpredictionapproachtourbanautonomousdriving.
AppliedSciences,2017,7(4):426.
[DOI:10.
3390/app7040426][35]AugustynowiczA.
Preliminaryclassificationofdrivingstylewithobjectiverankmethod.
Internationaljournalofautomotivetechnology,2009,10(5):607610.
[DOI:10.
1007/s1223900900718][36]HartS,SharirM,PnueliA.
Terminationofprobabilisticconcurrentprograms:(extendedabstract)Symposiumonprinciplesofprogramminglanguages.
1982:16.
[DOI:10.
1145/582153.
582154][37]VardiMY.
Automaticverificationofprobabilisticconcurrentfinitestateprograms.
Foundationsofcomputerscience.
1985:327338.
[DOI:10.
1109/SFCS.
1985.
12][38]VardiMY,WolperP.
Anautomatatheoreticapproachtoautomaticprogramverification.
ProceedingsoftheFirstSymposiumonLogicinComputerScience.
IEEEComputerSociety,1986:322331.
[39]CourcoubetisC,YannakakisM.
Thecomplexityofprobabilisticverification.
JournaloftheACM,1995,42(4):857907.
[DOI:10.
1145/210332.
210339][40]KwiatkowskaM,NormanG,ParkerD.
PRISM4.
0:Verificationofprobabilisticrealtimesystems.
InternationalConferenceonComputerAidedVerification(CAV).
2011:585591.
[DOI:10.
1007/9783642221101_47][41]KwiatkowskaM,NormanG,ParkerD.
Probabilisticsymbolicmodelcheckingwithprism:ahybridapproachInternationalJournalonSoftwareToolsforTechnologyTransfer.
SpringerVerlag,2001.
[DOI:10.
1007/s1000900401402][42]KwiatkowskaM.
Quantitativeverification:modelstechniquesandtools.
Proceedingsofthethe6thjointmeetingoftheEuropeansoftwareengineeringconferenceandtheACMSIGSOFTsymposiumonThefoundationsofsoftwareengineering.
2007:449458.
[DOI:10.
1145/1295014.
1295018][43]HartmannsA,HermannsH.
Themodesttoolset:Anintegratedenvironmentforquantitativemodellingandverification.
InternationalConferenceonToolsandAlgorithmsfortheConstructionandAnalysisofSystems.
Springer,2014:593598.
[DOI:10.
1007/9783642548628_51][44]KatoenJP,ZapreevIS,HahnEM,etal.
Theinsandoutsoftheprobabilisticmodelcheckermrmc.
PerformanceEvaluation,2011,68(2):90104.
[DOI:10.
1016/j.
peva.
2010.
04.
001][45]HenselC,JungesS,KatoenJ,etal.
Theprobabilisticmodelcheckerstorm.
CoRR,2020,abs/2002.
07080.
[46]DehnertC.
,JungesS.
,KatoenJP.
,VolkM.
AStormisComing:AModernProbabilisticModelChecker.
InternationalConferenceonComputerAidedVerification(CAV)2017[DOI:10.
1007/9783319633909_31]18JournalofSoftware软件学报附中文参考文献:[4]孙海英.
基于多形态时钟输入输出迁移系统的安全软件测试研究[博士学位论文].
华东师范大学,2017.
[16]杜德慧,程贝,刘静.
面向安全攸关系统中小概率事件的统计模型检测.
软件学报,2015,26(2):305320.
[18]杜德慧,昝慧,姜凯强,程贝.
一种面向CPS的自适应统计模型检测方法.
软件学报,2017,28(5):11281143.
腾讯云轻量服务器老用户续费优惠和老用户复购活动
继阿里云服务商推出轻量服务器后，腾讯云这两年对于轻量服务器的推广力度还是比较大的。实际上对于我们大部分网友用户来说，轻量服务器对于我们网站和一般的业务来说是绝对够用的。反而有些时候轻量服务器的带宽比CVM云服务器够大，配置也够好，更有是价格也便宜，所以对于初期的网站业务来说轻量服务器是够用的。这几天UCLOUD优刻得香港服务器稳定性不佳，于是有网友也在考虑搬迁到腾讯云服务器商家，对于轻量服务器官方...
香港云服务器 1核 1G 29元/月 快云科技
快云科技: 12.12特惠推出全场VPS 7折购 续费同价 年付仅不到五折公司介绍：快云科技是成立于2020年的新进主机商，持有IDC/ICP等证件资质齐全主营产品有：香港弹性云服务器，美国vps和日本vps，香港物理机，国内高防物理机以及美国日本高防物理机产品特色：全配置均20M带宽，架构采用KVM虚拟化技术，全盘SSD硬盘，RAID10阵列， 国内回程三网CN2 GIA,平均延迟50ms以下。...
819云互联(800元/月),香港BGP E5 2650 16G,日本 E5 2650 16G
819云互联 在本月发布了一个购买香港，日本独立服务器的活动，相对之前的首月活动性价比更高，最多只能享受1个月的活动 续费价格恢复原价 是有些颇高 这次819云互联与机房是合作伙伴 本次拿到机房 活动7天内购买独立服务器后期的长期续费价格 加大力度 确实来说这次的就可以买年付或者更长时间了…本次是5个机房可供选择，独立服务器最低默认是50M带宽，不限制流量，。官网：https://ww...
网络测速工具为你推荐
-
计算机xp支持ipad支持ipad步骤iosDeviceios5重庆宽带测速重庆电信测速我的网速溢出win10445端口Win10系统开放端口号怎样查看？itunes备份itunes 里面的资料如何备份?iphonewifi苹果手机怎么wi-fi共享win7如何关闭445端口如何关闭WIN7自动配置 IPV4 地址 169.254