Jan, 2023

基于组件的建模与仿真检验框架：集成各组件

PDF
TL;DR本文提出了一个综合的验证框架来应对组合性验证中的一些重要问题，并提出了一个验证过程来验证不同类型的系统模型，如反应式、实时和概率系统的组合性。该框架提供了验证组合性所需的方法、技术和工具支持。为了验证动态 - 语义组合性，我们探讨了三种不同的方法，即基于 Petri 网的代数分析、基于有色 Petri 网的状态空间分析和基于通信顺序处理的模型检查。
发现论文，激发创造
  • 验证学习为基础的安全关键航空系统的认证框架

    本文提出了一种针对航空系统中基于学习的组件进行设计时间和运行时保证的安全验证框架，该框架整合了两种新方法：同时考虑了离线和在线验证机制，并且允许各个模块使用独立的方法和技术进行开发，以满足系统不同阶段的安全性要求，从而实现系统产品的持续学习和评估。

    May, 2022

  • DSL 组合的形式代数框架

    本研究讨论了一种使用代数结构来建模元语言的正式框架，以编写、组合和提供 DSL 抽象之间的互操作性，目的是为了验证元语言的组成性质。通过构建这个正式框架，并通过我们针对 DARPA V-SPELLS 计划所开发的管道，我们的论文全面讨论了此验证流程的概览。验证流程拆分为四个主要组件：第一是在 Coq 中提供元语言的正式模型；第二是在 Coq 中给出我们选择的代数结构的说明；第三，我们需要在 Coq 中实现我们的代数结构的具体实例，并给出 Coq 的证明，证明这个实现符合第二步的规范；最后，在 Coq 中给出元语言的正式模型是第三步实现的一个实例的证明。

    Feb, 2023

  • 可验证的组合性强化学习系统

    我们提出了一个可验证和组合的强化学习框架，其中一组强化学习子系统被组合起来以实现整体任务，子系统之间通过定义接口和部分可观察性相互交互。实验结果展示了该框架在各种环境中的新颖功能。

    Sep, 2023

  • 动态和控制模型的通用验证框架与证书合成

    我们提供了一个对系统规范进行编码和定义相关证明的通用框架，并提出了一种自动化的方法来形式合成控制器和证明，通过利用神经网络的灵活性提供候选控制和证明函数，同时使用 SMT 求解器提供正确性的正式保证，我们通过开发一个原型软件工具对我们的框架进行测试，并评估其在通过对广泛的基准测试进行控制和证明合成时的有效性。

    Sep, 2023

  • 可验证和组合的强化学习系统

    提出了一种可验证和组合强化学习的框架，其中包含一组学习单独子任务的子系统，并填充入标准任务的高层模型，将各个子任务组合成全部任务，成功证明了该框架的实用性和有效性。

    Jun, 2021

  • 模型的组合性是由什么决定的？一个理论视角：附加材料

    本文旨在理解语言中组成性结构在模型失败中的作用以及与其表达能力和样本复杂度的关系，并提出了一种神经符号化的组成性函数及其复杂性的定义，并分析了各种现有的通用和特殊目的序列处理模型在该定义下的组成性复杂性，最后基于提出的定义给出了显式地依赖于它的组成性模型的表达能力和系统化泛化的理论保证，并突出了影响实验性能的因素。

    May, 2024

  • 基于 Agent 的自主系统决策实际验证

    本文介绍了一种验证方法，用于分析基于代理的混合系统中的决策制定组件，该方法包括适用于基于代理的逻辑组件的模型检查技术，并且该技术与连续部分的混合系统的单独分析相结合，从而允许使用程序模型检查器来验证混合自主系统中决策制定的实际实现。

    Oct, 2013

  • 基于组合归纳不变式的神经网络控制系统验证

    本文介绍了一种针对神经网络控制系统（NNCS）安全验证的新方法，利用归纳不动点方法，并配合自动推断必要的分解谓词的算法，将验证过程从数小时（甚至超时）缩短至几秒钟，在案例研究中显著提高了验证性能。

    Dec, 2023

  • 概率模型检查和自主性

    本文综述了概率模型检测在 PRISM 和 PRISM-games 模型检查器支持下的可观测和不可观测马尔可夫决策过程、顺序和并发随机博弈以及相关概率时态逻辑，以及其在自主系统中的应用，并探讨了未来研究方向和挑战。

    Nov, 2021

  • 高度可配置数字设计的高效配置覆盖的半正式验证方法

    使用半形式验证方法对高度可配置的数字设计进行高覆盖率配置覆盖的研究

    Apr, 2024