An Institutional Framework for Heterogeneous Formal Development in UML
我们提出了一个框架，正式的软件开发与UML。与以前的方法，装备UML与正式的语义，我们遵循一个机构为基础的异构方法。这可以直接表达不同UML图类型的合适的形式语义，而不需要将所有内容映射到一个特定的形式主义（假设它是一阶逻辑或图形语法）。我们展示了如何不同方面的正式开发过程可以连贯地形式化，从设计和霍尔风格的条件代码的实现本身的要求。该框架可以用于水平地验证不同UML图的一致性（例如，各种要求之间的一致性）以及垂直地（例如，设计或实施的正确性的要求）。
2014-03-30 cs.LO cs.SE
Meta-Modeling Semantics of UML
统一建模语言正在成为面向对象系统建模的事实标准。然而，作为标准定义的一部分的语义文档主要提供了对语言的语法和格式良好性规则的描述。该语言的含义主要用英语描述，过于非正式和非结构化，无法为开发正式分析和开发技术提供基础。本文概述了一种形式化策略，使精确的UML的核心语义。这是通过加强现有UML元模型的指称语义来实现的。为了说明这种方法，泛化/特化的语义是精确的。
2014-09-24 cs.SE
A Formal Transformation Method for Automated Fault Tree Generation from a UML Activity Model
故障分析和故障解决应该是任何端到端系统开发过程的一部分。本文关注的是开发一种形式化的转换方法，映射在UML活动建模的控制流语义等价的故障树。转换方法的特点是使用命题演算和概率论。故障传播链的引入，以促进转换方法。一个总体元模型之间的转换，并应用到一个理解的交通管理系统的系统问题，以证明该方法。这样，系统行为模型的关系结构就反映在故障树的结构中。本文最后讨论了转换方法的局限性，并提出了将其扩展到对象流、状态机和功能分配的方法。
2018-04-30 cs.SE
Proceedings 9th edition of Working Formal Methods Symposium
本卷收录了2025年9月在罗马尼亚Alexandru Ioan Cuza大学举办的第9届工作形式化方法研讨会的论文集。
2025-09-15 cs.LO cs.PL cs.SE
QuantUM: Quantitative Safety Analysis of UML Models
在开发安全关键系统时，必须对不同的设计方案进行评估。特别是，系统的架构设计的早期安全评估是可取的。尽管有过多的正式的定量分析方法，但软件和系统架构师仍然很难将这些技术集成到他们的日常工作中。这主要是由于缺乏可以直接应用于架构级模型的方法，例如UML图。此外，所使用的描述方法不需要对形式方法有深刻的了解。我们的方法弥补了这一差距，并提高了定量安全分析方法到开发过程中的集成。分析的所有输入都是在UML模型的层次上指定的。然后，该模型被自动地转换成分析模型，并且分析的结果因此在UML模型的级别上被表示。因此，在分析过程中使用的分析模型和形式化方法对用户是隐藏的。我们说明了我们的方法使用工业实力的案例研究的有用性。
2011-07-06 cs.SE
Formal Verification of Ecosystem Restoration Requirements using UML and Alloy
本文提出一种基于UML元模型和Alloy形式化的模型驱动方法，通过Alloy Analyzer验证生态系统的安全性与活性属性，确保生态系统规格说明可靠并满足恢复目标，并以CRESTO实例进行说明。
2024-05-31 cs.SE
Proceedings Tenth Symposium on Working Formal Methods
本文介绍了第十届工作形式方法研讨会（FROM 2026）的举办信息，包括时间地点、组织方、同期会议及收录的14篇论文。
2026-09-28 cs.LO cs.SC cs.SE
A Note on Semantics (with an Emphasis on UML)
本注释阐明了句法和语义的概念及其关系。今天，许多混乱产生于“语义学”一词被用于不同的含义。我们讨论了一个通用的方法，在定义语义，是可行的文本和图形符号，并讨论这种方法使用一个例子形式化。层次Mealy自动机的形式化和语义定义使用输入/输出行为允许我们定义一个规范，以及实现语义。最后，分类不同的方法，适合在这个框架。这种分类也可以在定义新语言的语义时作为指导方针。
2014-09-24 cs.SE
Proceedings of the Sixth Working Formal Methods Symposium
我们很高兴地介绍在“Al. I.”举行的第六届工作形式方法研讨会（从2022年开始）的论文。2022年9月19日至20日，罗马尼亚雅西大学。从旨在汇集研究人员和从业者谁工作的正式方法，通过贡献新的理论成果，方法，技术和框架，和/或使正式方法的工作，通过创建或使用软件工具，应用理论的贡献。该计划委员会选择了五个贡献和四个邀请演讲，其中一个与第28届逻辑，语言，信息和计算研讨会（WoLLIC 2022）共享。两个贡献处理匹配逻辑，一个表达逻辑框架，程序设计语言和其他逻辑的正式定义可以嵌入。其他贡献涉及分布式系统，多代理系统和教学正式的方法。邀请的会谈目前的工作与这些主题大致一致。
2022-09-19 cs.LO cs.PL cs.SE
Defining UML Family Members Using Prefaces
统一建模语言是可扩展的，因此可以被视为一个语言家族。无论是隐式的还是显式的，任何特定的UML模型都应该伴随着用于该模型的特定UML家族成员的定义。定义应包括句法和语义问题。本文提出了一种机制，将模型与这样的定义。任何特定的定义都会构成我们所说的序言。这个名字的意图是表明，一个特定的UML家族成员的定义在概念上必须在使用该家族成员构建的任何模型之前。序言应该很大，并且应该使用包来组织。这将允许不同序言之间进行大量共享。本文提出序言应该具有一种公理化的语义风格，通过不一定完全形式化，并基于一般情况和特殊情况的思想，提供了一种通用的语义方法，可以减少大型序言中的不一致问题
2014-09-24 cs.SE
Towards a System Model for UML. The Structural Data Model
在本文档中，我们将介绍一个系统模型作为UML 2.0语义模型的基础。系统模型是UML语义定义的核心和基础。为此，基本系统是针对UML的。本文件的结构如下：在第1节的其余部分，我们将讨论一般方法并强调主要决定。本节对于理解本文档的其余部分非常重要。第2节包含系统模型的结构部分的实际定义。如第1节所述，它是内置的层。为了简洁起见，我们将更深入的讨论推迟到第4节的附录中。本文档是Kingston皇后大学与Braunschweig和München工业大学合作的UML 2.0形式化项目的一部分。这个版本1.0是一个长期努力的结果，定义面向对象的结构，行为和交互，可能是分布式系统抽象到足以具有一般价值，但也足够详细的UML的语义基础。我们还要感谢外部审稿人，特别是Gregor von Bochmann、Gregor Engels和Sébastien Gérard的帮助。
2014-09-22 cs.SE
Modular Description of a Comprehensive Semantics Model for the UML (Version 2.0)
在本文档中，我们将介绍一个系统模型作为统一建模语言（UML）的语义域[OMG 07a，OMG 07b]。系统模型被认为是UML语义定义的一个可能的核心和基础。为此，本文中的定义是针对UML的，这意味着UML的中心概念已经被形式化为系统模型的理论。本文件的结构如下：在第1章的其余部分，我们讨论了一般方法，并强调了主要的决定。本章对于理解本文档的其余部分非常重要。第二章是系统模型结构部分的定义。第3章和第4章包含控制和通信相关的定义，这些定义构成了第5章描述系统状态的基础。在第6章（基于事件）和第7章（定时）中，我们介绍了状态转换系统的两种变体来定义对象行为。第8章结束了这篇文章。本文档是系统模型的第二个版本，该模型是定义面向对象的结构、行为和交互的主要努力的结果，可能是分布式系统，其抽象程度足以具有一般价值，但也足够详细，可作为UML的语义基础。系统模型的第一个版本可参见[BCR 06、BCR 07a、BCR 07b]。
2014-09-22 cs.SE
Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking
业务分析师和领域专家经常使用与技术和平台无关的高级模型来勾画软件系统的行为。开发人员将用技术细节来完善和丰富这些高级模型。因此，随着时间的推移，细化的模型可能会偏离原始模型，特别是当两种模型独立演化时。在这种情况下，我们专注于行为模型;也就是说，我们的目标是确保细化的低级别行为模型符合相应的高级别行为模型。基于现有的形式化验证技术，我们提出包含检查作为一种手段，以评估系统的行为所描述的低级别模型是否满足已指定的高级别同行。主要障碍之一是如何减轻创建行为模型的正式规范以及一致性约束的负担，这是一项手动完成的繁琐且容易出错的任务。本文提出的方法旨在通过将行为模型视为验证输入，并将行为模型自动映射到可直接由模型检查器使用的形式属性和描述上，来缓解上述挑战。我们讨论了我们的方法中的各种挑战，并展示了我们的方法在说明性场景中的适用性。
2014-04-03 cs.LO cs.SE
User Assistance Characteristics of the USE Model Checking Tool
统一建模语言（UML）是一种广泛使用的通用建模语言。与对象约束语言（OCL）一起，可以通过用UML和附加的OCL约束定义结构和行为来描述正式模型。在正式模型的开发过程中，重要的是要确保这些模型是（a）正确的，即一致和完整的，以及（b）可测试的，在这个意义上，开发人员能够交互地检查模型属性。USE工具（基于UML的规范环境）允许研究这两个特性。我们演示了该工具如何支持建模者通过使用多种图形方法来分析、验证和确认UML和OCL模型，这些方法可以帮助建模者解释和可视化正式的模型描述。特别是，我们讨论了如何将所谓的USE模型验证器插件集成到USE环境中，以允许非领域专家使用它并构建对象模型，以帮助验证模型一致性等属性。
2017-01-30 cs.HC cs.SE
Formal Modeling and Initial Analysis of the 4SECURail Case Study
我们提出的情况下开发的4 brackail项目和用于其正式建模和分析的方法的案例研究。从一个简单的SysML/UML行为模型的系统需求，三个正式的模型已经开发使用三种不同的框架，即UMC，ProB和CADP/LNT。本文展示了如何从三个不同的角度来表示和分析系统的不同方法，使我们能够利用由此产生的多样性。
2022-03-18 cs.SE
UML Sequence Diagram: An Alternative Model
序列图的普遍接受可以归因于它们相对直观的性质和描述部分行为的能力（与状态图等图相反）。然而，研究表明，超过80%的毕业生无法创建软件设计，甚至无法创建部分设计，许多学生不知道序列图如何受到其他模型的约束。许多学生在识别有效的交互对象和用适当的参数构建消息方面表现出困难。此外，根据权威人士的说法，尽管已经为序列图提出了许多不同的语义（例如，转换到状态机），不存在所需序列图行为的合适的语义基础细化，因为直接样式语义不能精确地捕获所需序列图行为;转换到其他形式主义忽略了序列图的基本特征，例如保护条件和临界区域。本文提出了一种替代序列图，一个广义的模型，提供了进一步的理解序列图同化到一个新的建模语言称为思维机（TM）。序列图通过去除表面的仅垂直维度的扩展限制而水平扩展，以保留事件的逻辑年表。TM算法在动作方面是非线性传播的。事件及其年表是在第二个描述平面上构建的，该平面叠加在最初的静态描述上。其结果是一个更精确的表示，将简化建模过程。这是通过重建序列图的情况下，从文献中证明。
2021-05-31 cs.SE
Semantic based model of Conceptual Work Products for formal verification of complex interactive systems
许多临床工作流程依赖于交互式计算机系统，用于高技术性、概念性的工作产品，例如诊断、治疗计划、护理协调和病例管理。我们描述了一个自动逻辑推理机来验证这些高度技术性的，但抽象的，工作产品是必不可少的照顾客观规范。概念性的工作产品规格作为一个基本的输出要求，必须清楚地陈述，正确和可解决的。这种规范具有战略重要性，因为反过来，它们使系统模型检验能够验证用户过程所采用的机器功能实际上能够实现这些抽象产品。我们选择多发性硬化症（MS）门诊患者的病例管理作为我们的用例，因为它具有挑战性的复杂性。作为第一步，我们说明了如何从UML的图形类和状态图可以开发和批评与主题专家作为规范的概念工作产品的情况下管理。一个关键特性是规范必须是声明性的，因此独立于任何过程或技术。我们的工作领域本体与语义网的工具，需要翻译UML类和状态图的自动推理的可解性验证。然后，可解模型将准备好用于随后对人类程序和机器功能的系统进行模型检验。我们使用了表达规则语言SPARQL推理符号（SPIN）来开发UML类图、状态机及其交互的形式化表示。利用SPIN证明了静态概念和动态概念相互作用的一致性。我们讨论了如何将新的SPIN规则引擎合并到对象管理组（OMG）本体定义元模型（ODM）中
2020-08-04 cs.SE stat.ML
Towards Conceptual Modeling Semantics: Eventizing Tarski's Truth Schema
软件工程中的建模语言（例如，UML）是从软件系统建模发展而来的，在软件系统建模中，指称和操作类型的语义是研究和实践的传统主题。根据一些作者，虽然大部分静态语义（例如，UML）似乎已经达成了共识，活动、交互和状态机的动态语义构成了一个重大挑战。语义学的核心是句子与（实际）世界之间的关系。仔细检查建模语言领域中与语义相关的问题以避免可能影响实际适用性的问题是很重要的。在这方面的一个努力是OMG发布的2020年基础UML（fUML）规范草案，其基本语义指定了与传统程序设计语言中的程序相同意义上的可执行。此外，学术界的努力已经寻求开发一种替代方法来使用形式语义（例如，使用罗素的类型理论和塔斯基的声明语义学）。本文旨在开发语义学的类似探索性冒险，只是为了一种更温和的图形建模语言，称为事物机器模型。该模型促进了对仔细审查的建模语言的深入理解，并导致相当富有成效的问题。构建thinging机器模型似乎有助于这一方向的进展，本文的初步结果表明该方法的可行性。
2020-11-03 cs.SE
Towards a Semantics of Activity Diagrams with Semantic Variation Points
UML活动图已经成为一种建立在各种抽象层次上的模型控制和数据流的符号，从算法的细粒度描述到业务应用程序中的高级工作流模型。一个形式化的语义必须捕捉在真实系统中活动图的解释的灵活性，这使得它不适合定义一个固定的形式化语义。在本文中，我们定义了一个语义的语义变化点，允许一个可定制的，特定于应用程序的解释活动图。我们研究活动图语义的具体变体，这也可能需要语法的变体来反映当前的预期用途。
2014-09-08 cs.SE
Towards a Step Semantics for Story-Driven Modelling
图转换（GraphTransformation，GraTra）提供了一种正式的、声明性的方法来指定模型转换。在实践中，GraTra规则应用程序通常通过附加语言编程，利用该附加语言可以适当地控制规则应用程序的顺序。故事驱动建模（SDM）是编程的GraTra的一种方言，最初作为Fujaba CASE工具套件的一部分开发。SDM使用一种直观的、受UML启发的可视化语法，提供了常见的命令式控制流结构，如序列、条件和循环，这些结构相当简单，但它们与单个GraTra规则的交互却很重要。在本文中，我们提出了我们正在进行的工作，提供一个正式的步骤语义的SDM，它侧重于执行的SDM规范的第一个结果。
2016-12-06 cs.SE
Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications
本卷包含第二届法国新加坡正式方法和应用研讨会（FSFMA'14）的会议记录。该研讨会于2014年5月13日在新加坡举行，作为第19届形式方法国际研讨会（FM'14）的卫星活动。FSFMA旨在分享研究兴趣，并在正式方法及其应用领域开展合作。研讨会的科学主题涵盖（但不限于）形式规范、模型检验、验证、程序分析/转换、软件工程以及计算机科学主要领域（包括航空航天）的应用等领域。该研讨会汇集了来自法国，新加坡和其他国家的研究人员和行业研发专家，交流他们的知识，讨论他们的研究成果，并探索潜在的合作。本卷包含八个贡献：四个邀请会谈和四个定期文件。
2014-07-08 cs.LO cs.SE
Development of formal models, algorithms, procedures, engineering and functioning of the software system "Instrumental complex for ontological engineering purpose"
给出了一个软件系统“Instrumental Complex for Ontological Engineering Purpose”的广义模型表示。代表了完整的软件系统开发过程。建立了“本体工程仪器综合体”软件系统的形式化模型，包括数学表达式、UML图等，并描述了“本体工程仪器综合体”软件系统在客户机-服务器环境下的三层体系结构。
2022-01-01 cs.AI cs.SE
Formal Methods in Railways: a Systematic Mapping Study
形式化方法是基于知识的技术，用于软件密集型系统的严格开发。铁路信号领域是一个传统上应用形式化方法的领域，有几个成功的案例。本文报告了一个映射研究，调查景观的研究应用正式的方法来发展铁路系统。我们的主要结果如下：（i）我们确定了1989年至2020年期间发表的328项与我们的研究范围相关的主要研究，其中44%在过去5年内发表，24%涉及行业;（ii）大部分研究是透过例子（41%）及经验报告（38%）进行评估，而全面的个案研究则十分有限（百分之一点五）;（iii）模型检查是最常用的技术（47%），其次是仿真（27%）和定理证明（19.5%）;（四）主要语言是统一建模语言（18%）和B语言（15%），常用工具是ProB语言（9%）、NuSMV语言（8%）和UPPAAL语言（7%）;然而，使用的语言和工具多种多样;（v）大部分系统是联锁产品（40%），其次是高级控制逻辑模型（27%）;（vi）大部分研究集中在架构（66%）和详细设计（45%）开发阶段。基于这些发现，我们强调了目前的研究差距和预期的行动。特别是，需要专注于更实证的研究方法，如案例研究和控制实验，并降低抽象程度，通过应用正式的方法和工具，更接近软件开发的开发阶段。我们的研究有助于以经验为基础的角度对未来的研究和实践中正式的方法应用于铁路。
2022-02-25 cs.SE
