利用多空间工具的语义分析来自动证明MISRA违规

MISRA标准是跨行业广泛采用的编码标准。在嵌入式软件开发和质量保证团队中，它已经成为一种常见的最佳实践。这些组织中有很多都严格遵守至少一部分适用规则(如果不是全部的话)的规则。这样的遵从性策略将需要一个审查过程来处理对编码规则的违反，而这个过程通常是资源密集型的。

一个系统的MISRA合规过程将包括静态分析工具可以检测编码规则违反情况。这可以是为了遵守编码规则而对代码进行更改，或者检查违反规则的地方以适当地证明它们是正确的。然后会有一个处理偏差的过程(MISRA标准需要一个过程来证明偏差)。这可以是修改代码以符合编码规则或证明偏差的形式。

一旦您确定了编码规则的违规，您就可以手动分析违规，并选择修复问题或提供理由。其理由基本上是为了证明违反编码规则不会有任何副作用。因此，它可能是相当资源密集型，取决于以下几个因素:

• 您是在开发新代码还是在调整遗留代码?后者可能是一场噩梦。
• 您在开发过程的哪个阶段检查遵从性?开发过程越晚，成本就越高。
• 谁在进行分析，谁在审查结果?这与上面的合规问题有关。如果开发人员运行分析并解决问题，而不是QA组在最后运行分析并向开发人员发送报告以解决问题，那么这种方法是有效的。在我们与客户的讨论中，我们发现QA团队很难验证开发人员提供的违反MISRA的理由。

但是，如果您能够减少这些挑战——解决这些违规行为所需的时间和精力，又会怎样呢?你会问，怎么做到的?如果您能够访问有关违反某些MISRA规则的操作的详细信息，并证明这些特定操作对于所有可能的运行时场景是安全的，因此没有副作用(MISRA规则的精髓)，那么该怎么办呢?

这在多元空间静态分析解决方案中是可能的，这是可能的，因为Polyspace代码验证正式证明。如果能够证明特定的操作对于每一个可能的执行路径(对于程序中的每一个可能的控制和数据流)都是安全可靠的，那么即使某个操作违反了特定的编码规则，不需要对代码进行任何更改，也不需要在团队之间来回讨论如何进行验证。您只需指出来自Code验证器验证的证明作为您的理由。

让我们看看这里的一些示例代码，其中我们添加了两个底层大小不同的整数类型(int 32和unsigned int 16)，这将导致隐式转换，因此将违反MISRA规则10.1。但是，正如您在下面的图片中看到的，加法操作不会导致溢出(副作用)。因此，除了在您的报告中捕获理由之外，不需要做任何工作。

这仅对映射到由Polyspace Code验证的底层运行时检查的MISRA规则的子集是可能的。这个过程使我们的一些客户节省了20%的工作量。如果您有兴趣了解关于这个主题的更多信息，或者查找映射到各种检查的MISRA规则列表，那么您可以联系作者．