HAL多学科开放获取存档：抽象解释数值属性的模块化分析

0HAL编号：tel-025541250https://theses.hal.science/tel-02554125v20提交日期：2020年8月27日0HAL是一个多学科开放获取存档，用于存储和传播科学研究文档，无论它们是否发表。这些文档可以来自法国或国外的教育和研究机构，或者来自公共或私人研究中心。0HAL多学科开放获取存档，旨在存储和传播法国或国外的教育和研究机构、公共或私人实验室发表或未发表的研究级科学文献。0通过抽象解释进行数值属性的模块化分析0Remy Boutonnet0引用此版本：0Remy Boutonnet. 通过抽象解释进行数值属性的模块化分析. 数据结构与算法[cs.DS].阿尔卑斯大学[2020-..]，2020年。英文。�NNT：2020GRALM004�。�tel-02554125v2�0博士论文0为了获得学位0格勒诺布尔阿尔卑斯大学博士0专业：计算机科学0部长令：2016年5月25日0由RémyBOUTONNET展示0由尼古拉斯∙哈尔布瓦克斯指导，阿尔卑斯大学研究主任，阿尔卑斯大学0在VERIMAG实验室的数学、科学和信息技术博士学院内准备0通过抽象解释进行数值属性的模块化分析0通过抽象解释进行数值属性的模块化分析02020年3月9日公开支持的论文，评审委员会成员包括：0尼古拉斯∙哈尔布瓦克斯先生，法国国家科学研究中心代表团阿尔卑斯分部主任，导师安德烈亚斯∙波德尔斯基教授，德国弗莱堡大学，评审员安托万∙米涅教授，巴黎索邦大学，评审员塞萨尔∙蒂内利教授，爱荷华大学，美国，考官科琳娜∙安库尔特研究员，巴黎高科矿业学院，考官奥利维尔∙布伊索博士工程师，美国梅松公司，考官苏珊娜∙格拉夫研究主任，法国国家科学研究中心代表团阿尔卑斯分部，主席0如何检查一个程序以确保它是正确的？0ALAN M. TURING 检查一个大型程序报告会议，高速自动计算机，剑桥，1949年6月24日。0摘要0安全关键系统中的任何软件错误或设备故障都可能造成灾难性后果。对关键系统中的程序进行验证和分析对于确保软件满足其规范并且没有运行时错误至关重要。通过抽象解释的静态程序分析计算程序可达状态的一个准确近似。它发现程序的不变性属性，这些属性由抽象域的元素表示。由于计算成本高昂，大多数工业静态分析工具不使用表达能力丰富的关系数值抽象域，如凸多面体。我们提出了一种基于计算程序的不相交关系摘要的模块化分析方法，用于自动发现数值属性。过程摘要只需计算一次，并用于以自底向上的方式计算过程调用的效果。我们的方法特别适用于提高线性关系分析的可扩展性，或者使用凸多面体的抽象解释，尽管它基于一个更通用的框架，可用于任何关系抽象域。不相交关系摘要是由关系抽象域的元素表示的有限集合，表示抽象输入输出关系。它们是基于过程前置条件的分区计算的。我们提供了一些启发式方法来计算过程前置条件的抽象分区。我们还提供了改进摘要计算精度的方法，特别是通过对分析过程中的前置条件进行仔细处理。我们的方法也适用于递归过程，其中摘要以递归方式计算为自身。我们在名为mars的C程序新静态分析平台中实现了我们的方法。我们对M¨alardalen基准程序进行了实验，结果显示我们的方法可以显著减少线性关系分析的分析时间，相比于在每个调用上下文中完全分析过程的完全上下文敏感分析。分析精度没有受到显著损害，甚至可以通过使用分离来改善。在第二部分中，我们提出了一种用于数值属性的反应系统的模块化分析方法。我们提出了一种灵活的反应组件行为表示方法，称为关系模式自动机(RMA)，它允许在不同抽象级别上分析反应系统的行为。RMA可以根据实现组件反应的过程的不相交摘要自动构建。使用RMA对单个组件的分析结果可以被重用以模块化地分析具有多个组件实例化的较大的反应系统。我们将此方法应用于简化的自动地铁控制系统的分析。0关键词：静态分析，抽象解释，过程间分析，过程摘要，凸多面体，反应式系统，同步编程。0摘要0在关键系统中存在错误或故障可能会产生可怕的后果。验证和分析嵌入在关键系统中的程序对于确保所提供的软件符合其规范并且在执行时没有错误至关重要。通过抽象解释进行静态分析可以计算程序可达状态的安全近似。它通过用抽象域的元素表示程序的不变性属性来发现程序的不变性属性。数值抽象域，如八边形或凸多面体域，具有不同的精度级别。工业静态分析工具通常不使用最具表达能力的数值抽象域，如凸多面体域，因为其操作复杂性。在本论文中，我们提出了一种用于发现数值属性的程序的模块化分析方法，该方法基于过程的不交和关系摘要的计算。每个过程的摘要是通过自下而上的方式计算的，并在过程调用的效果分析中使用。尽管我们的方法应用于线性关系分析或多面体抽象解释，以提高其可扩展性，但它在更广泛的适用于任何关系抽象域的框架中定义。过程的不交摘要是由抽象关系域的元素表示的有限的输入-输出关系集合。它们是通过使用过程的前置条件的分区计算得到的。我们提出了计算前置条件分区的启发式方法。我们还提出了改进摘要计算精度的方法，特别是通过特殊处理前置条件。我们的方法也适用于递归过程，其中摘要是根据它们自身计算的。我们的模块化分析已经在一种名为mars的新的C程序静态分析工具中实现。我们的实验表明，与在每个调用上下文中分析过程的传统分析相比，我们的方法可以显著减少线性关系分析的分析时间。结果的准确性没有显著降低，并且通过在摘要中使用不交可以进一步提高准确性。在第二部分中，我们提出了一种用于分析反应式系统的模块化方法。我们提出了一种灵活的反应式组件表示方法，称为关系模式自动机（RMA），可以在不同的抽象级别上分析反应式系统。关系模式自动机可以根据实现每个组件的过程的不交摘要自动构建。每个组件的分析结果可以在更大规模的反应式系统的分析中重复使用，其中每个组件可以实例化多次。该方法应用于简化的地铁网络控制系统的分析。0关键词：静态分析，抽象解释，过程间分析，过程摘要，凸多面体，反应式系统，同步编程。0致谢0我感谢Antoine Min´e和Andreas Podelski对本文稿的审查和评论。我感谢CesareTinelli，Corinne Ancourt，Olivier Bouissou和SusanneGraf参加了我的论文答辩委员会。我感谢我的导师NicolasHalbwachs给了我与他一起工作的绝佳机会，自从我五年前的TER研究实习以来。没有他，这项工作是不可能的。我感激并感谢他的深思熟虑，广博的科学知识，他的不断支持和巨大的可用性。我感谢Claire Maiza和Fabienne Carrier的支持，并给我机会在我的L3magist`ere实习期间发现计算机科学研究。我感谢来自Verimag和IMAG大楼的同事和学生，尤其是Valentin，Yanis，Cl´ement，Cyril，Vincent，Matheus，Bai和Ma¨eva，感谢他们的友谊以及我们在这三年中分享的所有餐食和讨论。我感谢Valentin对抽象解释，计算机科学中最深奥的领域以及其他各种主题的所有有趣和充满激情的讨论，我们在 la pause期间进行了许多讨论。我感谢我的大学朋友Rapha¨el和Timoth´ee的陪伴。我感谢Adam，Damien，Romain和Th´eotime成为我最棒的朋友。我感谢J´er´emy成为我的朋友，并且自从我们在大学的第一天起就在我的生活中，也是我认识的最有才华的人之一。我要感谢我的祖父，他从小就让我对科学产生了兴趣。他传授给我他对微妙的艺术和精确的科学的热爱，他鼓励我倾听那些古老的书籍和物品等待着讲述的惊人故事。我要感谢我的祖母Jeanne，感谢她的智慧，教会我努力工作和各种稀有技能的好处。我感谢我的父母和兄弟姐妹对我的持续和坚定的支持，尤其是在怀疑和逆境时。我的父母传授给我温和、开放和追求正义的价值观。他们教会我如何对周围的世界保持好奇心。我特别感谢星期天的家庭传统——森林散步和探索各种古老、神秘或只是被遗忘已久的建筑和地方。110目录01 引言 1501.1 背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1501.2 贡献 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1601.3 大纲  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170I 现状 1902 通过抽象解释进行程序分析 2102.1 程序和语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2102.1.1 过渡系统  . . . . . . . . . . . . . . . . . . . . . . . . . . . 2102.1.2 程序作为控制流图 . . . . . . . . . . . . . . . . . . . . . . . . . . 2202.1.3 收集语义  . . . . . . . . . . . . . . . . . . . . . . . . . . . 2302.2 不动点定理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2402.2.1 完备格  . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2402.2.2 单调函数和塔斯基的不动点定理 . . . . . . . . 2502.2.3 连续函数和Kleene定理  . . . . . . . . . . . . . . . . . . . . 2502.3 具体和抽象域 . . . . . . . . . . . . . . . . . . . . . . . . . 2602.3.1 抽象域  . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2602.3.2 修正点计算 . . . . . . . . . . . . . . . . . . . . . . . . . 2702.3.3 收敛  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2802.4 数值抽象域 . . . . . . . . . . . . . . . . . . . . . . . . . . 3102.4.1 仿射等式 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3102.4.2 区域 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3102.4.3 八边形 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3202.4.4 凸多面体  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3302.5 高级技术  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3602.5.1 引导静态分析  . . . . . . . . . . . . . . . . . . . . . . . . . 3602.5.2 跟踪分区 . . . . . . . . . . . . . . . . . . . . . . . . . . . 3703 过程间分析：现状 3903.1 过程间分析的起源  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3903.1.1 函数式方法 . . . . . . . . . . . . . . . . . . . . . . . 4003.1.2 调用字符串方法  . . . . . . . . . . . . . . . . . . . . . . . 4203.2 通过图可达性的过程间数据流分析 . . . . . . . . . . . . . . . . . . . . . . . . 4403.3 过程间分析的堆栈抽象  . . . . . . . . . . . . . . . . . . . . . . . . 4603.4 语句级摘要  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471203.5 使用通用断言的过程摘要 . . . . . . . . . . . . . . . . . . . . . . . 4803.6 过程间关系分析  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4803.6.1 模块化静态分析  . . . . . . . . . . . . . . . . . . . . . . . . 4803.6.2 函数的关系抽象 . . . . . . . . . . . . . . . . . . . . . . . . 4903.6.3 基于线性代数的过程间分析  . . . . . . . . . . . . . . . . . . 4903.6.4 使用线性算术的双重过程间分析  . . . . . . . 500II 过程间分析的关系摘要 5104 关系抽象解释 5304.1 状态和传递闭包上的关系  . . . . . . . . . . . . . . . . . . . . . . . . . 5304.2 具体关系语义  . . . . . . . . . . . . . . . . . . . . . . . . . . 5604.2.1 具体关系摘要  . . . . . . . . . . . . . . . . . . . . . . . . . . . 5604.2.2 过程调用的具体语义  . . . . . . . . . . . . . . . . . . . . . . . . 5604.2.3 从状态到关系收集语义  . . . . . . . . . . . . . . . . . . . . 5704.2.4 一个非常简单的例子 . . . . . . . . . . . . . . . . . . . . . . . . . 5804.3 关系抽象解释  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5904.3.1 通用框架 . . . . . . . . . . . . . . . . . . . . . . . . . . . 5904.3.2 使用LRA构建摘要  . . . . . . . . . . . . . . . . . . . . . 6104.3.3 示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6204.4 前提条件  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6304.4.1 在前提条件下的扩展 . . . . . . . . . . . . . . . . . . . . 6404.5 结论  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6505 析取关系过程摘要 6705.1 激励示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6805.2 抽象关系的析取细化 . . . . . . . . . . . . . . . . . 6905.2.1 通用框架  . . . . . . . . . . . . . . . . . . . . . . . . . . . 6905.2.2 前置条件分区的细化05.2.3 调用的抽象效果05.2.4 应用于线性关系分析05.3 分区细化05.3.1 细化启发式05.3.2 根据局部可达性进行细化05.3.3 根据被调用过程的摘要进行细化05.3.4 迭代细化05.4 最后的改进：推迟循环反馈05.5 递归过程的摘要05.6 结论06 实现与实验06.1 mars静态分析器06.1.1 基本用法06.2 设计与实现06.2.1 抽象域1306.2.2 调度器06.2.3 传递函数模块06.3 mars中间表示06.3.1 抽象语法06.3.2 测试的转换06.4 过程参数的非重复06.4.1 布尔属性06.4.2 语义方程06.5 实验06.6 结论0III 反应式系统的模块化分析07 反应式系统的分析与验证07.1 反应式系统简介07.2 同步语言07.3 Lustre编程语言07.4 同步语言的编译07.5 结构化反应式程序07.6 分析与验证07.6.2 同步程序的分析07.7 结论08 关于使用关系模式自动机对反应式系统进行模块化分析08.1 有界事件计数器08.2 步骤过程的分离总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 8.2.1 一般原则 . .. . . . . . . . . . . . . . . . . . . . . . . . . . 12308.2.2 示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12508.2.3 从分离总结到模式 . . . . . . . . . . . . . . . . . . . . . . . . . 12808.3 关系模式自动机 . . . . . . . . . . . . . . . . . . . . . . . . . . . 12908.3.1 定义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12908.3.2 语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13108.3.3 并行组合 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13208.4 关系模式自动机的可达性分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 8.4.1计算策略 . . . . . . . . . . . . . . . . . . . . . . . . . . 13608.4.2 有界事件计数器的可达性分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13808.4.3 控制转移关系的迭代构建 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13908.5 关系模式自动机的并行组合分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14008.5.1 计算策略 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14108.5.2 构建简化产品自动机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14208.5.3 示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14308.6 关系模式自动机的简化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 8.6.1合并模式的简化 . . . . . . . . . . . . . . . . . . . . . 1451408.6.2 内部简化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14608.7 不变量 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 8.7.1关系模式自动机的不变量 . . . . . . . . . . . . . . 14608.7.2 弱不变量 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14708.7.3 分离不变量 . . . . . . . . . . . . . . . . . . . . . . . . . . 14708.7.4 关系增强 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14808.8 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14809 示例：地铁控制系统 14909.1 详细列车步骤过程总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 9.1.1内存变量的细化 . . . . . . . . . . . . . . . . . . . . . 15209.1.2 输入变量的细化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15409.1.3 总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15709.2 列车的关系模式自动机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15909.3 单列车分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . 16009.4 一对列车的模块化分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16309.5 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165010 结论 1670参考文献171150第1章0引言0自从1949年AlanTuring发表了关于程序验证的第一篇论文以来，许多事情发生了变化。抽象解释和过程间分析诞生于四十多年前。这篇论文是站在巨人的肩膀上的。01.1 上下文0如今，嵌入式系统无处不在。它们是大型设备的一部分的计算机系统。例子很多，从智能手机或数字手表的消费电子产品，到航空航天、交通或核电站中的非常大型和复杂的系统。它们中的许多是大规模生产的，大多数都很难更新，比如深度嵌入在智能手机通信子系统中的固件或核反应堆控制软件。许多嵌入式系统具有实时约束，其中一些被认为是安全关键的，控制软件的任何错误或设备的故障都可能产生灾难性后果，对环境产生重大影响，可能造成大量伤亡。关于软件错误的事故示例众所周知。1996年的阿丽亚娜5号坠毁事件[85]是由于整数溢出引起的。Therac-25放射治疗机[84]在1985年至1987年之间的至少六起事故中给患者造成了大量过量辐射，原因是各种软件缺陷和更广泛的软件工程问题。最近，波音梦想客787[2]由于交流电源管理系统固件中的计数器溢出问题，每248天就必须重新启动一次。这促使我们需要一个可靠而系统的验证过程来验证安全关键系统，提供可信的保证，即软件满足其规范，并且没有运行时错误。有几个方法家族：0•测试或动态分析是通过观察软件在某些精心选择的输入上的行为来进行的。尽管这种方法可以检测到错误，但它并不是穷尽的，因为一般情况下无法测试所有的输入和场景。测试0•静态分析是一类在程序的静态表示上执行的技术，而不是执行它。其中一些技术在数学上证明了程序没有错误，而其他技术则能够发现错误。通过抽象解释进行的程序分析计算了程序可达状态的一个精确近似。它发现了程序的不变性属性，这些属性由抽象域的元素表示。这些不变性可以用于证明运行时的错误的不存在，例如算术溢出，或者证明给定的断言。工业工具如Polyspace [ 94 ]或Astr´ee [ 19]可以证明用C语言编写的大型嵌入式软件中不存在运行时错误。一些工具如PIPS [ 69 ] Clousot [ 46 ]或Infer [ 29 ]适用于更广泛的软件种类。In this thesis, we are interested in improving the scalability of Linear Relation Analysis,or abstract interpretation based on convex polyhedra, by computing precise relationalsummaries of procedures. We make use of the procedural structure of programs to proposea new modular analysis for the automatic discovery of numerical properties. Althoughspecifically applied to convex polyhedra, it is based on a more general framework usablewith any relational abstract domain.Our analysis framework comes with a formalization of relational abstract interpreta-tion that we did not find elsewhere. Based on relational collecting semantics, we presentthe construction of relational procedure summaries as abstract input-relations betweenthe initial values of procedure parameters and their final value at the exit of a procedure.Procedures can exhibit very different behaviors which can not be expressed preciselyby a single element of a classical abstract domain such as convex polyhedra. In order tohave precise procedure summaries, we compute disjunctive relational summaries, whereeach disjunct is an abstract input-output relation represented by a separate element of arelational abstract domain.Taken together, the sources of each individual relation in a disjunctive summary forman abstract partition of the procedure precondition to account for all the possible valuesof parameters.The precision of a disjunctive summary is determined by the qualityof the precondition partitioning. We give heuristics to compute an abstract partitionof a procedure precondition. We also give ways to improve the precision of summarycomputation. As we show that preconditions are at the heart of precise summaries, theyare entitled to a specific and careful treatment during summary computation. Summariesare computed once and for all in a bottom-up fashion and used to analyze the effect ofprocedure calls.We also show that our approach applies to recursive procedures. In some way, thesummary of a recursive procedure must be computed in terms of itself.160第1章 引言0Astr´ee成功地扩展到了用C语言编写的大型嵌入式程序，但避免了更精确的抽象域，如凸多面体，因为它们的计算复杂度较高。而是使用了不太表达的抽象域，如整数区间或八边形。尽管大型程序被组织为函数或过程的集合，Astr´ee对程序进行自上而下的分析，而不真正考虑它们的过程间结构。过程要么被内联，要么在每次调用时重新分析。01.2 贡献0在本论文中，我们致力于通过计算精确的过程关系摘要来提高线性关系分析的可扩展性，或者基于凸多面体的抽象解释。我们利用程序的过程结构，提出了一种新的模块化分析方法，用于自动发现数值属性。尽管专门应用于凸多面体，但它基于一个更通用的框架，可与任何关系抽象域一起使用。我们的分析框架提供了一个关系抽象解释的形式化，我们在其他地方没有找到。基于关系收集语义，我们介绍了关系过程摘要的构建，作为过程参数初始值与过程退出时的最终值之间的抽象输入关系。过程可能表现出非常不同的行为，这些行为不能通过经典抽象域（如凸多面体）的单个元素来精确表示。为了获得精确的过程摘要，我们计算了不交的关系摘要，其中每个不交由关系抽象域的单独元素表示，代表一个抽象输入输出关系。在一个不交摘要中，每个单独关系的源构成了过程前置条件的抽象划分，以考虑参数的所有可能值。不交摘要的精确性取决于前置条件划分的质量。我们提供了启发式方法来计算过程前置条件的抽象划分。我们还提供了改进摘要计算精度的方法。正如我们所展示的，前置条件是精确摘要的核心，它们在摘要计算过程中应受到特殊和谨慎的处理。摘要是一次性地以自下而上的方式计算出来，并用于分析过程调用的效果。我们还展示了我们的方法适用于递归过程。在某种程度上，递归过程的摘要必须以自身为基础进行计算。0使用关系过程摘要进行模块化分析1701.3 概述0我们在一个名为mars（Mars抽象解释研究系统）的新静态分析器中实现了这种方法，该分析器基于Clang，由20000行C++代码和4000行OCaml代码组成。它从头开始设计用于实验新的静态分析。mars中间表示专门设计用于通过抽象解释来简化静态分析的开发，并提供高质量的源代码可追溯性信息。这项工作已发表在[27]中。0反应式程序的模块化分析0许多嵌入式程序必须根据其环境连续地对输入作出反应。它们被称为反应式程序。反应式程序可以用C语言编写，也可以用专用语言编写，如同步语言Lustre、Esterel或Signal。空中客车A380的飞行控制软件是用Lustre为基础的工业数据流同步语言SCADE编写的。反应式程序通常被组织为计算系统对输入的反应并产生输出的组件集合。反应式组件也可以具有在每个反应步骤中更新的内存。它们由称为步骤过程的步骤过程实现，这些步骤过程在全局无限循环中被重复调用。虽然Astrée可以扩展到从SCADE生成的大型C程序，但它并没有利用反应式程序的特性，并且在分析过程中完全丢失了组件的结构。在第二部分中，我们为反应式系统的新模块化分析铺平了道路，该分析基于步骤过程的不相交关系摘要的计算。我们提出了一种专门用于分析的反应式程序抽象称为关系模态自动机（RMA）。它提供了一种灵活的表示，允许以不同的详细程度表达反应式系统的行为。RMA是根据步骤过程的不相交关系摘要自动构建的。我们提出了RMA的可达性分析及其并行组合，该分析不需要在分析之前昂贵的显式构建并行产品。我们提供了各种启发式方法来减少给定关系模态自动机的精度水平，以实现在精度和分析性能方面的不同权衡。组件的分析结果可以用于包含它的较大系统的模块化分析，通过计算其在其他步骤过程中的抽象效果。这种方法目前在使用Python库PyApron上的小例子上实现，该库提供了对Apron抽象域库的高级绑定。0其他作品0在本论文期间，已发表了早期工作的延续，涉及抽象解释在经典递增和递减序列之外的一些改进[26]，以及线性关系分析在程序最坏情况执行时间估计中的应用[115]。01.3 概述0本论文分为三个部分：180第1章 引言0第一部分介绍了抽象解释的静态分析，并概述了关于程序的过程间分析的现状。首先介绍了本论文中使用的程序表示，并回顾了一些语义的基本概念，以及抽象解释的标准框架。它还提到了一些提高经典抽象解释精度的改进。然后，概述了过程间分析及其主要方法，从基础工作到现状，对其超过四十年的丰富文献进行了简要介绍。第二部分介绍了我们基于计算不相交关系过程摘要的模块化分析。首先描述了我们的通用框架，并对关系抽象解释进行了形式化。我们给出了这个框架在凸多面体抽象域上的一个特殊应用。我们特别关注了前置条件的处理及其在摘要计算中的作用。然后，我们展示了如何基于前置条件分区获得不相交的过程摘要。我们提供了几种分区启发式方法和改进的摘要计算方法。最后，我们介绍了mars静态分析器的实现，以及