What Good Are Strong Specifications?
轻量级形式化方法的经验表明，程序员愿意编写规范，如果它能给他们的日常开发活动带来切实的好处。本文考虑了更强的规范，并研究了它们是否可以作为一种增量实践来部署，从而带来额外的好处，而不会带来不可接受的昂贵成本。我们引入了一种方法，扩展了契约式设计，以先决条件，后置条件和不变量的形式编写功能属性的强规范。该方法的目的是让那些不熟悉正式技术但对编写简单规范感到舒适的开发人员感到满意。我们评估的成本和使用强规格的好处，通过应用该方法来测试数据结构实现写在Eiffel和C#。在我们广泛的实验中，针对强规范的测试检测到的bug是标准合约的两倍，在测试时的注释负担和运行时性能方面具有合理的开销。在广泛的软件质量形式化技术中，针对强规范的测试是一个“甜蜜点”，具有有利的收益与努力之比。
2013-02-22 cs.SE
An Entry Point for Formal Methods: Specification and Analysis of Event Logs
形式化规约语言由于完备验证方法所面临的严重的可扩展性问题而长期处于停滞状态。可扩展性验证承诺使用正式的规范来自动化部分更可扩展的测试艺术，但尚未广泛应用于实际系统，并且由于在线监控仪器的成本和复杂性而经常动摇。在本文中，我们将讨论正在进行的工作，应用基于事件的规范系统的日志机制的火星科学实验室在喷气推进实验室的任务。通过专注于日志分析，我们利用“仪器”已经实现，并与航天器进行通信所需的。我们认为，这项工作既显示了一个实用的方法，使用正式的规格测试，并打开有趣的研究途径，包括一个具有挑战性的规格学习问题。
2010-03-08 cs.SE
Implementation-First Approach of Developing Formal Semantics of a Simulation Language in VDM-SL
形式规格说明是严格软件实现的基础。VDM-SL是一种形式化的规约语言，具有广泛的可执行子集。包括VDM-SL在内的VDM系列的成功案例表明，制定经过良好测试的可执行规范可以降低实施阶段的成本。本文介绍并讨论了规格说明和实现的逆序。一个多智能体的仿真语言称为\remobidyc的发展进行了描述和研究的情况下，定义一个正式的规范后，最初的实施和反映到实施代码的规范。
2023-03-27 cs.SE
Generating Logical Specifications from Requirements Models for Deduction-based Formal Verification
工作涉及自动生成的逻辑规格的需求模型。以这种方式获得的逻辑规范可以使用演绎推理进行形式化验证。形式化验证关注模型行为的正确性。需求工程的可靠性对于软件开发过程的所有阶段都是必不可少的。演绎推理是一种重要的形式化方法。然而，逻辑规范，被认为是一组时序逻辑公式，很难指定手动经验不足的用户，这一事实可以被视为一个重大障碍，实际使用的演绎为基础的验证工具。提出了一种利用UML图建立需求模型的方法，包括逻辑规格说明。将活动图组织到预定义的工作流模式中可以自动提取逻辑规范。所提出的方法的关键方面是集成的需求工程阶段和逻辑规格的自动生成。提出了一种基于演绎的验证系统。推理过程可以基于语义表方法。提供了一个简单的需求获取和验证的示例。
2014-02-09 cs.SE
A Survey of Smart Contract Formal Specification and Verification
智能合约是一种计算机程序，允许用户在区块链平台上自动执行操作。鉴于智能合约在支持包括供应链、金融、法律和医疗服务在内的各行业重要活动方面的重要性，对验证和确认技术的需求非常强烈。然而，绝大多数智能合约缺乏任何形式的规范，这对于确定其正确性至关重要。在本次调查中，我们调查了文献中提出的智能合约的正式模型和规范，并提出了一个系统的概述，以了解共同的趋势。我们还讨论了目前使用的方法，在验证这些属性的规格，并确定差距，希望认识到有前途的方向，为未来的工作。
2021-04-19 cs.SE
Refinement-Based Specification: Requirements and Architecture
本文介绍了系统的需求和体系结构w.r.t.它们的分解和提炼它还介绍了细化层和基于细化的验证的想法。
2014-04-29 cs.SE
How Powerful are LLMs in Generating Formal Program Specifications?
Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of the Chinese Academy of Sciences（中国科学院大学）；School of Computer Science & Key Lab. of High Confidence Software Technologies of Ministry of Education, Peking University（北京大学计算机学院及教育部高可信软件工程重点实验室）；Zhongguancun Lab.（中关村实验室）
该研究引入基于Rocq的Coins评估框架，在HumanEval数据集上开展大规模研究，发现LLMs生成形式化程序规约仍具挑战，准确的规约评估是理解其能力的核心。
2026-08-14 cs.SE
Extracting Formal Specifications from Documents Using LLMs for Automated Testing
针对从软件文档中人工提取形式化规约耗时易错的问题，本研究评估了GPT-4o等LLMs的端到端提取能力，并提出“先标注后转换”的两阶段方法，使正确提取数量增加29.2%，最高准确率达71.6%。
2025-04-02 cs.SE
Model-based Analysis and Specification of Functional Requirements and Tests for Complex Automotive Systems
针对汽车系统复杂性导致需求与测试规范困难的问题，提出基于MBSE的方法，通过早期识别验证关注点并设计测试驱动建模，经KOSTAL及学生项目验证，可改善规范流程。
2023-11-15 cs.SE
SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
SpecGen利用大型语言模型通过对话生成和变异选择两阶段方法，自动生成形式化程序规范，在基准测试中优于现有方法。
2025-02-25 cs.SE
Can Formal Specifications Be Synthesized from Tests Alone?
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
该研究提出仅用测试代码和动态执行轨迹，结合LLM与有界模型检查合成形式化规格说明的方法，在SpecGenBench基准上取得初步效果，同时指出需解决检查器兼容性等关键挑战。
2026-08-14 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 survey on formal specification and verification of separation kernels
分离内核是安全和安全关键系统的基础软件，它为托管应用程序提供空间和时间分离以及分区之间的受控信息流。分离核在关键领域的应用要求通过形式化验证来验证分离核的正确性。据我们所知，没有关于这一主题的调查文件。本文综述了分离核的形式化描述和验证。本文首先介绍了分离核的概念和背景，并对不同分离核进行了比较。然后，我们调查了自2000年以来关于这个主题的最新技术。最后，通过详细的比较和讨论，对研究工作进行了总结.
2016-07-10 cs.SE
Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
Politecnico di Milano（米兰理工大学）
本文提出基于代理的方法，从非结构化规范中自动生成符合验证要求的形式化属性，通过提取、过滤和翻译三个模块，实现语义对齐，实验表明其在三个场景中准确率达77.8%。
2026-04-20 cs.SE
Model-based generation of natural language specifications
形式化模型的应用为软件和系统开发提供了许多好处，然而，形式语言的学习曲线可能是工业项目的关键因素。因此，反映正式模型所有方面的自然语言规范可能有助于理解模型，并且对于不知道相应形式语言的涉众特别有用。此外，在模型被修改的情况下，从模型自动生成文档将取代手动更新文档。本文介绍了一个正在进行的工作产生自然语言规格从形式化模型。我们的目标是从基本的建模工件（如数据类型、状态机和架构组件）生成英文文档。为了允许进一步的正式分析生成的规范，我们限制英语的子集，Attempto控制英语。
2016-12-06 cs.SE
Specification and Verification of Context-dependent Services
当前用于服务的发现、规范和提供的方法忽略了服务契约与服务可以保证其契约的条件之间的关系。此外，它们没有使用正式的方法来指定服务、契约和组合。没有正式的基础，就不可能通过形式化验证来证明服务组合的正确性条件和服务条款中合同义务的履行。我们在本文中纠正这种情况。我们提出了一个正式的定义与上下文相关的合同服务。我们定义了一个组合理论的服务与上下文相关的合同考虑到功能，非功能，法律和上下文信息。最后，我们提出了一个形式化验证方法，将服务组合的形式化规范转换为扩展的时间自动机，可以使用模型检验工具UPPAAL进行验证。
2011-08-11 cs.SE
LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software
North Dakota State University（北达科他州立大学）
该研究探索用大语言模型从需求文档和生产源代码生成Alloy形式规范及推导可执行测试用例，在Flipper和Cerberus库上评估，发现能揭示约束级缺陷，基于代码的规范方差更低，为生产软件自动测试推导提供了新方法。
2026-07-22 cs.SE
Validating Formal Specifications with LLM-generated Test Cases
INESC TEC；Universidade do Minho（米尼奥大学）
本文利用GPT-5等大语言模型自动生成测试用例，用于验证形式规范的正确性，有效检测人类编写错误的规范。
2026-02-18 cs.SE
Formal FocusST Specification of CAN
提出了一种基于FocusST框架的控制器局域网（CAN）协议的形式化规范.我们正式描述了协议的核心组件，这提供了一个基础，进一步的形式化分析，使用Isabelle/HOL定理证明。
2018-11-20 cs.FL cs.SE
Formal refinement of extended state machines
在传统的正式开发过程中，例如使用B方法，非正式的用户需求（手动）转换为一个全球性的抽象正式规范。这种翻译尤其难以实现。Event-B方法的开发是为了使用逐步细化来逐步和正式地构建这样的规范。每个增量都考虑到新的属性和系统方面。在本文中，我们建议耦合一个图形符号称为代数状态转换图（ASTD）与事件B规范，以便更好地理解软件的行为。动态行为由ASTD捕获，ASTD基于自动机和进程代数运算符，而数据模型则通过Event-B规范描述。我们提出了一种方法来逐步完善这种规范耦合，考虑到新的细化关系和控制规范和数据规范之间的一致性条件。我们比较使用每种方法获得的规范的可读性和证明的复杂性。传统的方法和我们的方法的优点和缺点进行了讨论。整个过程通过铁路CBTC类案例研究来说明。我们的方法得到了将ASTD翻译成B和将Event-B翻译成B的工具的支持。
2016-06-07 cs.SE
Adventures in FRET and Specification
本文回顾了使用NASA的FRET工具形式化需求的四个案例研究，证实其作为需求获取框架及提供需求到规格说明可追溯性的适用性。
2025-03-31 cs.SE
Having Fun in Learning Formal Specifications
为我们的软件提供正式的规范有很多好处。然而，教学生做到这一点并不总是容易的，因为正式方法的课程通常被学生认为是枯燥的。本文介绍了一个名为FormalZ的游戏，教师可以用它来介绍他们的课堂上的一些变化。学生可以在玩游戏的过程中获得一些乐趣，同时也可以学习以前置条件和后置条件的形式编写正式规范的基础知识。与现有的软件工程主题教育游戏（如Pex和Code Defenders）不同，FormalZ采用了深度游戏化的方法，在游戏中扮演更重要的角色，以产生更多的参与度。这篇简短的论文介绍了我们正在进行的工作：FormalZ的第一个实现以及初步用户评估的结果。这个实现在功能上是完整的，并且经过了测试，但是它的用户界面的改进仍然是未来的工作。
2019-03-01 cs.SE
Requirements variability specification for data intensive software
目前，特征建模技术在软件需求规约中的应用，增加了对数据密集型软件产品线（DISPLs）需求建模的变化支持。它被认为是表达不同产品需求之间的共性和可变性的最简单和最有效的方法。最近的几项工作，在DISPL的要求，处理数据的变化，不同的模型，这是远离现实世界的概念。这导致了分析、设计、实现和维护这种可变性的困难。然而，这项工作提出了一个软件需求规格说明方法的基础上的概念更接近的性质，这是遗传学的启发。基于遗传学的方法学在DISPL的需求变异性描述中取得了重要的成果，特征模型中的特征和关系丰富了需求变异性管理，这在目前的相关研究中还没有得到考虑，基于遗传学的方法学在数据密集型软件需求变异性描述中有着广阔的应用前景。
2019-04-28 cs.SE
Formal Consistency Checking over Specifications in Natural Languages
系统开发的早期阶段包括概述所需的功能，如功能，可用性或可用性。规范是从这些特征中派生出来的，这些特征将自然语言中的模糊概念具体化。规范验证的挑战来自不同表示之间的语法和语义差距以及自动工具的需求。在本文中，我们提出了一个需求一致性维护框架，以产生一致的表示。第一部分是从描述功能的自然语言到具有时间抽象的形式逻辑的自动转换。它通过添加语义推理和对划分输入和输出变量的支持来扩展纯句法分析。第二部分是使用综合技术来检查需求在可实现性方面是否一致。当过程失败时，将报告导致不一致的公式以定位问题。
2014-10-08 cs.SE
SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
Nanjing University（南京大学）
针对现有LLM规范综合方法在复杂程序上易失效的问题，提出SpecAgent智能体框架，通过依赖感知规划、RAG、智能体修复与评判，在真实C程序上实现96.82%精确率与88.95%召回率，并成功解决604个验证目标。
2026-10-06 cs.SE
SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis
School of Computer Science, Peking University（北京大学计算机学院）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Tencent（腾讯）
本文提出SpecRL框架，利用负测试比例作为规范完整性的信号，提升规范强度和验证成功率，实验显示其在不同模型规模上表现优异。
2026-07-15 cs.SE
Formal requirement and architecture specifications of a multi-agent robotic system
多智能体机器人系统的规范工程中最具挑战性的任务之一是正式指定和架构的系统，特别是作为一个多智能体机器人系统是并发的并发处理，往往有动态的环境。形式化的需求和体系结构规范以及从抽象到具体概念的逐步细化在系统的形式化中起着重要作用。本文提出了正式的需求和架构规范方面的一种方法，支持分析方面的功能以及非功能属性逐步细化从抽象到具体的规范和正式的架构定义。这些正式的规范已被举例说明的案例研究。随着形式化规范技术的日益成熟，我们构建正确的复杂多智能体机器人系统的能力也在迅速增长。
2015-01-21 cs.MA 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
StaBL - State Based Language for Specification of Web Applications
背景和动机：正式规约语言的使用是稀缺的Web应用程序开发相比，安全关键/硬件系统。问题/Problem：一个恰当的形式化规约语言应该具备以下特征：首先，它应该具有定义良好的语义，这样用它编写的规约就不会有内在的二义性。其次，它应该有工具支持自动检测规范错误。此外，对于像Web开发这样的领域，规范形式主义建立在熟悉的符号上是很重要的，因为在这些领域中学习高度数学化的符号的好处被认为是很低的。主要想法/结果：这项工作提出了一个基于状态的语言的启发Statecharts称为StaBL的Web应用程序的规范，以及如何StaBL可以用于编写这样的规范。我们还提出了修改的语言w.r.t Statechart，便于编写模块化和可扩展的规范。贡献：特别是，我们提出了本地作用域变量与状态间数据流的功能。我们总结了我们的经验，开发规范与StaBL，这表明，StaBL规范，一方面，能够捕捉最基本的元素的功能方面的Web应用程序，而前述的冗长的常规程序设计语言。
2019-01-08 cs.SE
Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework
许多项目专用语言，包括特别是过滤语言，是使用以自然语言编写的非正式规范来定义的。这导致了这些语言规范中的歧义和错误。本文报道了一个工业实验上使用的工具支持的语言规范框架（K）的过滤语言的语法和语义的正式规范具有类似的复杂性，现实生活中的项目。这个实验的目的是估计，在一个特定的工业环境中，正式指定一个包过滤语言使用工具支持的正式方法的困难和好处。
2017-01-30 cs.PL cs.SE
ViSpec: A graphical tool for elicitation of MTL requirements
阻碍形式化方法广泛应用的主要障碍之一是形式化规范的获取。正式的规范有助于安全关键机器人系统的测试和验证过程。然而，处理形式语言的复杂性是困难的，并且需要许多系统开发人员不具备的形式逻辑方面的高水平专业知识。在这项工作中，我们提出了一个图形化的工具，设计的开发和可视化的正式规范的人，没有受过训练的形式逻辑。该工具使用户能够使用图形化的形式主义，然后自动转换为度量时态逻辑（MTL）的规格。为了评估我们的工具的有效性，我们还设计并进行了一项可用性研究，其中包括来自学术学生社区和行业的队列。我们的研究结果表明，这两组都能够定义具有高水平的准确性的正式要求。最后，我们提出了我们的工具的应用程序定义操作的机器人手术和自主四轴飞行器的安全操作规范。
2015-08-03 cs.SE
Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo
本文探索使用大语言模型从英文商业合同自动生成 Symboleo 形式化规范，通过 38 种提示组合实验发现该方法前景良好，但语法遵循和环境变量识别等问题仍需改进。
2024-11-24 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
KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base
Institute for Software Chinese Academy of Sciences（中国科学院软件研究所）
提出KBSpec方法，利用外部官方文档和内部验证器反馈的双源知识增强LLM，通过自演化知识库持续更新成功轨迹，无需调参或标注数据，在JML规约生成上验证通过率提升10-25%。
2026-08-17 cs.PL cs.SE
Compositional Specifications for ioco Testing
基于模型的测试是一种很有前途的黑盒软件和硬件测试技术，其中测试用例是从高层规格自动生成的。如今，系统通常由多个相互作用的组件组成，由于其复杂性，测试在设计过程中占了相当大的一部分工作和成本。利用系统规格说明的组合结构可以大大减少基于模型的测试工作。此外，通过测试系统的各个组件来推断系统的属性，可以让设计人员减少集成测试的数量。本文研究了IOCO-检验理论的合成性质。我们提出了一种新的方法来组成和隐藏操作，基于合同的设计和接口理论的启发。这些操作保留在合成和隐藏下兼容的行为，并删除不兼容的行为。由此产生的规范特征的输入序列的组件的单元测试是足以推断组件集成的正确性，而不需要进一步的测试。我们提供了一种方法，使用这些结果，以尽量减少集成测试的努力，但也发现潜在的弱点规范。虽然我们专注于异步模型和IOCO一致性关系，但由此产生的方法可以应用于更广泛的系统类别。
2019-04-15 cs.SE
Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method
为了开发物联网和/或CSP系统，我们需要考虑来自物理世界的连续数据和计算机系统中的离散数据。这样的系统被称为混合系统。由于连续数据的密集性，对混合系统进行软件测试以保证其可靠性并不容易。此外，多任务系统的状态空间的大小呈指数增长。混合系统的形式化描述可以帮助我们在计算机支持下形式化地验证给定系统的期望性质。本文提出了一种用CafeOBJ代数规约语言将给定的多任务混合系统的形式规约描述为观测转换系统的方法，并通过CafeOBJ解释器中实现的基于等式推理的证明得分方法对其进行了验证。
2020-10-28 cs.SE
Application of classical compilation techniques for syntactic and semantic analysis of specification written in Object Z
为诸如Object Z这样的正式规约语言构建解析器并不是一件容易的事情。事实上，它需要在编译领域比在正式规范领域的双重能力。在本文中，我们首先介绍了一些工具，用于分析规格书写在Z和对象Z显示各自的特点。然后，我们确定了一些常见的语义约束对象Z。最后，我们提出了一种基于传统的编译技术为对象Z构建解析器的方法。
2012-10-15 cs.SE
SysML/KAOS Domain Models and B System Specifications
在本文中，我们使用的SysML/KAOS需求工程方法，SysML的扩展，与KAOS目标模型的概念，B系统的形式化方法的组合。定义了从SysML/KAOS目标模型到B系统规范的转换规则。它们允许获得B系统规范的框架。为了完成它，我们定义了一种语言来表达与目标模型相关联的领域模型。这个领域模型的翻译给出了B系统规范的结构部分。本文的贡献在于描述了从SysML/KAOS领域模型到B系统规范的转换规则。我们还提出了这些规则的形式化验证，我们描述了一个开源的工具，实现的语言和规则。最后，我们提供了一个审查的应用程序的SysML/KAOS方法的案例研究，如混合ERTMS/ETCS 3级标准的正式规范。
2018-06-28 cs.SE
Requirements, Formal Verification and Model transformations of an Agent-based System: A CASE STUDY
在多智能体系统的软件规格工程中，最具挑战性的任务之一是确保正确性。由于这些系统具有高并发性，通常具有动态环境，这些系统的形式化规范和验证以及从抽象到具体概念的逐步细化在系统正确性中起着重要作用。我们的目标是正式规范，分析功能以及非功能属性逐步细化从抽象到具体的规范，然后形式化验证这些规范。多智能体系统是一个多进程并行工作的并发系统。我们已经在盖亚多智能体方法与有限状态过程为基础的有限自动机技术，因此，我们已经定义了我们的系统的正式规格，检查的正确性和验证所有可能的流程并发执行这些规格。我们的贡献在于将基于组织抽象的需求规范转换为基于有限自动机的可执行形式化验证规范。我们已经考虑了一个案例研究，我们的多智能体系统，以确保正式的规范和验证。
2015-01-21 cs.MA cs.SE
An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications
本研究首次实证评估大语言模型修复声明式形式规约的能力，设计含单/双智能体、自动提示等的12种修复设置，发现带自动提示的双智能体方案优于现有Alloy APR技术，为软件工程中基于智能体的技术奠定基础。
2025-06-12 cs.SE
A Formal Approach based on Fuzzy Logic for the Specification of Component-Based Interactive Systems
形式化方法被广泛认为是分布式交互系统的规范、仿真、开发和验证的一种强有力的工程方法。然而，大多数形式化方法依赖于二值逻辑，因此受限于该逻辑的公理：规范有效或无效，组件行为可实现或不可实现，安全属性保持或被违反，系统可用或不可用。特别是当问题域具有不确定性，不精确性和不确定性时，这些方法的应用成为一项具有挑战性的任务。为了克服形式化方法的严格工作方式所带来的局限性，本文的主要目的是通过使用模糊逻辑来放松形式化规范的布尔概念。本方法是基于焦点理论，一个基于模型的和严格的形式化方法，基于组件的交互式系统。这项工作的贡献是双重的：i）我们引入了规范技术的基础上，模糊逻辑，可用于顶部的焦点开发正式规范的定性方式; ii）我们部分扩展焦点理论的模糊，它允许规范的模糊组件和模糊的相互作用。虽然前者提供了一种方法来近似I/O行为下的不精确性，后者能够捕捉到一个更定量的规格属性，如可实现性。
2015-03-17 cs.LO cs.SE
A Component-Based Formal Language Workbench
CBS框架支持程序设计语言的基于组件的规范。它的目标是大大减少形式语言规范的工作量，从而鼓励语言开发人员更广泛地利用形式语义。CBS提供了一个广泛的可重用语言规范组件库，促进了语言及其规范的共同进化。在介绍了CBS及其正式定义之后，这篇简短的论文报告了根据定义为CBS生成IDE的工作进展。它还考虑了在其他形式语言工作台上支持基于组件的语言规格说明的可能性。
2019-12-23 cs.PL cs.SE
Formal specification of a security framework for smart contracts
随着智能合约的规模和复杂性不断增长，确保其正确性和安全性变得越来越困难。由于缺乏隔离机制，代码中的一个错误或漏洞都可能导致整个系统崩溃，因此智能合约升级可能特别危险。确保智能合约安全性的传统方法，包括DSL，审计和静态分析，都是在代码部署到区块链之前使用的，因此在部署之后没有提供任何保护。每次升级后，整个代码都需要再次验证，这是一个困难而耗时的过程，很容易出错。为了解决这些问题，开发了一个名为Cap 9的智能合约安全协议和框架。它为开发人员提供了以安全和健壮的方式执行升级的能力，并通过使用基于功能的低级别安全模型来提高隔离性和透明度。我们使用Isabelle/HOL开发了Cap 9框架的形式化规范，并证明了其一致性。本文提出了一种基于细化的方法，我们用来创建规范，以及讨论在这个过程中遇到的一些困难。
2020-01-13 cs.SE
Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
Faculty of Engineering, University of Porto（波尔图大学工程学院）；INESC TEC（TEC研究所）；INESC-ID（ID研究所）
本文利用LLMs和测试或acles自动为Dafny程序生成形式规范和验证注解，实验表明该方法在多数情况下有效，并展示了IDE集成的可行性。
2026-01-19 cs.SE
VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
本文提出VECOGEN工具，结合大型语言模型与形式化验证，通过接收形式化规范、自然语言规范和测试用例，自动生成并迭代改进C程序，在Codeforces的15个问题中成功解决13个，验证了该方法在安全关键应用中的有效性。
2025-04-07 cs.SE
GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel
在正式开发中，最昂贵的错误来源和更难检测的错误是规格说明期间的错误。因此，形式化开发的第一步通常包括展示规范的所有行为的集合，例如使用自动机。从这个观察开始，许多研究都是关于从行为规范（如UML）生成B机器的。然而，不进行向后验证。这就是为什么，我们提出了GeneSyst工具，其目的是生成一个自动机描述至少所有的行为规范。细化步骤被认为是在所产生的SLTS子自动机出现。
2010-04-13 cs.SE
FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
University of California, Riverside（加州大学河滨分校）；Lawrence Livermore National Laboratory（劳伦斯利弗莫尔国家实验室）
本研究推出首个带明确前后置条件的C++形式化规范数据集FormalSpecCpp，可用于规范推断工具基准测试、LLM微调等，助力程序验证与AI辅助软件开发研究。
2025-02-21 cs.AI cs.LG cs.PL
Enhancing Formal Software Specification with Artificial Intelligence
IBM Research（IBM研究院）
本文提出利用人工智能技术，通过轻量级数学符号和自然语言构建中间规范语言，以降低形式软件规范的开发成本并提高实现正确性。
2026-01-11 cs.AI cs.SE
Formal Specification & Analysis of Autonomous Systems in PrCCSL/Simulink Design Verifier
时序约束的建模和分析在汽车系统中至关重要。EAST-ADL是一种专用于安全关键型汽车嵌入式系统设计的领域特定架构语言。在大多数情况下，系统中有界数量的时间约束违反不会导致系统故障时，违反的结果是可以忽略的，称为弱硬（WH）。我们以前指定的EAST-ADL的时钟约束规约语言（CCSL）的时间约束和转换成正式的模型服从模型检验的CCSL的时间行为。以前的工作扩展在本文中包括支持概率分析的时间约束的背景下WH：概率扩展CCSL，称为PrCCSL，定义和EAST-ADL的时间约束与随机属性指定在PrCCSL。PrCCSL中扩展约束的语义被转换为可以使用SIMULINK DESIGN VERIFIER进行验证的证明目标模型。此外，提出了一组映射规则，以促进翻译的保证。我们的方法被证明在一个自主交通标志识别车辆的案例研究。
2018-06-20 cs.SE
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
Reverse Engineering from Assembler to Formal Specifications via Program Transformations
FermaT转换系统基于达勒姆大学、德蒙福特大学和Software Migrations Ltd.过去十六年进行的研究，是一个工业强度的形式转换引擎，在程序理解和语言迁移方面有许多应用。本文是一个案例研究，它使用自动化加上手动指导的转换和抽象转换为一个非常高层次的抽象规范的IBM 370汇编代码程序。
2001-05-04 cs.PL cs.SE
Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
本文提出VERIFAI项目，探索结合NLP、本体建模与LLM等方法，从非正式自然语言需求自动生成可验证形式化规格说明，并总结关键挑战与研究方向。
2025-08-28 cs.SE
Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis
本研究提出结合大型语言模型Deepseek-R1与Frama-C符号分析工具，从C代码生成ACSL形式化规约，探讨了意图与实现规约的差异及符号分析对规约质量的提升。
2025-04-29 cs.SE
ARSENAL: Automatic Requirements Specification Extraction from Natural Language
SRI International（SRI国际公司）；TTTech C. AG（TTTech股份公司）
需求是从利益相关者（客户、用户、操作员、设计师和工程师）的角度对复杂系统预期行为的非正式和半正式描述。然而，对于关键系统的设计、测试和验证，我们可以将需求转换为可以自动分析的形式化模型。ARSENAL是一个框架和方法，用于系统地将自然语言（NL）需求转换为可分析的形式化模型和逻辑规范。可以分析这些模型的一致性和可实现性。ARSENAL方法专门针对各个领域，但该方法足够通用，可以适应新的领域。
2016-04-20 cs.CL cs.SE
