利用Polyspace工具的语义分析来自动证明MISRA违反
MISRA标准是一个广泛采用的行业编码标准。在嵌入式软件开发和质量保证小组中，它已经成为一种常见的最佳实践。许多这样的小组都严格遵守至少一部分适用规则的策略——如果不是所有的编码规则的话。这样的遵从性策略将需要一个审查过程来处理对编码规则的违反，并且这个过程通常是资源密集型的。
系统的MISRA合规流程将包括静态分析工具可以检测编码规则的违反。这可以是对代码进行更改以遵守编码规则，或者审查违规行为以适当地证明其合理性。然后会有一个过程来处理偏差(MISRA标准要求一个过程来证明偏差)。这可以是修改代码以符合编码规则或证明偏差的形式。
一旦确定了违反编码规则的情况，就可以手动分析违反情况，并选择修复问题或提供理由。其理由本质上是为了证明违反编码规则不会产生任何副作用。因此，它可能是相当资源密集型的，这取决于以下几个因素:
- 您是在开发新代码还是在调整遗留代码?后者可能是一场噩梦。
- 您在开发过程的哪个阶段检查遵从性?开发过程越晚，成本就越高。
- 谁在运行分析，谁在审查结果?这与上面的合规性问题有关。如果开发人员运行分析并解决问题，而不是QA组在最后运行分析并向开发人员发送报告以解决问题，那么这是有效的。在我们与客户的讨论中，我们发现QA团队很难验证开发人员提供的违反MISRA的理由。
但是，如果可以减少这些挑战——减少处理此类违规行为所需的时间和精力，会怎样呢?你会问是怎么做到的吗?如果您可以访问有关违反某些MISRA规则的操作的详细信息，并证明这些特定操作对于所有可能的运行时场景都是安全的，因此没有副作用(底层MISRA规则的精神)，那该怎么办?
这在Polyspace静态分析解决方案中是可能的，这只是因为它的能力多空间代码证明正式证明证明特定操作对于每一种可能的执行路径(对于程序中可能的每一种控制和数据流)都是安全可靠的能力意味着，即使某个操作违反了某种编码规则，也不需要对代码进行任何更改，也不需要在团队之间来回讨论如何进行验证。您只需指出来自代码验证器验证的证明作为您的理由。
让我们看看这里的一些示例代码，其中我们添加了两种不同底层大小的整数类型(int 32和unsigned int 16)，这将导致隐式转换，因此将违反MISRA规则10.1。但是，正如您在下面的图像中看到的，加法操作不会导致溢出(副作用)。因此，除了在报告中捕获理由之外，没有其他工作要做。
这仅适用于映射到由Polyspace Code provver验证的底层运行时检查的MISRA规则子集。这个过程已经使我们的一些客户减少了多达20%的工作量。
