首页> 外文期刊>Science of Computer Programming >A model-extraction approach to verifying concurrent C programs with CADP
【24h】

A model-extraction approach to verifying concurrent C programs with CADP

机译:一种使用CADP验证并发C程序的模型提取方法

获取原文
获取原文并翻译 | 示例

摘要

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs.
机译:用于工业关键系统的可靠软件的开发得益于使用形式模型和验证工具来尽早检测和纠正错误。理想情况下,使用基于模型的完整方法,形式模型应该是获取最终可靠代码的起点,并且验证步骤应该在高级模型上进行。但是,对于许多项目而言并非如此,尤其是在集成现有代码时。在本文中,我们描述了一种通过自动提取适用于现有工具进行分析的高级形式化模型来验证并发C代码的方法。我们的方法的基本组成部分是:(1)一种从源代码构建带标签的过渡系统的方法,该方法将流程控制和流程之间的交互考虑在内; (2)程序外部行为的建模方案,即操作系统提供的功能; (3)使用需求驱动的静态分析对程序进行进一步的抽象,从而在验证过程中节省时间和内存。整个提案已实现为CADP工具箱的扩展,该工具箱已经使用标记的过渡系统作为核心模型为多种输入语言提供了多种分析模块。所采用的方法非常适合现有的CADP体系结构,无需进行更改即可启用C程序验证。我们通过考虑VLTS基准套件和各种并发程序的C实现的示例来说明扩展的CADP工具箱的使用。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号