计算机科学 ›› 2017, Vol. 44 ›› Issue (4): 72-74.doi: 10.11896/j.issn.1002-137X.2017.04.015
刘斌斌,刘万伟,毛晓光,董威
LIU Bin-bin, LIU Wan-wei, MAO Xiao-guang and DONG Wei
摘要： 无人驾驶车辆技术是当前科学研究的重点领域之一,目前无人车决策系统的开发过程中面临着安全性不足的问题。针对该问题,提出了验证驱动的基于代码自动生成的无人车决策系统开发框架。该框架利用模型检验技术对无人车决策系统进行环境建模,通过验证可以发现无人车决策系统的设计过程中不易发觉的缺陷,解决其安全性不足的问题,同时能够将安全检查与软件开发同步,降低其维护成本。基于该框架,设计并实现了无人车决策系统辅助开发工具UNMANNED_RULE_EDIT(URE),目前该工具已初步应用于国内某单位研制的无人车上,为其开发研制工作提供了帮助。
| [1] LAN Y,LIU W W,DONG W,et al.Research on the Rule Editing and Code Generation for the High-Level Decision System of Unmanned Vehicles [J].Computer Engineering and Science,2015,37(8):1510-1516.(in Chinese) 兰韵,刘万伟,董威,等.无人驾驶汽车决策系统的规则描述与代码生成方法[J].计算机工程与科学,2015,37(8):1510-1516. [2] LIN H M,ZHANG W H.Model Checking:Theories,Techni-ques and Applications [J].Journal of Electronics,2002,30(12):1907-1912.(in Chinese) 林惠民,张文辉.模型检测:理论,方法与应用[J].电子学报,2002,30(12):1907-1912. [4] YANG J J.Study on SAT-based Bounded Model Checking and its Applications [D].Guangzhou:Sun Yat-sen University,2008.(in Chinese) 杨晋吉.基于SAT 的有界模型检验及其应用研究[D].广州 :中山大学,2008. [5] SHEN S Y.Explaining Counter Example of Model Checking[D].Changsha:University of Defense Technology,2005.(in Chinese) 沈胜宇.模型检验的反例解释[D].长沙:国防科学技术大学,2005 [6] PNUELI A.The Temporal Logic of Programs [C]∥Proc.of18th IEEE Symposium on Foundation of Computer Science (FOCS’ 77).1977:46-57. [7] EMERSON E A,CLARKE E M.Characterizing CorrectnessProperties of Parallel Programs Using Fixpoints [C]∥Proc.of the 7th Int.Colloquium on Automata,Languages and Programming (ICALP’80).1980:169-181. |
| No related articles found! |
|
||
首页