MSVL驱动的C程序模型检查方法

"本文介绍了一种使用MSVL（建模、仿真和验证语言）对C程序进行模型检查的方法。通过将C程序转换为MSVL程序，并用命题投影时态逻辑（PPTL）公式指定所需属性，然后使用统一的模型检查方法来检查MSVL程序是否满足该公式。如果满足，则C程序正确；如果不满足，则能找到反例。文章详细介绍了从C到MSVL的翻译算法，并给出了一个示例来说明该方法的工作原理。关键词包括：时态逻辑、MSVL、模型检查、验证、翻译。" 在计算机科学和软件工程领域，C语言是开发软件系统最常用的语言之一。然而，确保C程序的正确性和可靠性是一个重大的挑战。模型检查是一种自动验证技术，它能够系统地探索程序的所有可能执行路径，从而找出潜在的错误或不满足的性质。 MSVL是一种强大的工具，它结合了建模、仿真和验证的功能，使得对C程序的模型检查成为可能。在本研究论文中，作者提出了一种方法，首先将C源代码转化为MSVL语言的形式，这一步骤的关键在于如何精确地保持C代码的语义同时将其转换为MSVL的结构。转化过程可能涉及对C语言的控制流和数据流的深入理解和抽象。 接下来，使用命题投影时态逻辑（PPTL）来表述我们希望程序满足的属性。PPTL是一种扩展的时态逻辑，允许对程序的行为进行复杂的表述，包括对时间序列和状态变迁的约束。这使得我们可以定义如“在某个时刻之后，某个条件始终为真”这样的高级属性。 在转换和指定属性后，通过统一的模型检查算法来检验MSVL程序是否符合PPTL公式。若符合，说明C程序满足所设定的正确性条件；若不符合，模型检查器会返回一个反例，即一种导致不满足条件的执行路径，帮助开发者定位问题。 论文详细介绍了这个转换算法，这对于理解如何从C到MSVL的翻译过程至关重要。此外，作者还提供了一个实例，通过实际的代码和步骤演示了这种方法如何应用于具体的C程序验证，使得读者能更好地理解和应用这一技术。 这篇研究论文贡献了一种使用MSVL进行C程序模型检查的有效方法，为提高C程序的正确性和可靠性提供了一条新的途径。这种方法的实用性和效率对于软件验证领域具有重要意义，特别是在需要严格保证的系统，如航空航天或嵌入式系统等中。