Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification
传统上，从业者主要将形式化方法用于质量保证过程的一半：验证（我们构建的软件正确吗？）。另一半--验证（我们是否构建了正确的软件？）--相对来说，很少受到关注。虽然验证是基于精化的形式化方法的核心，其中每个新的精化步骤必须保留其抽象模型的所有属性，但验证通常被推迟到开发的最新阶段，此时模型可以自动执行。因此，在需求或其解释中的错误被发现得太晚了：通常在开发过程的最后。在本文中，我们提出了一种新的方法来检查符合性的需求和他们的正式细化为基础的规范在早期阶段的发展。我们提出的方法--“验证义务”--基于一个简单的想法，即验证和验证都是系统所有细化步骤的组成部分。
2021-02-11 cs.FL cs.SE
Refinement type contracts for verification of scientific investigative software
我们的科学知识越来越多地建立在软件输出上。定义数据分析管道和计算模型的用户代码对于自然科学和社会科学的研究是必不可少的，但很少有人知道如何确保其正确性。这种代码的结构和用于构建它的开发过程限制了传统测试方法的实用性。软件验证的形式化方法在确保代码正确性方面取得了巨大的成功，但通常需要比自然科学和社会科学更专业的培训，开发时间和资金。在这里，我们提出了一个Python库，它使用轻量级的形式化方法来提供正确性保证，而不需要专门的知识或大量的时间投资。我们的包提供了使用细化类型的函数入口和出口条件契约的运行时验证。它允许检查合同中的超属性，并提供自动测试用例生成来补充在线检查。我们共同开发了我们的工具与一个中型（$\approx$ 3000磅）软件包，它模拟决策的认知神经科学。除了帮助我们在开发周期的早期定位小错误之外，我们的工具还能够定位四个使用传统测试方法可能很难找到的错误。它还能够发现用户代码中不包含契约或细化类型注释的bug。这表明形式化方法可以用来验证科学软件的正确性，这是很难测试的主流方法。
2019-09-01 cs.SE
Feature Specification and Refinement with State Transition Diagrams
在本文中，我们介绍了一种图形规范技术，称为状态转换图（STD），并显示应用程序的功能交互问题。使用基于流的形式语义，我们提供了性病的细化规则。精化定义了STD规范上的实现关系。我们认为，功能作为一个特定的细化添加到一个给定的STD规范以前未指定的行为。然后，细化关系用于添加特征，并定义冲突特征的概念。我们的技术通过[25]中给出的一个例子的系统发展来证明。
2014-09-25 cs.SE
SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
Nanjing University（南京大学）；Nanyang Technological University（南洋理工大学）
本文提出SpecSyn，一种基于大语言模型的规范生成方法，通过分解程序并引入语义非等价变异和变体辨别机制，提升规范的语义强度，实验显示其在精度和召回率上显著优于现有方法。
2026-10-11 cs.SE
Structural Abstraction and Selective Refinement for Formal Verification
Institute of Computer Technology（计算机技术研究所）；TU Wien（维也纳技术大学）
针对复杂机器人环境安全验证耗时或失败问题，提出基于体素表示的结构抽象与结合CEGAR的选择性细化自动验证工作流，显著提升了模型检测效率。
2025-05-29 cs.RO cs.SE
SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java
安全关键Java（Safety-Critical Java，SCJ）是Java的一个版本，其目标是支持实时，嵌入式，安全关键软件的开发。特别是，SCJ通过引入实施更简单的体系结构和更简单的并发和内存模型的抽象来支持此类软件的认证。在本文中，我们提出了SCJ-Circus，一个面向细化的正式符号，支持规范和验证的低级别的编程模型，包括SCJ引入的新的抽象。SCJ-Circus是状态丰富进程代数Circus家族的一部分，因此，SCJ-Circus包括Circus结构，用于建模顺序和并发行为，实时和面向对象。我们在这里提出的语法和语义的SCJ-Circus，这是定义映射SCJ-Circus结构的标准Circus。这是基于现有的方法建模SCJ程序。我们还扩展了现有的马戏团为基础的细化策略，目标SCJ程序占SCJ马戏团模型的生成接近SCJ的实现。
2016-06-07 cs.LO cs.PL cs.SE
Refinement-based Specification and Security Analysis of Separation Kernels
在分离核的安全认证中，强制要求通过形式化方法来保证信息流的安全性。ARINC 653作为提高安全性的工业标准，已被主流分离内核所遵守。由于将安全和安全功能集成到一个分离内核中的新趋势，ARINC 653的安全性分析以及具有安全证明的形式化规范对于开发和认证符合ARINC 653的分离内核（ARINC SK）具有重要意义。提出了一种基于精化的ARINC SK规范开发和安全性分析方法。我们提出了一个通用的安全模型和逐步完善的框架。两个层次的功能规格的细化开发。对ARINC 653中分离内核的主要需求进行了建模，包括内核初始化、两级调度、分区和进程管理、分区间通信等。在Isabelle/HOL定理证明器中进行了形式化描述和安全性证明。我们已经审查了一个工业和两个开源的ARINC SK实现，即ARINC Works 653，XtratuM和POK的源代码，根据正式规范。在验证和代码审查过程中，发现ARINC 653标准及其实现中存在6个可能导致信息泄露的安全漏洞。
2017-02-20 cs.CR cs.SE
Managing LTL properties in Event-B refinement
事件B中的细化支持通过基于证据的逐步细化事件来开发系统。这种细化方法确保了安全属性得到保留，但需要额外的推理来建立活性和公平性。在本文中，我们提出的结果，允许两个正式的方法，事件-B和线性时序逻辑的紧密结合。特别是，我们展示了如何一类时序逻辑属性可以进行通过细化链的机器。细化步骤可以包括引入新事件、事件重命名和事件拆分。我们还确定了一个通用的活性属性，适用于细化链的初始系统的事件。该方法将帮助开发人员在开发的早期阶段验证线性时序逻辑属性，知道它们将在后期阶段被保留。我们通过一个简单的案例研究来说明结果。
2014-07-02 cs.SE
Proceedings 18th Refinement Workshop
精化是软件工程形式化方法的基石之一。细化是从抽象规范通过一系列基于抽象的步骤来开发更详细的设计或实现的过程，这些步骤相对于原始规范保持正确性。对Z、B、VDM和CSP等语言基础的研究使它们在某些工业部门得到了广泛的使用，例如，那些有安全或安全关键问题的人。除了精确的规范，形式化方法还允许精确和可验证的开发的可能性，正如精化的概念所捕获的那样。第18届精炼研讨会作为FLoC 2018的一部分在英国牛津举行。
2018-10-20 cs.LO cs.PL cs.SE
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
本研究形式化自动驾驶的RSS模型，用KeYmaera X证明其纵向安全性，并通过精化与编译保持安全属性，最终生成可测试的Python代码。
2023-05-15 cs.LO cs.SE cs.SY
Can Formal Specifications Be Synthesized from Tests Alone?
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
该研究提出仅用测试代码和动态执行轨迹，结合LLM与有界模型检查合成形式化规格说明的方法，在SpecGenBench基准上取得初步效果，同时指出需解决检查器兼容性等关键挑战。
2026-08-14 cs.SE
Dependability Engineering in Isabelle
在本文中，我们介绍了一个过程中的形式化系统开发支持的交互式定理证明在一个专用的Isabelle框架。这个伊莎贝尔基础设施框架实现规范和验证的循环过程中的攻击树分析密切相关的正式细化的规范。这个过程是循环的：在一个重复的迭代中，细化将更多的细节添加到系统规范中。如何找到下一个细化步骤是一个已知的难题：这个问题是通过使用Kripke结构和CTL逻辑的基于攻击的分析来解决的。我们把这个循环过程称为精炼-风险循环（RR-循环）。它最初是为了物联网医疗保健系统的安全和隐私而开发的，但更普遍地适用于安全性，即一般的可靠性。在本文中，我们提出了扩展的伊莎贝尔基础设施框架实现了一个正式的概念，属性保持细化交织攻击树分析的RR周期。该过程说明了规范的发展和隐私分析的移动冠状病毒预警应用程序。
2021-12-08 cs.CR cs.SE
Intent-aligned Formal Specification Synthesis via Traceable Refinement
Amazon Web Services（亚马逊云服务）；Harvard University（哈佛大学）
本文提出VeriSpecGen框架，通过需求级归因和局部修复生成意图对齐的规范，提升规范合成的准确性和效率。
2026-04-12 cs.AI cs.LG cs.LO
Tool-Assisted Multi-Facet Analysis of Formal Specifications (Using Alelier-B and ProB)
软件系统的工具辅助分析和方便的指导实践的正式方法仍然是激励的挑战。本文将讨论这些挑战。本文从多个方面对形式规格说明进行了分析。B方法和Atelier-B工具用于形式规范、安全属性分析和改进。ProB工具用于补充模型检验的研究，它有助于发现错误，从而改善以前的规格。
2009-10-09 cs.SE
Formal requirement and architecture specifications of a multi-agent robotic system
多智能体机器人系统的规范工程中最具挑战性的任务之一是正式指定和架构的系统，特别是作为一个多智能体机器人系统是并发的并发处理，往往有动态的环境。形式化的需求和体系结构规范以及从抽象到具体概念的逐步细化在系统的形式化中起着重要作用。本文提出了正式的需求和架构规范方面的一种方法，支持分析方面的功能以及非功能属性逐步细化从抽象到具体的规范和正式的架构定义。这些正式的规范已被举例说明的案例研究。随着形式化规范技术的日益成熟，我们构建正确的复杂多智能体机器人系统的能力也在迅速增长。
2015-01-21 cs.MA cs.SE
Formalizing and validating properties in Asmeta with Large Language Models (Extended Abstract)
University of Bergamo（贝加莫大学）
本文探讨将大型语言模型集成到Asmeta框架中，帮助用户定义、形式化、解释和验证时间属性，通过示例展示这种集成的可行性与潜在优势。
2026-03-16 cs.SE
Proceedings 16th International Refinement Workshop
第16届BCS-FACS精炼研讨会于2013年6月11日在芬兰图尔库与iFM 2013共同举办。本卷载有经同行审查后选定在讲习班上介绍的6篇论文。这些论文涵盖了细化理论和应用方面的广泛主题。精化是软件工程形式化方法的基石之一：从抽象规范通过一系列基于抽象的步骤开发更详细的设计或实现的过程，这些步骤相对于原始规范保持正确性。
2013-05-24 cs.LO cs.SE
Towards Large Language Model Aided Program Refinement
National University of Singapore（新加坡国立大学）；Griffith University（格里菲斯大学）；Peking University（北京大学）；Singapore Institute of Technology（新加坡科技设计大学）；Shanghai Jiaotong University（上海交通大学）；Singapore Management University（新加坡管理大学）
针对传统程序细化缺乏自动化及LLM生成代码不可靠的问题，提出LLM4PR工具，结合形式化细化演算与LLM自动生成并验证代码，确保代码正确性。
2024-06-26 cs.AI cs.CL cs.SE
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
HSA基金会已经制定了HSA平台系统架构规范，该规范在解决明确和一致的方法来指定弱一致内存的需求方面有很大的帮助。HSA是用自然语言指定的，这使得它对多种模糊的解释开放，并且可能在硬件和软件中实现它时出现错误。在本文中，我们提出了一个形式化的HSA模型，可用于并发软件应用程序的开发和验证，以及在开发和验证的HSA兼容平台本身。我们使用Event-B语言来建立一个可证明正确的层次结构的模型，从最抽象的HSA接近实现级别的详细细化。我们的内存模型是通用的，因为它们代表了任意数量的主机，程序和指令交织。我们使用精化来推理这样的一般模型。使用罗丹工具，我们能够建模和验证整个层次的模型使用证明，以建立每个细化是正确的。我们定义了一个自动化的验证方法，使我们能够测试模型的基线符合性对一套已发布的HSA石蕊测试。一旦我们完成了模型验证，我们开发了一个覆盖率驱动的方法，从事件B模型和用户指定的覆盖率模型中提取更丰富的测试集。这些测试用于硬件和软件系统的广泛回归测试。我们的方法的细化为基础的正式建模，基线符合性测试的模型和覆盖率驱动的测试提取使用单一的语言的事件-B是一种新的方式来解决所面临的一个关键挑战的设计和验证的多核系统。
2016-05-16 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
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Lancaster University（兰卡斯特大学）；Tsinghua University（清华大学）；Harbin Institute of Technology（哈尔滨工业大学）；Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）
提出Forge管道，结合Vibe编码与模型驱动工程，通过多种形式化验证（Dafny、CSP、Isabelle）迭代修正LLM生成的Java代码，生成符合安全标准的验证证据。
2026-06-24 cs.FL cs.SE
Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
University of Oxford（牛津大学）
该研究提出Syntropy框架，结合多方会话类型规范与大语言模型合成无死锁通信协议精化，经评估其有效性达95.6%-99.5%，可生成多样且语法正确的协议精化方案。
2026-10-14 cs.AI cs.SE
Incremental Database Design using UML-B and Event-B
许多关键系统的正确操作依赖于底层数据库的数据一致性和完整性属性。因此，一个可验证的和严格的数据库设计过程是非常可取的。本研究的目的是调查和提供一个全面和实用的方法，通过分层细化正式的方法建模数据库。该方法是由一些案例研究，使用UML-B的抽象和细化和验证与罗丹工具的指导。UML-B是Event-B形式主义的图形表示，Rodin工具支持Event-B和UML-B的验证。我们的方法指导开发人员通过分层细化在UML-B中建模关系数据库，并指定数据库上的必要约束和操作。
2018-05-15 cs.DB cs.LO cs.SE
On Formal Methods for Collective Adaptive System Engineering. {Scalable Approximated, Spatial} Analysis Techniques. Extended Abstract
在这个扩展的摘要中，简要介绍了形式化方法在系统工程中的作用。然后讨论了两个基于坚实的数学理论的有用的分析技术的例子，以及已经建立的支持这种技术的软件工具。第一种技术是可扩展的近似人口DTMC模型检查。第二个是闭包空间的空间模型检验。这两种技术都是在欧盟资助的QUANTICOL项目的背景下开发的。
2016-07-08 cs.LO cs.PF cs.SE
The Unit-B Method -- Refinement Guided by Progress Concerns
我们提出了Unit-B，一个正式的方法的灵感来自事件B和UNITY。单元B旨在逐步设计满足安全性和活性特性的软件系统。该方法的特点是新的概念，粗和细的时间表，一个概括的弱和强的公平性指定事件的调度假设。基于事件时间表，我们提出了证明规则，原因的进展性质和细化顺序保持活性和安全属性。我们通过一个例子来说明我们的方法，表明系统开发不仅可以由安全性，而且还可以由活性要求来驱动。
2020-03-31 cs.LO cs.SE cs.SY
