安全关键嵌入式系统中的Ada异常

Question

我开始学习Ada在嵌入式设备中的潜在用途,这对于安全至关重要.到目前为止,我真的很喜欢它.但是,在我对嵌入式编程的研究中,我遇到了在嵌入式系统中是否使用异常处理的热门话题.我想我理解为什么有些人似乎避免它:

• 根据其实现,它可以引入运行时开销或更大的代码大小(在"实现"中提到)
• 执行异常所花费的时间可能是非确定性的(我看到的几个来源之一)

现在我的问题是,Ada语言或GNAT编译器是否解决了这些问题？我对安全关键代码的理解是,非确定性代码大小和执行时间通常是不可接受的.

尽职调查:我很难找到确切的Ada例外情况,但我的理解是他们的原始实现要求更多的运行时开销以换取减少代码大小的影响(上面的第一个链接明确提到了Ada).除了上面的第一个链接,我已经查看了提到代码确定性的配置文件,比如Ravenscar配置文件和本文,但似乎没有提到异常处理确定性.公平地说,我可能正在寻找错误的地方,因为这个话题似乎很深.

Answer 1

有嵌入式系统是安全或关键任务的,嵌入式系统是硬实时的,嵌入式系统是两者兼而有之.

实时硬实时的嵌入式系统可能受到限制.70年代,同事们在导弹制导系统上工作,在主回路中有大约4个指令值!(你可以想象,它是用汇编语言编写的,并使用了一个调优的执行程序,而不是RTOS.不支持异常).另一方面,我工作的最后一个,在1 GHz PowerPC板上,对特定中断的响应有2毫秒的最后期限,我们测得的最坏情况是1.3毫秒(无论如何这是一个软实时要求,你不必连续错过太多).

该系统也有安全要求(我知道,我知道,安全的导弹系统,呵呵)虽然我们被允许使用例外,但未处理的例外意味着系统必须关闭,导弹在飞行中或没有,导致损失导弹 并且我们严格禁止说when others => null;要吞下一个例外,所以我们没有处理的任何例外都会被"未处理"并且会反弹到最高级别.

参数是,如果发生未处理的异常,您将无法再知道系统的状态,因此您无法证明继续存在.当然,更广泛的安全工程必须考虑整个系统应该采取什么行动(例如,这个处理器可能应该以恢复模式重新启动).

有时人们将异常作为其控制流程的一部分; 事实上,对于处理随机文本输入,一个常用的方法是,而不是检查文件的结尾,只需继续,直到你得到End_Error;

loop
   begin
      --  read input
      --  process input
   exception
      when End_Error => exit;
   end;
end loop;

Jacob的回答讨论了使用SPARK.您不必使用SPARK来处理异常,但当然能够向您自己(以及您的安全审核员证明!)证明不会有任何异常.处理异常非常棘手,有些RTS(例如Cortex GNAT RTS)没有; 配置编译指示

pragma Restrictions (No_Exception_Propagation);

意味着异常不能传播到它们被引发的范围之外(程序将通过调用a来崩溃Last_Chance_Handler).

仅仅在它们被引发的范围内传播异常不是,IMO,这是有用的:

begin
   --  do something
   if some error condition then
      raise Err;
   end if;
   --  do more
exception
   when Err =>
      null;
end;

避免"多做"代码会是一种相当混乱的方式.最好使用标签!

Answer 2

Ada中的例外是确定性的.(但是一些可以引发异常的检查有一些自由.如果编译器可以提供正确的答案,那么如果中间结果超出了相关类型的范围,则不一定要引发异常.)

至少一个Ada编译器(GNAT)具有"零成本"异常实现.这不会使异常完全免费,但在实际引发异常之前,您不需要支付运行时成本.您仍然需要在代码空间方面支付费用.这个成本有多大取决于架构.

我自己没有研究安全关键系统,但我确信Ariane 4惯性导航系统中用于软件的运行时间包括异常.

如果您不想要例外,一种选择是使用SPARK(一种源自Ada的语言).您仍然可以使用任何您喜欢的Ada编译器,但是您使用SPARK工具来证明程序不会引发任何异常.你应该注意到SPARK并不神奇.您必须通过插入断言来帮助这些工具,这些工具可以用作证明的中间步骤.