安全关键嵌入式系统中的Ada例外 [英] Ada Exceptions in Safety Critical Embedded Systems

问题描述

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

• 根据其实现，它可能会导致运行时开销或更大的代码大小(此处提到的在实施"下)
• 执行异常所花费的时间可能是不确定的(我看到的几种来源之一)

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

尽职调查:我很难确切地确定确定性Ada异常的程度，但是我的理解是它们的原始实现要求更多的运行时开销，以换取减小的代码大小影响(上面的第一个链接提到了Ada明确地).除了上述第一个链接之外，我还研究了提及代码确定性的配置文件，例如Ravenscar配置文件和本文，但是似乎没有提及异常处理确定性.公平地说，由于这个话题看起来很深，所以我可能在错误的地方找东西.

解决方案

异常在Ada中是确定性的. (但是某些可能引发异常的检查具有一定的自由度.如果编译器可以提供正确的答案，则如果中间结果超出了所讨论的类型的范围，则不一定总是引发异常.)

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

我自己还没有从事安全关键系统的工作，但是我可以肯定地知道Ariane 4惯性导航系统中用于软件的运行时包含异常.

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

I started learning Ada for its potential use in an embedded device which is safety critical. So far, I'm really liking it. However, in my research on embedded programming, I came across the hot topic of whether to use exception handling in embedded systems. I think I understand why some people seem to avoid it:

• depending on its implementation it can introduce either run-time overhead or larger code size (mentioned here under "Implementation")
• the time it takes to execute exceptions can be non-deterministic (one of several sources I saw)

Now my question is, Does the Ada language or the GNAT compiler address these concerns? My understanding of safety critical code is that non-deterministic code size and execution time is often not acceptable.

Due Diligence: I am having a bit of trouble finding out exactly how deterministic Ada exceptions can be, but my understanding is their original implementation called for more run-time overhead in exchange for reduced code size impact (above first link mentions Ada explicitly). Beyond the above first link, I have looked into profiles mentioning determinism of code, like the Ravenscar profile and this paper, but nothing seems to mention exception handling determinism. To be fair, I may be looking in the wrong places, as this topic seems quite deep.

解决方案

Exceptions are deterministic in Ada. (But some checks which can raise an exception have some freedom. If the compiler can provide a correct answer, it doesn't always have to raise an exception, if an intermediate result is out of bounds for the type in question.)

At least one Ada compiler (GNAT) has a "zero cost" exception implementation. This doesn't make exceptions completely free, but you don't pay a run-time cost until you actually raise an exception. You still pay a cost in terms of code space. How large that cost is depends on the architecture.

I haven't worked on safety critical systems myself, but I know for sure that the run-time used for the software in the Ariane 4 inertial navigation system included exceptions.

If you don't want exceptions, one option is to use SPARK (a language derived from Ada). You can still use any Ada compiler you like, but you use the SPARK tools to prove that the program can't raise any exceptions. You should note that SPARK isn't magic. You have to help the tools, by inserting assertions, which the tools can use as intermediate steps for the proofs.

这篇关于安全关键嵌入式系统中的Ada例外的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！