您的位置:首页 > 其它

Ada语言适合实时安全关键需求

2009-11-19 12:51 197 查看
Ada语言适合实时安全关键需求

作者:BENJAMIN M. BROSGOL, SENIOR TECHNICAL STAFF ADACORE
,2009年7月
原文:http://www.cotsjournalonline.com/magazine/articles/view/100982/pg:1
译者:logiciel,2009年11月19日

开发军用系统的实时软件是困难的。在这种系统中,正确性不仅意味着计算正确的结果,而且是要在规定的时间间隔内完成计算。当系统是安全关键的,事情更难。为了满足如DO - 178B那样的标准,军用系统开发商需要向合格审定机构有力地证明系统执行了应该执行的任务,并且没有执行不应该执行的任务。编程语言作为表述系统的媒介,直接影响到减轻或增加执行这一任务的难度。
Ada一开始就是为开发实时和安全关键系统而设计的。随着它的演变,无论在提供功能的方面,以及允许用户省略功能这一同等重要的方面,它在继续实现这一目标。在国防工业中的实时和安全关键的应用方面,Ada有良好记录,并提供了最满足业界需要的语言技术。
实时问题
一个系统是实时的,如果它的正确性涉及满足时间约束,或者更简单地说,满足截止时间。一个实时系统与外部世界相连,并执行一些诸如设备监测/控制的任务。如果错过截止时间意味着任务的完全丧失,这是硬实时。如果错过了最后期限包含的一些目标,但允许该任务能够继续执行,这是软实时。实时程序的截止时间的通常范围从毫秒到秒。一个实时系统是安全关键的,如果它的失效可以直接导致人的生命的丧失或严重的环境破坏。
并行和异步活动
实时安全关键软件的开发要比其它类型的系统困难得多。首先,它通常要处理并发和异步的活动,这比纯粹的顺序应用编程复杂得多。其次,开发者必须通过系统保证的有说服力的演示来表明满足安全关键行业提出的认证要求,这包括健全的开发过程的证据,或最终产品的正确性和安全性,或包括这两者。例如,DO- 178B标准的最高安全级别要求表明从需求到代码和从代码到需求的可追溯性,并通过软件的覆盖分析表明没有“死代码”(指应用程序中存在的不能对应到任何需求的代码)。
实时和安全关键系统的编程语言的选择会影响工作,从而影响到软件的成本、开发和认证。编程语言必须满足以下几种要求:
可靠性:语言应该有防止产生错误和帮助检测漏网错误的功能。这意味着没有“陷阱和缺陷”(指效果不直观的功能),具有捕获错误的检查,如在开发过程的早期发现类型不匹配,以及更普遍的,支持健全的软件工程原则,如封装。
分析性:应该有可能从(手动或自动)检查源程序文本推断出的程序的正确性和安全性。与此有关的特性包括可预测的时间和空间、数据流约束、控制流约束和无歧义行为的保证。
可表达性:语言应包含通过内置的功能和标准库的组合来编制可靠、长寿命的实时程序的功能。语言应该提供并发支持、异常处理、时间管理、访问硬件特定功能的低级别设施,或许如定点算术这样的专用功能。一般用于大型系统的构建和维护的功能,如面向对象编程和灵活的命名空间管理,也很有用。
一个直接的问题是这些要求有冲突。由于语义的复杂性以及隐含地包含更多的库代码,增强通用性和表达能力的功能使程序更加难以分析,或缺乏从源代码到目标代码的可追溯性。在实践中,为避免这些问题,选择语言子集和专门剪裁的运行库使之可以认证。
接下来的问题是编程语言如何引导这种权衡:为了以一种自然的方式表达实时程序要提供足够的通用性,但为了分析最终代码是否符合安全关键标准要对功能/库的使用执行足够的限制。Ada对这一难题提供了一个独特的解决方案,它允许项目按特定的应用来决策这种权衡。
从底向上的实时
Ada从一开始就支持实时和安全关键系统,并使用传统和保守的运行时模型。简言之,Ada是一个强类型的分程序结构语言,其功能包括异常处理、并发性(任务)、模块化(包)、层次命名空间、面向对象编程、通用的模板和低级机制。它还包括一个与其它语言(例如C)接口的标准设施,一个广泛的预定义库集合,以及支持系统编程、实时系统、分布式系统、信息系统、数值和高集成度系统的专门附件。Ada语言最初在80年代由国际标准化组织制订了标准,随后经历了两个修订。Ada语言的现行版本的标准被称为Ada2005。
一个Ada程序通常包含一个主过程和它间接或直接依赖的包。当程序启动时,将执行数据初始化和包中其它可执行的构造(“展开”),然后调用主要程序。Ada程序结构的一个例子如图1所示。



图1 Ada程序结构示例
Ada程序可能包含一个或多个控制线程(任务)。有一个“静态”区域包含顶层包内声明的数据,堆栈(每个任务一个)和一个堆。与Java不同,过程和函数内声明的数据对象在栈中,没有必要对数组和记录这类复合数据使用动态分配。堆仅用于由程序显式执行的动态分配。因此,如果在主程序启动后没有动态分配,堆管理和存储回收不成问题。
Ada避免基于C语言语法的编程语言中的典型的陷阱。例如,一个八进制字面量,如177被写为8#177#,而不是0177。另一个例子是,能够在数值字面量中使用下划线使数值对于人类读者显而易见。Ada的复合语句的语法避开“悬挂else”的陷阱和C的switch语句的各种问题。
Ada的最有用功能之一是程序员能够指定一个标量变量的值的范围, Ada语义可确保检测到超出范围的赋值。指定标量范围对于向人类读者转达程序的意图是一种宝贵的援助,该信息还可以被编译器用于优化,被静态分析工具用于错误分析。Ada语义确保在运行时检测到臭名昭著的“缓冲区溢出”漏洞,例如赋值超出数组的末尾。
并发管理
典型的实时程序涉及并发性,因为它很自然地为监测或控制各种外部设备或过程的软件组件的控制定义独立的线程。这就提出了如何用编程语言对并发进行建模的直接问题。一些语言,如C和C+ +,忽视这个问题,认为并发是一个可以由一个外部库提供的服务。这样语言标准是简单了,但是程序员需要认识到,在引入并发后,顺序应用程序中所使用的语义可能会发生变化。例如,一个非重入库,对于顺序应用程序可能是安全的,但被并发线程调用时会导致数据结构的损坏。
相比之下,若干种语言(包括Ada,Java和C#)提供并发的特别功能。Ada的并发模型有独到之处,它的基础是可靠和有效的。Ada并发的单元是任务,任务之间一般通过封装的数据(受保护对象)或直接的沟通(会合)相互作用。受保护对象执行封装的以状态为基础的互斥,但避免象Java和其它语言所引起的竞争条件。图2是使用受保护对象的Ada任务例子。请注意,接口(包Point_Pkg的规范)与图1相同,但这里用于任务程序的实现是安全的。,当AdaCore在一个多核系统中实现GNAT Pro Ada环境时,Ada任务模式扩展到多核架构,但不需要改变运行库。



图2 Ada并发程序结构示例

除了提供一般的并发模型,实时系统的语言需要处理时间、截止时间、调度等功能,以及低层处理(中断处理,访问“原始数据存储”等)。Ada直接满足所有这些要求。例如,在调度方面Ada定义了任务优先级的语义,在优先级封顶协议的基础上规定了优先级继承和对象锁定机制,并提供了多种任务指派策略,其中包括“运行,直到被阻塞或抢占”和“最早的截止时间优先”。由于对象锁定受优先级封顶协议的管辖,可以在单处理器中优化保护对象,以避免互斥和排队开销。
Ada让事情安全
安全关键软件投入运行提高了质量保证的标杆,其中的一个关键要求是可分析性。为了确保象数据存储这样的制约得到满足,开发人员需要保证有足够的栈空间。这意味着要么没有递归或表明递归是有界的。需要淘汰或小心管理动态分配(安全关键中的自动垃圾回收仍然是一个研究课题)。根据采用的分析技术,其他类似功能也必须取消或限制其使用。不存在“一刀切”的一个子集,限制的种类取决于安全水平和所使用的具体的分析技术。
Ada有一种独特的方法解决这个问题:通过一个称为编注(pragma)限制的机制,一个程序可以指定哪些功能被禁止。试图使用任何这些被禁止功能会导致编译失败。程序实现可以省略支持该功能的运行库,这样开发者不需要提供这些库的认证材料。这种点菜方式提供了最大的灵活性。可以取消或限制的功能包括任务、异常处理、动态分配和面向对象编程。 AdaCore的GNAT Pro是执行这种优化技术的一个例子。洛克希德马丁航空将使用AdaCore的GNAT Pro 为C - 130J超大力士飞机开发飞行管理系统接口管理器和无线电控制的软件。
雷文斯卡文件
一组相关的限制规定可以捆绑成一个文件(profile)。Ada 2005标准包括所谓的雷文斯卡文件(Ravenscar profile)它包括一个简单的任务功能集的定义,其使用和运行库都可以进行安全认证。一个使用雷文斯卡文件的程序包含一组任务,每个任务依据一个简单事件或一个定时永久循环。尽管简单,但雷文斯卡文件足以表达实际的各种并发程序。
有各种语言可用于实时和安全关键系统的,但Ada引人注目,因为它是专门为此设计的。它的基础是可靠性和早期的错误检测,,它通过提供一个灵活的机制,使开发人员可以定制自己的语言子集,从而引导表达性和分析性之间的平衡。通过传统的基于栈的运行时模型,Ada避免象Java语言严重依赖动态分配会出现的问题。Ada也是SPARK语言及其工具的基础,SPARK程序是合法的Ada程序,可用任何标准的Ada编译器编译,它在安全关键和高保密性应用方面有成功的经验。更多细节请参阅侧栏“SPARK:一个增强的用于高完整性系统的Ada子集。”Ada多年来增加了对高完整性方面的支持,它仍然是适合这个领域的苛刻要求的最贴切的技术。
内容来自用户分享和网络整理,不保证内容的准确性,如有侵权内容,可联系管理员处理 点击这里给我发消息
标签: 
相关文章推荐