Proceedings 18th Refinement Workshop
精化是软件工程形式化方法的基石之一。细化是从抽象规范通过一系列基于抽象的步骤来开发更详细的设计或实现的过程，这些步骤相对于原始规范保持正确性。对Z、B、VDM和CSP等语言基础的研究使它们在某些工业部门得到了广泛的使用，例如，那些有安全或安全关键问题的人。除了精确的规范，形式化方法还允许精确和可验证的开发的可能性，正如精化的概念所捕获的那样。第18届精炼研讨会作为FLoC 2018的一部分在英国牛津举行。
2018-10-20 cs.LO cs.PL cs.SE
A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements
验证复杂的安全关键系统是一项重大挑战。手动测试和模拟经常使用，但只能探索系统可达状态的子集。形式化方法是一种基于知识的软件规格说明和开发技术，它可以提供系统状态空间上的属性证明和穷举检查。在本文中，我们提出了一个正式的需求驱动的方法，适用于我们的工业合作伙伴提供的飞机发动机控制器的模型。我们的方法开始正式化的控制器的自然语言的要求，使用（预先存在的）正式的需求获取工具（FRET），迭代，与我们的行业合作伙伴协商。一旦形式化，FRET可以自动转换的要求，使他们的验证旁边的Simulink模型的飞机发动机控制器;的要求也可以指导形式化验证使用其他方法。在我们的方法中，这两个并行流寻求结合正式的需求引出，经典的验证方法和运行时验证的结果，以支持在Simulink中建模的航空航天系统的验证，从需求阶段到执行。我们的方法利用正式方法的力量，补充现有的验证技术，并支持整个验证过程中的需求的可追溯性。这种方法通过确保预先正式化要求并在开发过程中可用，简化了开发可验证飞机发动机控制器的过程。在本文中，我们给出了一个概述（FRET），描述我们的方法和工作的形式化和验证的要求，并概述了未来的工作，使用我们的方法。
2021-10-18 cs.SE
Developing the UML as a Formal Modelling Notation
统一建模语言（UML）正迅速成为面向对象系统建模的事实标准。考虑到这个角色，UML必须有一个定义良好的、充分开发的语义.这样的语义是必需的，以确保UML概念被精确地陈述和定义。在本文中，我们描述和激励的方法来形式化UML中，正式规格说明技术被用来深入了解UML符号和图表的语义。我们目前的工作进行了精确的UML（PUML）组上的一个精确的语义模型的UML类图的发展。语义模型被用作一组语法转换规则的基础，这些规则使得可以对UML类图进行正式的推导。它还显示了如何使用这些规则来验证一个类图是否是另一个类图的有效细化（设计）。由于这些规则是在语法层面上提出的，因此可以认为UML可以成功地用作正式的建模工具，而不需要在正式规范技术中常见的符号复杂性。
2014-09-24 cs.SE
Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD)
本卷包含IMPEX 2017的联合会议记录，第一次关于在正式系统开发中处理隐式和显式知识的研讨会和FM&MDD，第二次关于开发可信赖系统的形式和模型驱动技术的研讨会（FM&MDD）于2017年11月16日在中国西安举行，作为ICFEM 2017的一部分，第19届国际正式工程方法会议。IMPEX强调的机制，减少异质性的模型所引起的缺乏明确的语义表达的形式化技术，用于指定这些模型。更确切地说，会议的目标是突出在处理正式系统开发中的隐式和显式语义方面的进展。FM&MDD的目标是促进对开发和应用用于设计可信系统的正式和模型驱动技术领域的理解，讨论该领域中出现的问题，改善不同研究社区之间以及学术界和工业界之间的对话，讨论该领域未来研究的路线图，并建立一个论坛，讨论和传播新的想法和研究成果，该地区
2018-05-12 cs.LO cs.SE
EPspectra: A Formal Toolkit for Developing DSP Software Applications
软件方法开发数字信号处理（DSP）应用程序带来了一些很大的特点，如灵活性，资源的可重用性和易于升级的应用程序。然而，由于软件的复杂性不断增加，它需要漫长而繁琐的测试和验证阶段。这意味着需要一个软件编程环境，能够将DSP模块放在一起，并提供调试、验证和验证代码的设施。这项工作的目的是为开发DSP软件应用程序提供仿真和验证等设施。这使我们开发了一个扩展工具包，Epspectra，建立在Pspectra，第一个工具包可用于设计基本的软件无线电应用程序的标准PC工作站。在本文中，我们首先提出Epspectra，一个基于Esterel的扩展Pspectra，使便携式DSP应用程序的设计和实现更容易。它允许大大减少测试和验证时间，同时需要相对较少的形式化验证方法的专业知识。其次，我们演示了Epspectra的使用，以GSM基站的无线电接口部分为例。我们还提出了验证程序的三个安全属性具有复杂的控制路径。这些都必须遵守严格的时间表规则。此外，Epspectra实现了目标应用程序的验证，因为可执行代码生成和形式化验证使用了相同的模型。
2005-02-04 cs.LO cs.SE
Developing a Prototype of a Mechanical Ventilator Controller from Requirements to Code with ASMETA
严格的开发流程旨在有效地开发关键系统，特别是如果故障可能对人类和环境造成灾难性后果。这些过程通常依赖于形式化方法，由于其数学基础，可以保证模型的精确性和属性保证。但实际上很少采用。在本文中，我们报告了我们使用抽象状态机形式化方法和ASMETA框架开发MVM（机械呼吸机米兰）控制软件原型的经验，MVM是一种在COVID-19大流行期间设计、成功认证和部署的机械肺呼吸机。由于时间限制和缺乏技能，没有对MVM项目采用正式方法。然而，我们在这里要评估的可行性发展（部分）呼吸机使用正式的方法为基础的方法。我们的开发过程从一个高层次的正式规格说明的系统来描述MVM的主要操作模式。然后，通过一系列细化的模型，所有其他的需求都被捕获，直到一个级别，在该级别中，MVM控制器的原型的C++实现从模型自动生成，并进行测试。沿着该过程，在每个细化级别，执行不同的模型确认和验证活动，并且每个细化的模型被证明是前一级别的正确细化。通过MVM的案例研究，我们评估我们的形式化方法的有效性和可用性。
2021-11-16 cs.FL cs.SE
Developing Bug-Free Machine Learning Systems With Formal Mathematics
Stanford University（斯坦福大学）
在机器学习系统中，噪声数据、非凸目标、模型错误指定和数值不稳定都可能导致不期望的行为。因此，检测实际实现错误可能极其困难。我们展示了一种方法，开发人员使用一个交互式的证明助手来实现他们的系统，并说明一个正式的定理，定义它意味着他们的系统是正确的。在证明助手中交互地证明这个定理的过程暴露了所有的实现错误，因为程序中的任何错误都会导致证明失败。作为一个案例研究，我们实现了一个新的系统，Certigrad，优化随机计算图，我们生成一个正式的（即机器可检查）证明系统采样的梯度是真实的数学梯度的无偏估计。我们使用Certigrad训练了一个变分自编码器，发现其性能与在TensorFlow中训练相同模型相当。
2017-06-26 cs.AI cs.SE
Developing controlled natural language for formal specification patterns using AI assistants
Institute of Automation and Electrometry（自动化与电测研究所）
本文提出利用AI助手开发受控自然语言的方法，通过三个阶段构建基于形式规范模式的自然语言需求，用于事件驱动的时间要求分析。
2025-12-30 cs.AI cs.FL cs.SE
Integrating Inter-Object Scenarios with Intra-object Statecharts for Developing Reactive Systems
在所有的软件开发项目中，工程师都面临着将需求层转换为设计层，然后转换为实现代码层，然后验证结果的正确性的挑战。有许多方法、语言和工具可以促进这一过程，包括在需求、设计和实现层之间进行多次来回的“改进之旅”，方法是把重点放在使所涉及的工件正规化和使整个过程中的各种任务自动化。在本文中，我们介绍了一种新颖的和独特的开发环境，它集成了基于XML的编程（SBP）通过LSC语言和面向对象的，可视化的Statecharts形式主义，反应式系统的发展。LSC的目标是直接从需求规范创建模型和系统，Statecharts主要用于指定最终组件的行为。我们的集成使语义丰富的联合执行，共享和接口的对象和事件，并可用于创建，然后逐步增强可测试的模型，从早期的需求启发，通过详细的设计。在某些情况下，它可以用于生成最终的系统代码。我们描述的集成和语义的技术细节，并讨论其意义，为未来的开发方法。
2020-10-07 cs.SE
Assurance Case Development for Evolving Software Product Lines: A Formal Approach
University of Toronto（多伦多大学）
本文提出一种形式化方法，用于演化软件产品线的提升保证案例开发与回归分析，支持感知变异性的AC语言、基于模板的开发提升及SPL演化影响分析，并提供了基于模型的工具与医疗设备应用实例。
2025-11-04 cs.SE
Experiences in Developing Time-Critical Systems - The Case Study "Production Cell"
从1994年的一个项目内竞争中使用的玩具生产单元的非正式需求描述开始，我们给出了一个正式的规范，尽可能接近的要求。我们使用Manna和Waldinger（1980）的演绎程序合成方法来获得一个经过验证的TTL类电路来控制细胞。正式规范还涵盖了机械方面，因此不仅允许对软件问题进行推理，还可以对机械工程问题进行推理。除了一个方法局限于一阶谓词逻辑与明确的，连续的时间，尝试采用特定于应用程序的用户定义的逻辑运算符，以得到一个更简洁的规范以及证明。
2014-04-04 cs.LO cs.SE
Validating Formal Specifications with LLM-generated Test Cases
INESC TEC；Universidade do Minho（米尼奥大学）
本文利用GPT-5等大语言模型自动生成测试用例，用于验证形式规范的正确性，有效检测人类编写错误的规范。
2026-02-18 cs.SE
Extending Rely-Guarantee thinking to handle Real-Time Scheduling
本文将依赖-保证方法扩展到实时调度领域，通过系统质疑调度器假设来识别和规定其容错特性。
2023-11-30 cs.SE
Encapsulating Formal Methods within Domain Specific Languages: A Solution for Verifying Railway Scheme Plans
形式化方法的发展和应用是计算机科学领域一个长期的研究课题。仍然存在的一个特殊挑战是将正式方法纳入工业实践。本文介绍了一种方法，用于开发领域特定的语言建模和验证，以帮助在工业中的正式方法的吸收。它说明了这种方法在铁路领域的成功应用。所提出的方法解决问题，围绕忠实的建模，可扩展性的验证和访问的建模和验证过程中的从业者在域。
2014-03-23 cs.LO cs.SE
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems
本卷包含MARS 2020的会议记录，这是作为ETAPS 2020的一部分举行的第四次真实系统形式分析模型研讨会，欧洲软件理论与实践联合会议。MARS研讨会汇集了来自不同社区的研究人员，他们正在复杂模型出现的领域开发真实系统的正式模型，例如网络，网络物理系统，硬件/软件协同设计，生物学等。（1）大型案例研究是必不可少的，以表明规范形式主义和建模技术适用于真实系统，而许多研究论文只考虑玩具例子或微小的案例研究。(2)开发一个真实系统的精确模型需要大量的时间，通常是数月或数年。然而，在大多数科学论文中，由于缺乏空间，需要跳过模型的重要细节，并为形式化验证方法和结果留出空间。MARS研讨会纠正了这些问题，强调建模而不是验证，以便保留从正式建模中吸取的教训，这些教训通常不在其他地方讨论。
2020-04-26 cs.LO cs.PL cs.SE
Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems
本卷包含MARS 2022的会议记录，这是第五次关于真实系统形式分析模型的研讨会，作为ETAPS 2022的一部分举行，欧洲软件理论与实践联合会议。MARS研讨会汇集了来自不同社区的研究人员，他们正在开发复杂模型出现的领域中的真实系统的正式模型，例如网络，网络物理系统，硬件/软件协同设计，生物学等。* 大型案例研究是必不可少的，以表明规范形式主义和建模技术适用于实际系统，而许多研究论文只考虑玩具例子或微小的案例研究。* 开发一个真实系统的精确模型需要大量的时间，通常是数月或数年。然而，在大多数科学论文中，由于缺乏空间，需要跳过模型的重要细节，并为形式化验证方法和结果留出空间。MARS研讨会旨在纠正这些问题，强调建模而不是验证，以便保留从正式建模中吸取的教训，这些教训通常不在其他地方讨论。
2022-03-17 cs.LO cs.PL cs.SE
Proceedings of the 7th Workshop on Models for Formal Analysis of Real Systems
本文集旨在通过大规模案例研究展示形式化规范和建模技术在现实系统中的应用，强调建模而非验证，保留形式化建模中的经验教训，为未来分析和比较奠定基础。
2026-04-03 cs.LO cs.SE
Meta-Modeling Semantics of UML
统一建模语言正在成为面向对象系统建模的事实标准。然而，作为标准定义的一部分的语义文档主要提供了对语言的语法和格式良好性规则的描述。该语言的含义主要用英语描述，过于非正式和非结构化，无法为开发正式分析和开发技术提供基础。本文概述了一种形式化策略，使精确的UML的核心语义。这是通过加强现有UML元模型的指称语义来实现的。为了说明这种方法，泛化/特化的语义是精确的。
2014-09-24 cs.SE
Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems
MARS 2024研讨会论文集聚焦真实系统形式化建模，旨在解决大规模案例研究匮乏与模型细节易被省略的问题，强调建模重于验证以分享建模经验。
2024-03-26 cs.LO cs.PL cs.SE
Mechanised Assurance Cases with Integrated Formal Methods in Isabelle
通常需要保证案例作为验证关键系统的一种手段。在保证中使用形式化方法可以提高自动化程度，并克服模糊性，错误推理和证据支持不足的问题。然而，保证案例很少能够完全形式化，因为正式方法的使用取决于非正式流程验证的模型。因此，我们需要保证技术，支持正式和非正式的工件，明确的推理链接和假设，可以通过评估检查。我们的贡献是一个机械的框架，用于开发基于伊莎贝尔系统的集成形式化方法的保证案例。我们展示了嵌入的结构化保证案例元模型（SACM）使用伊莎贝尔/自由度，并展示了如何将其链接到源于我们的验证框架，伊莎贝尔/UTP的正式分析技术。我们通过机械化Tokeneer安全案例的一个片段来验证我们的方法，并通过形式化验证提供证据。
2019-05-15 cs.LO cs.SE
Proceedings First Latin American Workshop on Formal Methods
软件开发的形式化方法是旨在通过使用符号、分析过程等来开发高质量软件的技术，基于数学基础。虽然传统上他们的目标是提高软件的正确性，形式化技术已被应用到软件质量的其他方面。此外，虽然最初的正式方法采用复杂的“重量级”的分析机制（通常是手动或半自动），已经取得了进展，拥抱“轻量级”，很多时候完全自动化，分析技术，扩大了正式方法在各种软件工程上下文中的采用。拉丁美洲正式方法研讨会汇集了正式方法以及自动分析等相关领域的研究人员。特别是，讲习班为在这些领域工作的拉丁美洲研究人员提供了一个场所，以促进他们的互动与合作。该讲习班于8月举行，是CONCUR 2013年的附属活动。它发生在布宜诺斯艾利斯，阿根廷的首都和最大的城市，也是南美洲最有趣的文化场所之一。
2014-01-02 cs.LO cs.SE
Experience in using a typed functional language for the development of a security application
在本文中，我们提出了我们的经验，在开发一个安全的应用程序使用类型的函数语言。我们描述了它的语义和编译器的正式接地允许一个值得信赖的发展，并促进了履行的安全规范。
2014-04-26 cs.CR cs.SE
Developing Autonomic Properties for Distributed Pattern-Recognition Systems with ASSL: A Distributed MARF Case Study
Lero - the Irish Software Engineering Research Centre（莱罗爱尔兰软件工程研究中心）；University of Limerick（利默里克大学）；Concordia University（康考迪亚大学）
在本文中，我们讨论了我们的研究发展的特殊属性，引入自主行为的模式识别系统。在我们的方法中，我们使用ASSL（自治系统规约语言）正式开发DMARF（分布式模块化音频识别框架）等属性。这些属性通过管理框架模式识别管道的四个阶段的自治中间件增强了DMARF。DMARF是一种生物启发系统，采用模式识别，信号处理和自然语言处理，帮助我们处理各种科学应用所需的音频，文本或图像数据，例如，生物识别应用在这种情况下，自主DMARF（ADMARF）的概念可以被自主和机器人系统采用，这些系统理论上需要很少或没有人为干预，除了数据汇集用于模式分析和观察结果。在这篇文章中，我们解释了DMARF的自治属性的ASSL规范模型。
2011-12-16 cs.CV cs.DC cs.SE
The missing link: Developing a safety case for perception components in automated driving
University of Waterloo（滑铁卢大学）；DENSO CORPORATION（电装公司）
安全保证是自动驾驶（AD）系统开发和社会接受的核心问题。感知是AD的一个关键方面，它在很大程度上依赖于机器学习（ML）。尽管已知的挑战与ML为基础的组件的安全保证，建议最近出现的单元级安全的情况下，解决这些组件。不幸的是，AD安全案例表达了系统级的安全要求，这些努力缺少将系统级的安全要求与单元级的组件性能要求相结合所需的关键链接参数。在本文中，我们提出了集成安全的情况下，感知（ISCaP），一个通用的模板，这样一个链接的安全参数专门为感知组件。该模板采用演绎和正式的方法来定义级别之间的强可追溯性。我们展示了ISCaP的适用性与详细的案例研究，并讨论了其作为一种工具，以支持增量开发的感知组件。
2022-09-06 cs.AI cs.LG cs.RO
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
软件的演绎验证尚未进入行业，因为复杂性和可扩展性问题需要高度专业的专家。然而，长期的观点是开发验证工具，帮助工业软件开发人员更快，更容易地找到软件系统中的错误或瓶颈。KeY项目构成了一个用于指定和验证软件系统的框架，旨在使形式化验证工具适用于主流软件开发。为了帮助KeY的开发人员、用户和演绎验证社区，我们从用户的角度总结了使用KeY 2.6.1指定和验证真实世界Java代码的经验。为此，我们集中讨论OpenJDK 6的Collections-API的部分内容，其中存在非正式规范。当我们描述我们如何桥接非正式和正式规范时，我们也展示了我们遇到的伴随的挑战。我们的经验是，（a）原则上，演绎验证类API代码库是可行的，但需要很高的专业知识，（b）为现有的代码库开发正式的规范仍然是出了名的困难，（c）在Java中的某些语言结构的规格是具有挑战性的工具建设者。我们在指定OpenJDK 6的部分方面的初步努力构成了未来研究案例研究的垫脚石。
2018-11-27 cs.LO cs.PL cs.SE
