订阅程序员杂志RSS CSDN首页> 程序员杂志

火星代码

发表于2014-03-07 11:48| 次阅读| 来源《程序员》| 0 条评论| 作者CACM

摘要:随着火星探测的使命日趋复杂,航天飞行器的硬件和软件规模及复杂性都有所增加。本文侧重介绍了飞行器软件设计中使用的预防措施:基于风险的编码规则、基于工具的编码审查以及逻辑模型检查。

随着火星探测的使命日趋复杂,航天飞行器的硬件和软件规模及复杂性都有所增加。比如MSL(火星科学实验室,即“好奇号”)承载的代码比之前所有登月飞行器总和还多。不像普通的嵌入式软件,航天飞行器的软件是仅有单一任务且针对独立对象的罕见阵列,并且只编写使用一次,在测试阶段也仅有一次机会,要求对测试环境把控极端精确。一个微小编码错误可能带来的损失不仅仅是丢失重要的太阳系数据,更可能是巨大资金甚至声誉的损失。本文侧重介绍一些在如MSL的飞行器软件设计中使用的预防措施,这些措施一般是不常见的。下面主要介绍三个侧重点:基于风险的编码规则、基于工具的编码审查以及逻辑模型检查。

基于风险的编码规则(Risk-based Coding Rules)首先要查明什么类型的错误最常出现在目标领域内。因为大部分关于航天领域的任务异常数据已公开,所以查找起来并不难。一种常见错误是因为动态内存分配问题,起因是太空探索初期使用的动态内存覆盖。在MSL中我们使用的编码是风险相关而不是样式相关的。我们的JPL编码有两点设计规则,首先其必须与之前的任务观测到的异常编码直接风险关联,其次编码规则必须通过工具编码审查。我们开发的编码标准符合不同等级的规则,并适用于相对应类型的软件。六个等级的规则分别是:基本开发语言的规则,预测在嵌入式系统中执行的规则,代码定义的规则,关键人物的代码规则,MISRA C编码中“应当(shall)”级别的编码规则以及“必须(should)”级别的编码规则。


基于工具的代码审查(Tool Based Code Review)设计更多的可能的方式去拦截代码缺陷,并及早地使用它们十分重要。传统意义上的同等代码复查仅适用于少量代码。对于审查几百万行的代码利用这种方式会严重损耗系统。这时,静态代码分析器就可以派上用场,它可以不厌其烦地反复检查相同类型的代码区域并耐心地报告所有错误代码。建立MSL的运行任务时我们挑选了四个市场上常用的静态代码分析工具。从对MSL代码审查的统计显示绝大多数的意见和工具审核报告可以立刻将程序合理修改,无须单独审阅,这样节省下来的大量时间可以在最终提交前将关键模型多次审核。

模型检验(Model Checking)是用于分析多线程代码逻辑检测的最好的检验方式。在MSL中120个并行任务被同一个实时操作系统控制器控制完成,线程竞争经常存在。我们使用一个逻辑模型检测器叫做Spin,它专门验证分布式系统软件及异步线程,用来发现违反用户定义的执行程序。我们分析了MSL任务的几个关键软件组件,包括一个双CPU启动控制算法、闪存文件系统及数据管理子系统。实践证明用我们研发的软件模型检查机制,可以有效地减小飞行中的风险。

原文链接:http://cacm.acm.org/magazines/2014/2/171689-mars-code/fulltext

0
0

近期活动

更多

2015中国大数据技术大会

为了更好帮助企业深入了解国内外最新大数据技术,掌握更多行业大数据实践经验,进一步推进大数据技术创新、行业应用和人才培养,2015年12月10-12日,由中国计算机学会(CCF)主办,CCF大数据专家委员会承办,中国科学院计算技术研究所、北京中科天玑科技有限公司及CSDN共同协办的2015中国大数据技术大会(Big Data Technology Conference 2015,BDTC 2015)将在北京新云南皇冠假日酒店隆重举办。

微博关注

程序员移动端订阅下载

相关热门文章