针对无人机系统安全的新型层级式软件架构

朱晓蕊; 梁辰; 殷振国; 邵中; 刘孟启; 陈昊

doi:10.1631/FITEE.1800636

Your Location：

Home >

Browse articles >

针对无人机系统安全的新型层级式软件架构

智能机器人专题 | Updated：2022-05-19

- 针对无人机系统安全的新型层级式软件架构
- A new hierarchical software architecture towards safety-critical aspects of a drone system
- 信息与电子工程前沿（英文） 2019年20卷第3期页码：353-362
- Affiliations：
  
  Department of Mechanical Engineering and Automation, Harbin Institute of Technology (Shenzhen), Shenzhen 518055, China
  Department of Computer Science, Yale University, New Haven 06511, USA
- Author bio：
  
  Xiao-rui ZHU, E-mail: xiaoruizhu@hit.edu.cn
  [ "Zhong SHAO, E-mail: zhong.shao@yale.edu" ]
- Funds：
  
  Project supported by the National Natural Science Foundation of China (No. 91648012) and Shenzhen Science, Technology, and Innovation Comission, China (No. JCYJ20160401100022706)
- DOI：10.1631/FITEE.1800636
  中图分类号： V279;TP311.5
- 收稿：2018-10-12，
  
  修回：2019-;3-14，
  
  纸质出版：2019-03
- Accepted：
Scan QR Code
朱晓蕊, 梁辰, 殷振国, 等. 针对无人机系统安全的新型层级式软件架构[J]. 信息与电子工程前沿（英文）, 2019,20(3):353-362.

Xiao-rui ZHU, Chen LIANG, Zhen-guo YIN, et al. A new hierarchical software architecture towards safety-critical aspects of a drone system[J]. Frontiers of Information Technology & Electronic Engineering, 2019, 20(3): 353-362.
朱晓蕊, 梁辰, 殷振国, 等. 针对无人机系统安全的新型层级式软件架构[J]. 信息与电子工程前沿（英文）, 2019,20(3):353-362. DOI： 10.1631/FITEE.1800636.

Xiao-rui ZHU, Chen LIANG, Zhen-guo YIN, et al. A new hierarchical software architecture towards safety-critical aspects of a drone system[J]. Frontiers of Information Technology & Electronic Engineering, 2019, 20(3): 353-362. DOI： 10.1631/FITEE.1800636.

摘要

提出一种覆盖底层源代码到上层用户任务代码的新型层级式软件架构，用于提高无人机系统安全性与可靠性。每个软件模块采用形式化验证方法，验证其源代码是否符合设计规范，软件模块基于经过形式化验证的操作系统内核（certified kit operating system，CertiKOS），防止无人机由于意外软件故障而坠毁。考虑到无人机的机载传感器会对系统可靠性产生显著影响，对驱动传感器SPI总线与I2C总线形式化验证，并针对总线异常情况设计完成相关实验。实验结果表明，该软件架构能够有效提高无人机系统安全性与可靠性。

Abstract

A new hierarchical software architecture is proposed to improve the safety and reliability of a safetycritical drone system from the perspective of its source code. The proposed architecture uses formal verification methods to ensure that the implementation of each module satisfies its expected design specification

so that it prevents a drone from crashing due to unexpected software failures. This study builds on top of a formally verified operating system kernel

certified kit operating system (CertiKOS). Since device drivers are considered the most important parts affecting the safety of the drone system

we focus mainly on verifying bus drivers such as the serial peripheral interface and the inter-integrated circuit drivers in a drone system using a rigorous formal verification method. Experiments have been carried out to demonstrate the improvement in reliability in case of device anomalies.

关键词

Keywords

references

R Barry . . The FreeRTOS TM Kernel , , 2003 . . https://www.freertos.org/ https://www.freertos.org/ , , [Accessed on Feb. 12, 2019]. . .

B Bohrer , , , YK Tan , , , S Mitsch , , , 等 . . Veriphy: verified controller executables from verified cyber-physical system models . . Proc 39 th ACM SIGPLAN Conf on Programming Language Design and Implementation , , 2018 . . p.617 - - 630 . . DOI: 10.1145/3296979.3192406 http://doi.org/10.1145/3296979.3192406 . .

H Chen , , , XN Wu , , , Z Shao , , , 等 . . Toward compositional verification of interruptible OS kernels and device drivers . . Proc 37 th ACM SIGPLAN Conf on Programming Language Design and Implementation , , 2016 . . p.431 - - 447 . . DOI: 10.1145/2908080.2908101 http://doi.org/10.1145/2908080.2908101 . .

HG de Marina , , , FJ Pereda , , , JM Giron-Sierra , , , 等 . . UAV attitude estimation using unscented Kalman filter and TRIAD . . IEEE Trans Ind Electron , , 2012 . . 59 ( ( 11 ): ): 4465 - - 4474 . . DOI: 10.1109/TIE.2011.2163913 http://doi.org/10.1109/TIE.2011.2163913 . .

RH Gu , , , J Koenig , , , T Ramananandro , , , 等 . . Deep specifications and certified abstraction layers . . Proc 42 nd Annual ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages , , 2015 . . p.595 - - 608 . . DOI: 10.1145/2676726.2676975 http://doi.org/10.1145/2676726.2676975 . .

T Lee , , , M Leok , , , NH McClamroch . . Geometric tracking control of a quadrotor UAV on SE(3) . . 49 th IEEE Conf on Decision and Control , , 2010 . . p.5420 - - 5425 . . DOI: 10.1109/CDC.2010.5717652 http://doi.org/10.1109/CDC.2010.5717652 . .

JG Leishman . . Principles of Helicopter Aerodynamics . . Cambridge University Press, Cambridge, UK , , 2002 . . .

X Leroy . . Formal verification of a realistic compiler . . Commun ACM , , 2009 . . 52 ( ( 7 ): ): 107 - - 115 . . DOI: 10.1145/1538788.1538814 http://doi.org/10.1145/1538788.1538814 . .

SOH Madgwick , , , AJL Harrison , , , R Vaidyanathan . . Estimation of IMU and MARG orientation using a gradient descent algorithm . . IEEE Int Conf on Rehabilitation Robotics , , 2011 . . p.1 - - 7 . . DOI: 10.1109/ICORR.2011.5975346 http://doi.org/10.1109/ICORR.2011.5975346 . .

G Malecha , , , D Ricketts , , , MM Alvarez , , , 等 . . Towards foundational verification of cyber-physical systems . . Science of Security for Cyber-Physical Systems Workshop , , 2016 . . p.1 - - 5 . . DOI: 10.1109/soscyps.2016.7580000 http://doi.org/10.1109/soscyps.2016.7580000 . .

G Nutt . . Nuttx Real-Time Operating System , , 2007 . . http://nuttx.org http://nuttx.org , , [Accessed on Feb. 12, 2019]. . .

I Réti , , , M LukȢtsi , , , B Vanek , , , 等 . . Smart mini actuators for safety critical unmanned aerial vehicles . . Conf on Control and Fault-Tolerant Systems , , 2013 . . p.474 - - 479 . . DOI: 10.1109/SysTol.2013.6693929 http://doi.org/10.1109/SysTol.2013.6693929 . .

D Ricketts , , , G Malecha , , , MM Alvarez , , , 等 . . Towards verification of hybrid systems in a foundational proof assistant . . ACM/IEEE Int Conf on Formal Methods and Models for Codesign , , 2015 . . p.248 - - 257 . . DOI: 10.1109/MEMCOD.2015.7340492 http://doi.org/10.1109/MEMCOD.2015.7340492 . .

AJ Simpson , , , J Stoker . . Safety challenges in flying UAVs (unmanned aerial vehicles) in non segregated airspace . . IET Int Conf on System Safety , , 2006 . . p.81 - - 88 . . DOI: 10.1049/cp:20060206 http://doi.org/10.1049/cp:20060206 . .

KC Wang . . Embedded real-time operating systems . . In: Wang KC (Ed.), Embedded and Real-Time Operating Systems. Springer, Cham, Germany , , 2017 . . p.401 - - 475 . . DOI: 10.1007/978-3-319-51517-5_10 http://doi.org/10.1007/978-3-319-51517-5_10 . .

浏览量

Downloads

CSCD

文章被引用时，请邮件提醒。

Submit

工具集

关联资源

暂无数据