A survey on formal specification and verification of separation kernels
分离内核是安全和安全关键系统的基础软件，它为托管应用程序提供空间和时间分离以及分区之间的受控信息流。分离核在关键领域的应用要求通过形式化验证来验证分离核的正确性。据我们所知，没有关于这一主题的调查文件。本文综述了分离核的形式化描述和验证。本文首先介绍了分离核的概念和背景，并对不同分离核进行了比较。然后，我们调查了自2000年以来关于这个主题的最新技术。最后，通过详细的比较和讨论，对研究工作进行了总结.
2016-07-10 cs.SE
Generating Logical Specifications from Requirements Models for Deduction-based Formal Verification
工作涉及自动生成的逻辑规格的需求模型。以这种方式获得的逻辑规范可以使用演绎推理进行形式化验证。形式化验证关注模型行为的正确性。需求工程的可靠性对于软件开发过程的所有阶段都是必不可少的。演绎推理是一种重要的形式化方法。然而，逻辑规范，被认为是一组时序逻辑公式，很难指定手动经验不足的用户，这一事实可以被视为一个重大障碍，实际使用的演绎为基础的验证工具。提出了一种利用UML图建立需求模型的方法，包括逻辑规格说明。将活动图组织到预定义的工作流模式中可以自动提取逻辑规范。所提出的方法的关键方面是集成的需求工程阶段和逻辑规格的自动生成。提出了一种基于演绎的验证系统。推理过程可以基于语义表方法。提供了一个简单的需求获取和验证的示例。
2014-02-09 cs.SE
A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements
验证复杂的安全关键系统是一项重大挑战。手动测试和模拟经常使用，但只能探索系统可达状态的子集。形式化方法是一种基于知识的软件规格说明和开发技术，它可以提供系统状态空间上的属性证明和穷举检查。在本文中，我们提出了一个正式的需求驱动的方法，适用于我们的工业合作伙伴提供的飞机发动机控制器的模型。我们的方法开始正式化的控制器的自然语言的要求，使用（预先存在的）正式的需求获取工具（FRET），迭代，与我们的行业合作伙伴协商。一旦形式化，FRET可以自动转换的要求，使他们的验证旁边的Simulink模型的飞机发动机控制器;的要求也可以指导形式化验证使用其他方法。在我们的方法中，这两个并行流寻求结合正式的需求引出，经典的验证方法和运行时验证的结果，以支持在Simulink中建模的航空航天系统的验证，从需求阶段到执行。我们的方法利用正式方法的力量，补充现有的验证技术，并支持整个验证过程中的需求的可追溯性。这种方法通过确保预先正式化要求并在开发过程中可用，简化了开发可验证飞机发动机控制器的过程。在本文中，我们给出了一个概述（FRET），描述我们的方法和工作的形式化和验证的要求，并概述了未来的工作，使用我们的方法。
2021-10-18 cs.SE
Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
本文提出通过将 Stipula 法律合同翻译为带 JML 规范的 Java 代码，并利用 KeY 工具自动验证其部分和完全正确性，证明了通用演绎验证工具在翻译方法中的有效性。
2025-09-26 cs.SE
Towards A Broader Acceptance Of Formal Verification Tools: The Role Of Education
形式化方法虽然具有优势，但在软件开发实践中面临着广泛接受和采用的挑战。主要原因是假设的复杂性。学术界可以通过一个深思熟虑的教学和实践计划来解决这个问题。本文中详细介绍的用户研究正在检查AutoProof工具，其动机是识别形式化方法的复杂性。参与者（计算机科学硕士课程的学生）的表现和反馈的经验与正式的方法帮助我们提取特定的问题领域，影响工具的可用性。研究结果推断，随着验证工具功能的改进，教学计划必须修改，以包括先决条件的课程，使形式化方法易于学生适应，并促进其在软件开发过程中的使用。
2019-06-04 cs.SE
Towards Formal Verification of a TPM Software Stack
本文基于Frama-C对开源TPM软件栈tpm2-tss开展形式化验证案例研究，针对链表和复杂数据结构带来的挑战提出解决方案，验证了代表性函数的功能性质与无运行时错误，并指出实现完整验证所需的工具改进。
2023-10-27 cs.SE
Bus Protocols: MSC-Based Specifications and Translation into Program of Verification Tool for Formal Verification
消息序列图（MSC）是一种吸引人的可视化形式主义，主要用于系统设计的早期阶段，以捕获系统的需求。然而，如果我们走向一个实现，一个可执行的规范，以某种方式相关的MSC为基础的要求，必须获得。MSC可以有效地用于指定总线协议的方式，其中高级转换系统用于捕获协议的系统组件的控制流，MSC用于描述非原子组件的交互。该规范系统可进行形式化验证。在本文中，我们提出的方式，我们可以指定的总线协议，使用MSC和这些规格说明如何可以转换成程序的验证工具（我们已经使用的符号模型验证器（SMV））使用的形式化验证。在这方面，我们为以下任务作出了贡献。首先，介绍了利用MSC来指定协议的方法。其次，一个翻译器，翻译的规范（描述在文本输入文件）到SMV程序已经建成。最后，我们给出了使用SMV程序对AMBA总线协议进行验证的结果。通过转换过程找到的SMV程序可以用于自动验证任何指定的总线协议的各种属性。
2010-09-26 cs.SE
Formal Verification, Engineering and Business Value
如何将模型检验和静态程序分析等自动化验证技术应用于数百万行嵌入式C/C++代码？如何将这种技术包装成软件开发人员和工程师可以使用的方式，他们可能没有形式化验证的背景？以及如何说服企业经理实际支付这样的软件？这项工作解决了其中一些问题。基于我们自己开发和发布Goanna源代码分析器的经验，我们解释了模型检验，静态分析和SMT解决的底层技术，涉及创建工业证明工具的步骤。
2013-01-01 cs.SE
A User Study for Evaluation of Formal Verification Results and their Explanation at Bosch
该研究针对博世汽车工程师开展调研与实验，发现形式化方法应用存在理解难点，验证了反例解释方法可降低验证结果理解难度，为工业界形式化方法落地提供参考。
2023-04-18 cs.SE
An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization
本文介绍去中心化重配置语言Concerto-D，它扩展自Concerto，具备去中心化协调避免单点故障、Maude机械化形式语义保障可执行性两大优势，适配边缘计算、CPS等场景，用真实CPS案例做了示例验证。
2024-12-11 cs.PL cs.SE
Specification and Verification of Context-dependent Services
当前用于服务的发现、规范和提供的方法忽略了服务契约与服务可以保证其契约的条件之间的关系。此外，它们没有使用正式的方法来指定服务、契约和组合。没有正式的基础，就不可能通过形式化验证来证明服务组合的正确性条件和服务条款中合同义务的履行。我们在本文中纠正这种情况。我们提出了一个正式的定义与上下文相关的合同服务。我们定义了一个组合理论的服务与上下文相关的合同考虑到功能，非功能，法律和上下文信息。最后，我们提出了一个形式化验证方法，将服务组合的形式化规范转换为扩展的时间自动机，可以使用模型检验工具UPPAAL进行验证。
2011-08-11 cs.SE
Requirement analysis, Architectural design and Formal verification of a multi-agent based University Information Management System
提出了一种基于多Agent的高校信息管理系统的分析、设计和形式化验证方法。大学IMS访问信息，创建报告，方便教师和学生。协调器代理管理所有代理之间的协调。它还管理整个系统的数据库连接。建议的IMS是基于BDI代理体系结构，该模型的基础上的信念，愿望和意图的系统。安全性和活性的正确性性质由一阶谓词逻辑指定。
2015-01-06 cs.SE
A Survey of Smart Contract Formal Specification and Verification
智能合约是一种计算机程序，允许用户在区块链平台上自动执行操作。鉴于智能合约在支持包括供应链、金融、法律和医疗服务在内的各行业重要活动方面的重要性，对验证和确认技术的需求非常强烈。然而，绝大多数智能合约缺乏任何形式的规范，这对于确定其正确性至关重要。在本次调查中，我们调查了文献中提出的智能合约的正式模型和规范，并提出了一个系统的概述，以了解共同的趋势。我们还讨论了目前使用的方法，在验证这些属性的规格，并确定差距，希望认识到有前途的方向，为未来的工作。
2021-04-19 cs.SE
A User-Study Protocol for Evaluation of Formal Verification Results and their Explanation
背景：由于特征和功能的数量不断增加，工业中现代安全关键系统的复杂性不断增加。这就需要正式的方法，以信任这样的系统。然而，由于可用性问题，在工业中使用正式方法是有要求的，例如，理解模型检验结果的困难。因此，假设是，以用户友好的方式呈现模型检查器的结果可以促进正式方法在行业中的使用。目的：我们的目标是评估工程师接受的形式化方法，如果理解验证结果的复杂性变得容易。方法：我们进行了两项不同的探索性研究。首先，我们进行了一项在线调查，以探讨在识别不一致的规范和使用正式的方法，从工程师的挑战。其次，我们进行了一组前测和后测实验，以收集工程师使用正式的方法，如果理解验证结果是容易的印象。局限性：本研究的主要局限性是概括性，因为调查集中在一个特定的目标群体，它使用了前实验设计。
2021-08-13 cs.SE
Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas
在通信协议的设计过程中，许多设计决策会影响协议的行为及其正确性。协议的形式化规范和验证可以证明其正确性。本文给出了一个利用CSM自动机的形式规格说明和时序逻辑验证设计决策的实例。
2017-10-25 cs.SE
Formal Verification of Dynamic and Stochastic Behaviors for Automotive Systems
功能和非功能需求的形式化分析在汽车系统中至关重要。这些系统的行为往往依赖于复杂的动力学以及随机行为。我们提出了一个概率扩展的时钟约束规约语言，称为PrCCSL，规范（非）功能性需求，并证明了需求的正确性，通过映射到UPPAAL模型的语义规范。以前的工作扩展在本文中，包括一个扩展的PrCCSL，称为PrCCSL*，规范的随机和动态系统的行为，以及复杂的要求相关的多个事件。为了形式化地分析PrCCSL* 中规定的系统行为/需求，将PrCCSL* 规范转换为随机UPPAAL模型以进行形式化验证。我们实现了一个自动翻译工具，即ProTL，它也可以使用UPPAAL-SMC作为分析后端对PrCCSL* 规范进行形式化分析。我们的方法证明了两个汽车系统的案例研究。
2019-10-31 cs.SE
A Formal Verification Technique for Architecture-based Embedded Systems in EAST-ADL
随着汽车嵌入式系统等软件密集型系统的复杂性显著增加，开发有质量保证的软件密集型系统是一项日益严峻的挑战。EAST-ADL是一种架构描述语言，旨在在安全关键汽车产品的开发中以多个抽象级别指定汽车嵌入式系统架构。在本文中，我们提出了一个基于架构的验证技术，增强了基于模型的开发过程中支持的EAST-ADL适应模型检查EAST-ADL规范。我们采用UPPAAL作为验证工具，以确保预测的功能行为的模型在EAST-ADL满足功能和实时要求。提出了基于体系结构的验证准则，并推导出符合该准则的转换规则。这使我们能够从EAST-ADL规范中提取相关信息，并生成可分析的UPPAAL模型。定义了EAST-ADL规范的形式化语义，这对EAST-ADL规范的自动验证至关重要。我们的方法是通过验证转向车系统单元的安全性来证明的。
2019-03-14 cs.SE
ProofWright: Towards Agentic Formal Verification of CUDA
Georgia Institute of Technology（佐治亚理工学院）；NVIDIA Research（英伟达研究院）；Stanford University（斯坦福大学）
ProofWright 通过整合自动形式验证与 LLM 代码生成，为 CUDA 核心提供内存安全、线程安全和语义正确性保证，验证了 74% 的生成内核，发现传统测试遗漏的细微错误。
2026-03-18 cs.SE
Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
University of Arizona（亚利桑那大学）
本文提出了一种可扩展的方法论，用于通过形式验证微服务系统架构，通过静态建模和SMT约束集实现形式验证，并验证其正确性和适用性。
2025-09-02 cs.LO cs.SE
Boost the Impact of Continuous Formal Verification in Industry
软件模型检验在过去的二十年里取得了长足的进步，但其可扩展性和适应性仍然是制约其实际应用的主要瓶颈之一。在这里，我们描述了一种通过利用持续集成和回归测试等实践将软件模型检验技术集成到DevOps文化中的方法。特别是，我们提出的方法着眼于修改的软件系统，因为它的最后一次验证，并提交给一个连续的形式化验证过程中，一组回归测试用例的指导下。我们的愿景是专注于开发人员，通过使用他们的主要软件开发方法和工具，将形式化验证技术集成到开发人员的工作流程中。
2019-07-17 cs.LO cs.SE
Smart Contracts Formal Verification: A Systematic Literature Review
本文系统综述智能合约形式化验证相关文献，梳理规格说明、验证工具与实验，并提出基于描述逻辑的替代验证方法。
2025-10-15 cs.LO cs.SE
Requirements, Formal Verification and Model transformations of an Agent-based System: A CASE STUDY
在多智能体系统的软件规格工程中，最具挑战性的任务之一是确保正确性。由于这些系统具有高并发性，通常具有动态环境，这些系统的形式化规范和验证以及从抽象到具体概念的逐步细化在系统正确性中起着重要作用。我们的目标是正式规范，分析功能以及非功能属性逐步细化从抽象到具体的规范，然后形式化验证这些规范。多智能体系统是一个多进程并行工作的并发系统。我们已经在盖亚多智能体方法与有限状态过程为基础的有限自动机技术，因此，我们已经定义了我们的系统的正式规格，检查的正确性和验证所有可能的流程并发执行这些规格。我们的贡献在于将基于组织抽象的需求规范转换为基于有限自动机的可执行形式化验证规范。我们已经考虑了一个案例研究，我们的多智能体系统，以确保正式的规范和验证。
2015-01-21 cs.MA cs.SE
Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
Microsoft Research（微软研究院）
该研究提出神经形式化验证（NFV），让AI编码智能体与成熟验证器结合，为主流语言开发者实现一键式程序验证，在Python编程问题数据集上取得了良好的验证效果。
2026-09-15 cs.PL cs.SE
Verifying Stochastic Behaviors of Decentralized Self-Adaptive Systems: A Formal Modeling and Simulation Based Approach
自适应软件被认为是最先进的方法，它的发展引起了人们的广泛关注。去中心化是设计和管理现代自适应软件系统复杂性的有效方法。然而，仍然存在巨大的挑战。一个主要的挑战是在设计和实现活动中将分散性与传统的自适应实现框架统一起来。一个是保证在高度动态和不确定的环境中运行的分散自适应系统所需的全局目标和性能。另一个挑战是预测系统的内部变化对其自适应环境的影响。为了解决这些问题，我们将关注点分离的机制与使用时间自动机的建模方法相结合，以允许系统进行分析和验证。采用时间计算树逻辑描述系统目标，并通过动态环境下的随机仿真实验验证了分散自适应系统的自适应特性。在本文中，我们提取了一个激励的例子，从实际应用中的无人机应急任务场景。最后，以该动机为例对整个方法进行了评价和说明，统计结果可作为无人机在赛博物理空间布局规划的参考。
2017-12-28 cs.FL cs.SE
Software is infrastructure: failures, successes, costs, and the case for formal verification
Université Paris Cité（巴黎西岱大学）；University of Malta（马耳他大学）；University of Southern Denmark（南丹麦大学）；King’s College London（伦敦国王学院）
本文探讨了软件在现代社会中的重要性及质量缺陷带来的成本，主张通过形式验证和程序分析来提升软件可靠性。
2026-01-29 cs.CY cs.SE
Using Formal Methods for Autonomous Systems: Five Recipes for Formal Verification
形式方法是用于软件设计和工程的基于数学的技术，它能够对系统的行为进行明确的描述和推理。自主系统使用软件在没有人类控制的情况下做出决策，通常嵌入在机器人系统中，通常是安全关键的，并且越来越多地被引入日常环境中。自治系统需要健壮的开发和验证方法，但形式化方法的实践者经常被问到：为什么要使用自治系统的形式化方法？为了回答这个问题，这份立场文件描述了从文献中收集的五个配方，用于正式验证自治系统的各个方面。配方的例子是如何形式化方法可以成为一个有效的工具，自主系统的开发和验证。在设计过程中，它们可以明确地描述需求;在开发过程中，可以根据需求验证正式规范;可以从验证的规范合成软件组件;可以在运行时监控行为并与原始规范进行比较。现代形式化方法通常包括高度自动化的工具支持，这使得能够对系统的状态空间进行详尽的检查。本文认为，形式化方法是一个强大的工具，与其他强大的软件工程技术的发展技术的剧目安全自治系统。
2021-07-28 cs.LO cs.SE
Formal Verification of Autonomous Vehicle Platooning
University of Sheffield（谢菲尔德大学）
预计在不久的将来，我们的高速公路上将有多辆自动驾驶汽车组成车队或车队。然而，在部署这样的车队之前，必须对这些车队中车辆的新自主行为进行认证。车辆排队的一个适当的表示是作为一个多智能体系统，其中每个代理捕获的“自主决策”进行的每辆车。为了保证车辆队列中的自主决策智能体不违反安全要求，我们使用了形式化验证。然而，由于用于验证代理代码的形式化验证技术不能扩展到整个系统，并且由于全局验证技术不能捕获自治行为的基本验证，因此我们使用两种方法的组合。这种混合策略使我们不仅可以验证系统模型的安全要求，还可以验证用于对自动驾驶汽车进行编程的实际代理代码的安全要求。
2016-02-04 cs.AI cs.SE
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
本文提出一种符合功能安全标准的 PLC 程序形式化验证即服务，通过外部专家降低组织内部培训成本，并扩展至时间相关及专有技术保护组件建模，在 CERN 与 GSI 粒子加速器安全关键装置中验证了其有效性。
2025-02-26 cs.LO cs.SE
Causality and Responsibility for Formal Verification and Beyond
King's College London（伦敦国王学院）
由哈尔彭和珀尔定义的实际因果关系理论及其定量度量--责任度--在计算机科学的各个领域都被证明是非常有用的，因为它产生的结果与我们的直觉之间有很好的匹配。在本文中，我描述了因果关系的应用形式化验证，即解释反例，细化的覆盖度量，和符号轨迹评估。我还简要讨论了因果关系的法律推理的最新应用。
2016-08-29 cs.AI cs.SE
Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development
在基于工业模型的开发（MBD）框架中，通常使用文本描述非正式地指定需求。为了使正式方法的应用，这些规格需要正式的输入语言的所有正式工具，应适用于分析模型在不同的发展水平。在本文中，我们提出了一个统一的方法，计算机辅助的正式规格说明的要求和他们的完全自动化翻译成规约语言的不同的验证工具。我们考虑一个两阶段的MBD方案，第一个Simulink模型的开发，自动生成可执行代码。我们（i）提出了一种规约语言和一个原型工具，用于正式但仍然是文本的需求规范，（ii）展示了如何将这些需求自动转换为Simulink Design Verifier的输入语言，用于验证Simulink模型和BTC EmbeddedValidator的源代码验证，以及（iii）展示了我们的统一框架如何在自动化形式化验证之外还实现测试用例的自动化生成。
2019-06-17 cs.LO cs.SE
VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees
Lund University（隆德大学）；Linköping University（林雪平大学）
本文提出训练后优化框架生成验证友好型神经网络（VNNs），在保持预测性能的同时提升形式化验证可行性，从而高效地为更多网络建立硬鲁棒性保证。
2024-06-10 cs.LG cs.SE
Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
Formal Methods and Tools Lab, ISTI–CNR, Pisa, Italy（ISTI-国家研究委员会，意大利比萨）
本文基于Uppaal对合同自动机运行环境进行形式化建模、验证与测试，以提升开源分布式应用的可靠性。
2026-03-04 cs.FL cs.SE
Simulator Semantics for System Level Formal Verification
Sapienza University of Rome（罗马第一大学）
本文提出系统级形式验证中模拟器的正式语义，以解决模拟器行为未被形式化建模的问题，确保验证方法的正确性。
2015-09-24 cs.SE cs.SY eess.SY
Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges
MIT-IBM Watson AI Lab（MIT-IBM沃森人工智能实验室）；IBM Research（IBM研究院）；Massachusetts Institute of Technology（麻省理工学院）
自动驾驶系统--如自动驾驶汽车、自动驾驶无人机和自动化列车--必须有强大的安全保障。在过去的十年中，基于形式化方法的技术在为大型软件系统（包括操作系统内核、加密协议和无人机控制软件）提供强正确性保证方面取得了一些成功。这些成功表明，通过构造正式的、计算机检查的正确性证明来确保自治系统的安全性是可能的。本文确定了现有的形式化验证技术的三个假设，解释了这些假设如何限制验证在自治系统中的适用性，并总结了初步工作，以提高形式化验证提供的证据的强度。
2020-06-15 cs.AI cs.LG cs.SE
Contribution to the Formal Specification and Verification of a Multi-Agent Robotic System
IRISA（法国国家信息与自动化研究所布列塔尼大西洋分部）；University of South Brittany（南布列塔尼大学）；The Islamia University of Bahawalpur（巴哈瓦尔布尔伊斯兰大学）
重要的是要有多智能体机器人系统规范，以确保正确性，安全性和活性。由于这些系统具有并发性，并且通常具有动态环境，因此这些系统的形式化规范和验证以及从抽象到具体概念的逐步细化在系统正确性中起着重要作用。形式化验证用于系统空间的详尽调查，从而确保排除行为中未检测到的故障。我们构建系统的子组件，基于软件体系结构的增量。挑战是开发一个安全的多智能体机器人系统，更具体地说，以确保安全性和活性的正确性。基于模型检测的形式化规约具有灵活性强、语法具体等特点，对多智能体机器人系统的正确性起着至关重要的作用。由于这类系统具有高并发性，且大多数情况下是动态的，因此形式化地验证其安全性和活性是非常重要的。我们已经考虑了一个案例研究的多智能体机器人系统的仓库之间的股票运输，以证明我们的正式方法。我们提出的开发方法允许在规范定义期间进行形式化验证。开发过程分为需求规范、验证规范、体系结构规范和实现四个主要阶段。
2015-10-02 cs.AI cs.MA cs.SE
SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits
本文将密码电路抗故障验证问题形式化为NP完全问题，提出将其编码为布尔可满足性（SAT）问题并利用现成SAT求解器求解的方法，在开源工具FIRMER中实现了该方案，其实验验证效率与可扩展性显著优于现有方法。
2023-07-02 cs.AR cs.CR cs.SE
Towards the Formal Specification and Verification of Maple Programs
在本文中，我们提出了我们正在进行的工作和初步结果的形式规范和验证的MiniMaple（一个重要的子集Maple轻微扩展）程序。我们工作的主要目标是在这些程序中找到行为错误。通过静态分析确定其规格。这项任务是更复杂的广泛使用的计算机代数语言，如Maple，因为这些是从根本上不同于经典的语言：它们支持非标准类型的对象，如符号，未评估的表达式和多项式，并需要抽象的计算机代数概念和对象，如环和排序等作为一个出发点，我们已经定义和形式化的语法，语义，类型系统和规约语言的MiniMaple。
2012-07-10 cs.LO cs.MS cs.PL
