A Review of Validation and Verification of Neural Network-based Policies for Sequential Decision Making
该综述针对序列决策中神经网络策略的验证确认难题，通过文献调研与滚雪球检索筛选18篇2018-2023年相关论文，总结现有方法并指出该领域受关注度提升、问题与技术多样的特点及未来研究方向。
2023-12-15 cs.SE
Using Assurance Cases to Guide Verification and Validation of Research Software
本文通过主动脉分割软件案例，展示保证案例如何指导研究软件的验证与确认，强调证据收集及软件与用户责任区分的重要性。
2024-11-05 cs.SE
Revolutionizing Validation and Verification: Explainable Testing Methodologies for Intelligent Automotive Decision-Making Systems
Technical University of Munich（慕尼黑工业大学）
针对自动驾驶系统决策模型验证确认效率低、难溯源的问题，提出融合可解释性的测试方法学，含LLM生成测试场景等模块，旨在提升效率与透明度、降低成本并增强用户信任。
2025-06-20 cs.SE
Local and Global Analysis: Complementary Activities for Increasing the Effectiveness of Requirements Verification and Validation
本文提出了一种独特的方法来连接需求工程（RE）活动到一个过程框架，可以用来获得质量要求，减少支出的努力和成本。我们提出了一个两阶段模型，这是新颖的，因为它引入了概念的验证和确认（V&V）的早期需求生存周期。在第一阶段，我们在为每个单独不同的系统功能引出需求之后立即执行V&V。因为第一阶段的重点是迭代地捕获较小的相关需求集，所以每个相应的V&V活动更好地集中于检测和纠正每个需求集中的错误。在第二阶段，启动补充验证活动;相应的重点是要求集之间的联系质量，而不是要求集内的要求。因此，这种方法减少了核查工作，并加强了对核查任务的关注。与其他模型不同，我们的方法在需求的引出和V&V活动的执行之间具有最小的时间延迟。由于时间间隔很短，涉众对需求、其背景和理由有了更清楚的回忆;这增强了涉众的反馈。此外，我们的模型包括与软件行业中采用的有效RE过程密切相关的活动。因此，我们的方法有助于更好地理解需求流，并为可再生能源过程的实施提供指导。
2005-03-02 cs.SE
umd-verification: Automation of Software Validation for the EGI federated e-Infrastructure
在EGI e-Infrastructure中支持e-Science需要广泛而可靠的软件，用于高级计算用途，部署在大约300个欧洲和全球数据中心。统一中间件分发（UMD）和云中间件分发（CMD）是为EGI电子基础设施消费提供软件的渠道。软件按照软件供应过程（SWPP）进行编译、确认和分发，其中质量标准（QC）定义设定了EGI验收的最低质量要求。目前UMD和CMD发行版中存在的软件组件越来越多，阻碍了传统的基于手动的验证机制的应用，从而推动了自动化解决方案的采用。本文介绍了umd验证，一个开源的工具，强制执行的QC要求，在一个自动化的方式为科学处置的软件产品的持续验证的履行。UMD验证工具已成功集成到SWPP管道中，并逐步支持UMD和CMD存储库中产品的全面验证。虽然支持新产品的成本取决于基础设施即代码解决方案的可用性，以接管部署和高测试覆盖率，但已经集成的产品所获得的结果是有希望的，因为产品验证所投入的时间已经大大减少。此外，自动化的采用为流程的可靠性带来了好处，例如消除了与人为相关的错误或先前测试功能的回归风险。
2018-07-30 cs.SE
Verification and Validation of Autonomous Systems
Mercedes-Benz（梅赛德斯-奔驰）；Oakland University（奥克兰大学）
本文研究自主系统中软件缺陷的预防、发现与纠正方法，并提出在开发阶段提升软件可靠性保障水平的途径。
2024-11-20 cs.AI cs.SE
LLM4VV: Exploring LLM-as-a-Judge for Validation and Verification Testsuites
本文提出LLM4VV，通过基于智能体的提示方法和验证流水线结构，利用DeepSeek Coder评判基于指令的编程模型编译器测试套件，显著提升了LLM评判质量。
2024-08-22 cs.SE
Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents
本文提出一个针对自主智能体SLEEC规则的形式化规范、验证与核验框架，包括规则语言、tock-CSP形式语义以及冲突冗余检测和合规核验方法，并在消防无人机和辅助穿衣机器人上验证其适用性。
2023-07-07 cs.SE
Challenges of Virtual Validation and Verification for Automotive Functions
本文针对汽车功能虚拟验证与确认的挑战，通过专家研讨会和调查问卷，识别出17个关键挑战及解决方案，发现资源利用是关键需求，为领域后续研究提供方向。
2025-08-20 cs.SE
Model-based Verification and Validation of an Autonomous Vehicle System
网络物理系统（CPS）的软件开发，例如，自动驾驶汽车需要功能性和非功能性的质量保证，以保证CPS安全有效地运行。EAST-ADL是一种专用于安全关键型汽车嵌入式系统设计的领域特定架构语言。我们之前已经修改了EAST-ADL，以包含能量约束，并将EAST-ADL/STATEFLOW中建模的能量感知实时（ERT）行为转换为适合形式化验证的UPPAAL模型。本文通过对SIMULINK的支持和在同一工具链中集成Simulink/Stateflow来扩展以前的工作。基于EAST-ADL中扩展的ERT约束，将Simulink/Stateflow模型转换为具有随机语义的可验证UPPAAL模型，并将转换与形式化统计分析技术相结合：EAST-ADL约束的概率扩展定义为一种语义表示。提出了一组映射规则，以方便保证翻译。使用SIMULINK DESIGN VERIFIER/UPPAAL-SMC对功能和非功能特性进行了形式化分析。在自主交通标志识别车辆的案例研究中验证和演示了分析技术。
2018-03-19 cs.SE
Effective Requirements Generation: Synchronizing Early Verification & Validation, Methods and Method Selection Criteria
本文提出了一种有效的需求生成过程的实施和执行的方法。我们通过提供一个定义良好的需求工程模型来实现这一目标，该模型包括验证和确认（V&V）以及分析。此外，我们确定了重点活动目标和映射流行的方法，以较低级别的活动，并定义了一个标准为基础的过程，以优化方法的选择伴随活动。与其他模型不同，我们的模型解决了完整的需求生成过程，并由定义在更充分的抽象层次上的活动组成。此外，我们的模型还采用了一种独特的V&V方法，可提高质量并降低生成需求的成本。此外，活动目标被确定并明确说明-而不是像当前模型中那样隐含。为了帮助选择一组合适的方法，我们已经将常用的方法映射到基于其目标的活动。最后，我们已经确定了方法选择标准，并规定了一组简化的方法，这些方法可以优化模型中每个活动的标准。因此，我们的方法有助于选择方法的任务，通过使用选择标准，以减少一个更小的，可管理的一组潜在的方法的大集合。该模型、方法到活动目标的清晰映射以及基于标准的过程，共同为需求生成过程的有效实施和执行提供了急需的指导。
2005-03-02 cs.SE
Enhancing Translation Validation of Compiler Transformations with Large Language Models
本研究提出融合大语言模型的编译器转换翻译验证框架，以Alive2为基础工具，借助微调LLM预判转换可靠性并结合模糊测试找反例，解决传统形式化工具在LLVM转换等复杂场景的验证局限。
2024-02-01 cs.PL cs.SE
A Theory-driven Interpretation and Elaboration of Verification and Validation
本研究以V&V是知识构建活动为公理，用动态认知模态逻辑构建系统工程中验证与确认的形式化理论，厘清其概念基础，解决传统实践模糊性，提升工程方法论的精确性与一致性。
2025-04-11 cs.SE cs.SY eess.SY
Towards Improving Validation, Verification, Crash Investigations, and Event Reconstruction of Flight-Critical Systems with Self-Forensics
Concordia University（康考迪亚大学）
本文介绍了一种新的自我取证的概念，以补充标准的自主自我CHOP属性的自我管理系统，在Forensic Lucid语言中指定。我们认为，自我取证，与取证采取的网络犯罪域，是适用于“自我解剖”的目的验证的自主软件和硬件系统的飞行关键系统的自动化事件和异常分析和事件重建的工程团队在各种事件的情况下，在设计和测试以及实际的飞行数据。
2009-06-10 cs.AI cs.SE
End to End Verification and Validation with SPIN
在过去的几年中，用于模型检验的工具变得更加有效和可用。这使得用户能够将模型检验应用于工业规模的问题，但是验证模型实现的任务通常要困难得多。在本文中，我们提出了一种方法来做端到端的验证和确认的实时的系统使用SPIN模型检查。以SQRL起搏器正式方法挑战赛中提出的心脏起搏器系统为例，我们通过在SPIN中构建心脏起搏器的正式模型来展示我们的框架，检查模型的理想时间属性（表示为LTL公式），从模型生成C代码（通过PROMELA的改进）并验证生成的实现（使用SPIN）。我们认为，一个国家的艺术模型检验工具，如SPIN可以用来做正式规范以及验证的实现。为了评估我们的方法，我们表明，我们的起搏器模型是足够的表达，以获得一致的操作模式和细化规则保持LTL属性。
2013-02-20 cs.PL cs.SE
Probabilistic Failure Analysis in Model Validation & Verification
University of Toulouse（图卢兹大学）；IRIT（法国图卢兹计算机科学研究所）；INPT（国立图卢兹综合理工学院）
自动故障定位是模型确认和验证中的一个重要问题。它帮助最终用户分析故障的根源。在这项工作中，我们展示了故障定位的概率分析方法的早期实验。受贝叶斯概率论中Kullback-Leibler分歧的启发，提出了一种可疑因子来计算模型检验可达图中变迁的故障贡献，并利用该因子对潜在故障变迁进行排序.为了在详细设计的仿真模型中自动定位设计故障，我们提出使用统计模型隐马尔可夫模型（HMM），它提供了统计上相同的信息，以组件的真实行为。该方法的核心是故障定位算法和后向算法，前者给出了一组经过排序的可疑故障元件，后者计算HMM与仿真模型的匹配度来评估定位结论的置信度。
2016-11-18 cs.LG cs.SE
Challenges and Practices in Aligning Requirements with Verification and Validation: A Case Study of Six Companies
本文通过访谈6家公司的30名从业者，识别需求工程与验证确认协调中的沟通、追踪、变更控制等挑战，并提出实践路线图。
2023-07-24 cs.SE
Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification
传统上，从业者主要将形式化方法用于质量保证过程的一半：验证（我们构建的软件正确吗？）。另一半--验证（我们是否构建了正确的软件？）--相对来说，很少受到关注。虽然验证是基于精化的形式化方法的核心，其中每个新的精化步骤必须保留其抽象模型的所有属性，但验证通常被推迟到开发的最新阶段，此时模型可以自动执行。因此，在需求或其解释中的错误被发现得太晚了：通常在开发过程的最后。在本文中，我们提出了一种新的方法来检查符合性的需求和他们的正式细化为基础的规范在早期阶段的发展。我们提出的方法--“验证义务”--基于一个简单的想法，即验证和验证都是系统所有细化步骤的组成部分。
2021-02-11 cs.FL cs.SE
Verification, Validation and Integrity of Distributed and Interchanged Rule Based Policies and Contracts in the Semantic Web
基于规则的策略和契约系统在软件工程中的特性很少被研究。这是一个严重的遗漏，因为在基于规则的策略或契约表示语言中，规则被用作声明性程序设计语言来形式化真实世界的决策逻辑并在其上创建IS生产系统。本文采用了一种来自极限编程的SE方法，即测试驱动开发，并讨论了它如何适用于策略和合同规范的验证、确认和完整性测试（V&V&I）。由于测试驱动的方法集中在行为方面和得出的结论，而不是规则库的结构和故障的原因，它是独立的规则语言和测试系统的复杂性，因此更容易使用和理解的规则工程师和用户。
2006-09-29 cs.AI cs.SE
Developing a Unified Verification and Validation Activity Standard at JPL
Jet Propulsion Laboratory, California Institute of Technology（加州理工学院）
针对JPL验证与确认实践碎片化问题，提出基于关系型架构和SysML模型的统一V&V活动模式，并通过Jama平台实现受控定制，以平衡严谨性与敏捷性。
2026-09-25 cs.SE cs.SY eess.SY
Agentic Porting, Construction and Initial Verification and Validation of Libraries within the Open Source Unified TRAnsient Multi-Phase Advanced Reactor simulation Kit (Outram Park) Part I: A Software Engineering Log for Thermal Hydraulics
本研究将OpenFOAM库智能体迁移至Rust语言的Outram-Foam库，开发了两相HEM壅塞流求解器，验证显示其吻合度良好，智能体编码可提升开源库开发效率，人类专业知识仍为关键。
2026-09-18 cs.SE physics.comp-ph
Formal Data Validation with Event-B
本文介绍了在工业环境中执行的验证和确认活动，通过创建这些配置数据及其属性的正式B模型来验证地铁CBTC系统的配置数据。双工具链用于安全地检查某个给定的配置数据输入是否满足其属性。一个工具基于一些Rodin和开源插件，另一个工具基于ProB。
2012-10-26 cs.SE
A Survey of Verification, Validation and Testing Solutions for Smart Contracts
智能合约是存储在区块链上的程序，在满足预定条件时运行。然而，设计和实现智能合约并不简单，因为在区块链上部署时，不再可能修改它（无论是为了改进还是修复错误）。只有通过部署一个新版本的智能合约才有可能，这是昂贵的（新合约的部署成本和旧合约的销毁成本）。为此，有许多解决方案可以在部署之前测试智能合约。由于实现无错误的智能合约可以提高可靠性并降低成本，因此测试是一项必不可少的活动。在本文中，我们将试图解决智能合约测试的现有解决方案分为以下几类：公共测试网络，安全分析工具，区块链模拟器和区块链模拟器。然后，我们分析这些解决方案，对它们进行分类，并展示它们的优点和缺点。
2021-12-07 cs.DC cs.MA cs.SE
Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques
PrePost（部署前和部署后验证技术）研讨会旨在汇集计算机辅助验证和验证领域的研究人员，讨论部署前和部署后验证技术之间的联系和相互作用。研讨会涵盖的主题的例子是经典的模型检验和测试之间的关系，一方面和运行时验证和统计模型检验另一方面，类型系统之间的关系，可以通过静态或动态检查技术，如运行时监控。
2016-05-25 cs.LO cs.SE
Update on the Verification and Validation Efforts for the Stakeholder Tool for Assessing Radioactive Transportation
本研究针对美国能源部的放射性运输决策支持工具START开展验证与确认工作，通过大地测量法核查关键输出、开发可复现的验证方法，测试超150组路线并比对新旧版本的路线长度结果，以提升工具输出的可信度。
2023-06-15 cs.SE nlin.AO
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
School of Computer Science, Shanghai Jiao Tong University（上海交通大学计算机科学学院）；School of Artificial Intelligence, Shanghai Jiao Tong University（上海交通大学人工智能学院）；Shanghai Innovation Institute（上海创新研究院）；School of Computer Science and Engineering, University of Washington（华盛顿大学计算机科学与工程学院）
本文提出神经符号框架，通过自然语言描述和函数签名生成内存感知的形式函数规范，结合符号证明器和验证工具链迭代优化，提升形式规范的正确性与语法有效性。
2026-03-12 cs.AI cs.SE
Reconciling interoperability with efficient Verification and Validation within open source simulation environments
信息物理系统（CPS）包括物理子系统和软件子系统。基于仿真的方法通常用于支持多个领域的CPS的设计和验证与确认（V&V），例如：航空航天，国防，汽车，智能电网和医疗保健。因此，许多基于模拟的工具可用，这带来了巨大的互操作性挑战。为了克服这些问题，2010年提出了功能模型接口（FMI）作为支持模型交换（ME）和协同仿真（CS）的开放标准。符合这一标准的模型被称为功能模型单元（FMU）。FMU在定义复杂的CPS方面发挥着重要作用，例如，SSP标准。CPS的基于模拟的V&V通常需要探索不同的场景（即，外源CPS输入序列），其中许多显示共享前缀。因此，在共享前缀的结尾处的模拟器状态被保存，然后被恢复并用作下一场景的模拟的开始状态。在这种情况下，FMI的一个重要功能是能够按需保存和恢复内部FMU状态。不幸的是，此功能的实现不是强制性的，它只在某些商业软件中可用。这促使我们为开源CPS模拟环境开发这样的功能。在本文中，我们专注于JModelica，一个开源的建模和仿真环境中定义的Modelica语言的CPS。我们描述了我们如何赋予JModelica与我们的FMI 2.0功能的开源实现，以保存和恢复内部状态的FMU ME。此外，我们提出的结果评估，通过934基准模型，我们扩展的JModelica的正确性和效率。我们的结果表明，基于模拟的V&V平均比没有它的情况下快22倍。
2021-06-01 cs.SE cs.SY eess.SY
Intersection focused Situation Coverage-based Verification and Validation Framework for Autonomous Vehicles Implemented in CARLA
University of York（约克大学）；Boston University（波士顿大学）
自动驾驶汽车（AV），即自动驾驶汽车在安全关键领域运行，因为自动驾驶软件中的错误可能导致巨大的损失。从统计数据来看，道路交叉口是自动驾驶汽车运营设计领域（ODD）的一部分，具有最高的事故率。因此，测试自动驾驶汽车在道路交叉口的限制，并确保其在道路交叉口的安全性是相关的，因此，本文的重点。我们提出了一个基于情况覆盖率（SitCov）的AV测试框架，用于AV的验证与确认（V&V）和安全保证，该框架是在一个名为CARLA的开源AV模拟器中开发的。SitCov的自动驾驶测试框架的重点是在不同的环境和交叉口配置情况下的道路交叉口上的车辆与车辆的交互，使用情况覆盖标准的自动测试套件生成的自动驾驶汽车的安全保证。我们已经开发了一个本体的交叉情况，并使用它来生成一个情况超空间，即，从本体论中产生的所有可能情况的空间。为了评估我们的SitCov AV测试框架，我们在自我AV中植入了多个故障，并比较了基于情况覆盖和随机情况生成。我们发现，这两种生成方法触发的种子故障数量大致相同，但基于情况覆盖的生成告诉我们更多关于我们的自我AV的自动驾驶算法的弱点，特别是在边缘情况下。我们的代码是公开的在线，任何人都可以使用我们的SitCov AV测试框架，并使用它或进一步建立在它之上。本文的目的是有助于V&V和AV的开发领域，不仅从理论的角度来看，而且从开源软件贡献的角度来看，并发布一个灵活/有效的工具V&V和AV…
2022-01-25 cs.AI cs.MA cs.RO
Airavat: An Agentic Framework for Internet Measurement
University of California, Irvine（加州大学尔湾分校）
Airavat通过代理框架实现互联网测量工作流的自动化生成与验证，解决了复杂分析中工具协调和方法学验证的难题。
2026-02-24 cs.AI cs.NI cs.SE
Verification & Validation of Agent Based Simulations using the VOMAS (Virtual Overlay Multi-agent System) approach
基于Agent的模型在许多不同的领域都非常流行。例如，它们已被用于一系列领域，从肿瘤生长、免疫系统、分子到社交网络、人群以及计算机和移动自组织网络的模型。他们成功的原因之一是他们的直觉和人类认知的相似性。然而，由于这种抽象能力，尽管很容易适用于如此广泛的领域，但很难验证基于代理的模型。此外，构建有效和可信的模拟不仅是一项具有挑战性的任务，而且是一项重要的工作，以确保我们所建模的东西在某种抽象层次上是我们概念系统的模型;我们心目中的系统。在本文中，我们提出了一种新的技术，它具有广泛的适用性，可以应用到各种基于代理的模型验证基于代理的模型，解决了这一重要领域。我们提出了一个框架，其中一个虚拟的覆盖多智能体系统可以用来验证仿真模型。此外，由于基于代理的模型已经典型地增长，并行，在多个领域，以满足所有这些，我们提出了一个新的单一的验证技术适用于所有基于代理的模型。我们的技术，它允许基于代理的模拟验证使用VOMAS：一个虚拟的覆盖多代理系统。该覆盖多代理系统可以包括各种类型的代理，其在需要验证的基于代理的仿真模型之上形成覆盖。除了能够监视和记录之外，这些代理中的每一个都包含明确定义的约束，如果违反这些约束，则可以实时的记录。为了证明其有效性，我们展示了其广泛的适用性，在各种各样的仿真模型，从社会科学到计算机网络的空间和非空间概念模型。
2017-08-08 cs.AI cs.MA cs.SE
Early Validation of High-level Requirements on Cyber-Physical Systems
针对安全关键型网络物理系统（CPS）高层需求早期验证问题，提出将需求转换为事件演算并利用无接地s(CASP)等ASP求解器推理的方法，相关初步成果已被ICLP'24接收。
2025-02-13 cs.LO cs.SE
