A Note on Semantics (with an Emphasis on UML)
本注释阐明了句法和语义的概念及其关系。今天，许多混乱产生于“语义学”一词被用于不同的含义。我们讨论了一个通用的方法，在定义语义，是可行的文本和图形符号，并讨论这种方法使用一个例子形式化。层次Mealy自动机的形式化和语义定义使用输入/输出行为允许我们定义一个规范，以及实现语义。最后，分类不同的方法，适合在这个框架。这种分类也可以在定义新语言的语义时作为指导方针。
2014-09-24 cs.SE
Systematic teaching of UML and behavioral diagrams
本文研究如何在不依赖模型解析器的情况下系统化教学和评估手绘 UML 图，重点介绍活动图及图像标注、热点查找等多样化练习题型。
2024-10-23 cs.SE
Managing and Analysing Software Product Line Requirements
软件产品线特征建模对软件产品线的成功开发起着至关重要的作用。特征图是一种广泛使用的标记模型SPL的变种。然而，缺乏精确定义的正式符号表示和验证这样的模型。本文提出了一种方法，我们采用模型SPL变量使用UML，随后验证他们使用一阶逻辑。UML提供了系统的总体建模视图。一阶逻辑提供了一个精确和严格的解释的功能图。我们通过使用命题连接词来建模变体及其依赖关系，并构建逻辑表达式。这些表达式然后由Alloy验证工具进行验证。利用计算机辅助调度（CAD）系统说明了分析和验证过程。
2013-10-01 cs.SE
Transformation of UML Behavioral Diagrams to Support Software Model Checking
统一建模语言（UML）目前被接受为建模（面向对象）软件的标准，它在航空航天工业中的使用正在增加。根据UML开发的复杂软件的验证和确认并不是微不足道的，因为软件本身的复杂性，以及可以用于对软件的行为和结构建模的几种不同的UML模型/图。本文提出了一种方法来转换多达三个不同的UML行为图（序列，行为状态机，活动）到一个单一的过渡系统，以支持模型检验的软件开发按照UML。在我们的方法中，属性是基于用例描述形式化的。转换是针对NuSMV模型检查器完成的，但我们看到了使用其他模型检查器的可能性，例如SPIN。我们的工作的主要贡献是一个非形式语言（UML）的形式语言（语言的NuSMV模型检查器）在实践中的正式方法在软件开发中更大的采用转换。
2014-04-03 cs.SE
Towards a Formalization of the Unified Modeling Language
统一建模语言UML是一种用于描述面向对象系统的可视化和文档化的语言。UML结合了OOA、OODOMT和OOSE的概念，旨在作为面向对象分析和设计领域的标准。由于UML缺乏形式化的数学基础，许多UML结构的语法和语义都没有精确定义。本文概述了UML的形式化基础的建议它是基于一个数学系统模型
2014-09-25 cs.SE
On the Design of Agent-Based Systems using UML and Extensions
统一软件开发过程（USDP）和统一建模语言（UML）已被普遍接受为开发面向对象系统的标准方法和建模语言。虽然基于Agent的系统引入了新的问题，我们认为，USDP和UML可以用于在一个扩展的方式建模基于Agent的系统。本文提出了一种方法，用于设计基于代理的系统和特定的模型表示在一个基于UML的符号对应的软件开发过程的每个阶段。UML是使用提供的机制扩展的：原型。因此，这种方法可以用任何支持UML的CASE工具来管理。一个案例研究，一个特定的基于代理的学生评价系统（SAS）的发展。
2006-05-08 cs.AI cs.MA cs.SE
Use of UML and Model Transformations for Workflow Process Definitions
目前，许多不同的建模语言用于BPM系统中的工作流定义。本文作者分析了两种最流行的图形化语言，具有广泛的实际应用的可能性最高的UML活动图（AD）和业务流程建模符号（BPMN）。在实践中必要的工作流程方面进行了简要讨论，并在此基础上提出了一个自然的AD配置文件，其中涵盖了所有这些。还选择了功能等效的BPMN子集。本文还分析了这两种语言在流程执行上下文中的语义（即映射到XML）。通过分析AD和BPMN元模型，作者得出结论，从AD到BPMN的精确转换即使对于所选子集也不是微不足道的，尽管这些语言被认为是相似的。作者展示了如何在MOLA转换语言中定义这种转换。
2006-07-11 cs.SE
A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP
在并发和分布式系统中，死锁和不确定性可能变得越来越难以检测。UML活动图是模拟顺序和并发行为的流程图。尽管UML社区广泛采用这种图，但是没有标准的方法来验证活动图中是否存在死锁和不确定性行为。非决定性在文献中通常被忽视，即使它可能被认为是一个非常相关的属性。本文提出了一个自动验证UML活动图中死锁和不确定性的框架。它为活动图引入了一种组合CSP语义，用于从UML模型自动生成CSP规范。这些规范是使用FDR细化检查器自动验证死锁和不确定性行为的输入。我们提出了一个插件的Astah建模环境，机械化的翻译过程中，并调用FDR在后台执行验证的属性。该工具保持了图与其CSP规范之间的可追溯性。它分析FDR结果以突出显示导致死锁或不确定行为的关系图路径。该框架为UML建模工具增加了验证功能，并保持形式化语义对用户透明。因此，用户在建模过程中不需要理解或操作形式符号。我们提出了一个案例研究的结果，适用于所提出的框架，在云计算领域的模型验证。我们讨论了未来的应用，由于我们的方法的潜力。
2019-10-30 cs.SE
Well-formedness and typing rules for UML Composite Structures
从2.0版开始，UML引入了层次复合结构，这是一种定义复杂软件架构的表达方式，但在标准中定义的语义非常松散。在本文中，我们提出了一套一致性规则，消除歧义的UML复合结构的意义。我们的主要目标是为OMEGA UML概要文件提供一个复合结构的操作模型，OMEGA UML概要文件是一个可执行的概要文件，专门用于实时系统的正式规范和验证，在我们过去参与的一个项目中开发。然而，这里陈述的规则和原则适用于基于相同概念的其他分层组件模型，例如SysML。本报告中描述的OCL形式化支持所提出的规则。这种形式化应用于不同的复杂模型的评估和验证所提出的原则。
2010-10-29 cs.SE
Using Alloy to model-check visual design notations
本文探讨了图形符号的抽象语法的验证过程。我们为发现方法使用的五个UML图定义了一个统一的规范，在本文档中，我们说明了如何在Alloy中表示图，并根据我们的规范进行检查，以了解这些图在发现符号下是否有效。
2008-02-15 cs.SC cs.SE
A Formal Semantic for UML 2.0 Activity Diagram based on Institution Theory
给UML活动图（UMLAD）一个正式的语义是一项艰巨的任务。这种困难的原因是这种半形式化的形式主义的模糊性和精确的形式语义的缺乏。各种各样的语义学存在于处理这种语言所涵盖的各个方面的文献中。我们可以给出指称语义、功能语义和组合语义的例子。为了应付最近的趋势，给了一个异构的语义UML图，我们的目标是定义一个代数表示的语义UML AD。在这项工作中，我们定义了一个正式的语义UML 2.0 AD的基础上机构理论。对于UML AD形式化，这是一种图形化的语言，没有精确的形式语义，我们使用机构理论来定义预期的语义。因此，UMLAD形式主义将被定义在它自己的自然语义中。
2016-06-07 cs.LO cs.SE
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
Unleashing the Power of Sound: Revisiting the Physics of Notations for Modelling with auditory symbols
本文借鉴Moody视觉符号学“物理学”理论，提出一套面向软件建模工具的声音符号设计原则，并基于UML构建声音目录，通过实证研究验证其有效性，为声音在建模中的进一步应用奠定基础。
2023-04-17 cs.SE
QuantUM: Quantitative Safety Analysis of UML Models
在开发安全关键系统时，必须对不同的设计方案进行评估。特别是，系统的架构设计的早期安全评估是可取的。尽管有过多的正式的定量分析方法，但软件和系统架构师仍然很难将这些技术集成到他们的日常工作中。这主要是由于缺乏可以直接应用于架构级模型的方法，例如UML图。此外，所使用的描述方法不需要对形式方法有深刻的了解。我们的方法弥补了这一差距，并提高了定量安全分析方法到开发过程中的集成。分析的所有输入都是在UML模型的层次上指定的。然后，该模型被自动地转换成分析模型，并且分析的结果因此在UML模型的级别上被表示。因此，在分析过程中使用的分析模型和形式化方法对用户是隐藏的。我们说明了我们的方法使用工业实力的案例研究的有用性。
2011-07-06 cs.SE
Model Multiplicity (UML) Versus Model Singularity in System Requirements and Design
概念模型可用于管理系统开发生存周期的设计和实现阶段的复杂性。这样的模型需要牢牢掌握系统所基于的抽象原则，以及对实体和过程表示的高级性质的理解。在这种情况下，模型可以具有不同的体系结构特征。本文讨论了模型多样性（例如，统一建模语言[UML]），模型奇异性（例如，对象处理方法[OPM]，思维机器[TM]），以及涉及多重性和奇异性的异构模型。模型多样性的基本思想是，不可能在一个表示中表示所有视图，因此使用了许多模型，每个模型表示不同的视图。模型奇异性方法仅使用单个统一模型，该模型将其子系统同化为一个系统。本文关注的是当前的方法，特别是在软件工程文本中，多模态UML被引入作为通用建模语言（即，UML是建模）。在这种情况下，我们建议在建模中提出多重性与单一性的问题。这将促进对UML优点和建模过程中可能面临的困难的基本理解，特别是在教育环境中。此外，我们主张，观点的多样性并不必然导致模式的多样性。模型奇异性方法可以表示多个视图（静态，行为），而无需采用具有各种符号的多个模型的集合。我们提出了这样一个模型的一个例子，首先开发的静态表示。然后，动态视图和行为表示建立了一个分解策略与时间的概念交织。
2021-05-03 cs.SE
Formal Verification of Ecosystem Restoration Requirements using UML and Alloy
本文提出一种基于UML元模型和Alloy形式化的模型驱动方法，通过Alloy Analyzer验证生态系统的安全性与活性属性，确保生态系统规格说明可靠并满足恢复目标，并以CRESTO实例进行说明。
2024-05-31 cs.SE
A Model Driven Approach on Object Oriented PLC Programming for Manufacturing Systems with regard to Usability
本文提出了模块化自动化复用制造系统（modAT 4 rMS）的方法，以支持模型驱动工程（MDE）面向对象的制造自动化软件的可用性和软件模块化。对于可用性，我们指的是ISO 9241-11定义的有效性、效率和用户接受度。modAT 4 rMS符号基于统一建模语言（UML）和系统建模语言（SysML）的选定功能，并通过与工业从业者以及机电一体化学员的一系列实证研究进一步迭代开发。与modAT 4 rMS的可编程逻辑控制器（PLC）编程的MDE方法开发的目标，以促进模块化的面向对象的PLC软件的编程，通过提高结构和行为图类型之间的关系的表示，并通过减少抽象层次的结构模型。介绍了PLC软件结构和软件行为建模的modAT 4 rMS表示法，并以modAT 4 rMS编辑器原型为例进行了说明。对于开发的符号的评价结果，从一项研究与168名参与者，显示这种新方法的好处相比，经典的程序范式（IEC 61131-3）和特定领域的UML配置文件plcML在编程性能和可用性方面。最后讨论了该方法的优点和局限性，并对进一步的发展进行了展望。
2022-12-09 cs.SE
Formalizing UML State Machines for Automated Verification -- A Survey
本文综述了1997至2021年间形式化UML状态机语义以进行模型检查的研究，指出形式化可消除自然语言歧义、支持自动验证，从而在早期发现设计漏洞并降低成本。
2024-07-24 cs.LO cs.SE
A Formalism-Aware Reward Loop for Handwritten UML-to-PlantUML Generation
University of Cologne（科隆大学）
本研究提出形式化感知奖励循环，通过微调视觉-语言模型结合Group Relative Policy Optimisation生成PlantUML，提升了转换质量，为建模评估提供了新方向。
2026-08-03 cs.SE
Large Language Models for Software Engineering Diagrams: A Systematic Review of UML and ER modelling
Edinburgh Napier University（爱丁堡纳皮尔大学）
该系统综述分析64项2023-2025年研究，指出LLM在UML/ER建模中存在领域失衡、GPT依赖、评估不规范等问题，提出需标准化基准等改进方向。
2026-07-30 cs.SE
From Image to UML: First Results of Image Based UML Diagram Generation Using LLMs
本文评估多种 LLM 将 UML 类图图像转换为形式化模型的能力，证明其可纳入模型驱动工程流水线，同时指出局限并强调人机协同。
2024-06-18 cs.SE
Modelling politics in requirements engineering: adding emoji to existing notations
尽管有几位作者已经认识到“政治”的概念关键是任何建筑工程（RE）过程中的一个重要组成部分，从业者仍然缺乏一个务实的答案，如何处理政治方面：这样的能力已经成为一个最可取的，但完全不详细的一部分，我们通常和含糊地称为“专业经验”。从业者也没有得到任何适当的工具或方法来容易地发现，代表，控制，如果可能的话，利用政治。作者认为，这个问题可以成功地处理和解决，如果当我们映射组织对系统的发展，我们包括权力和政治在其“太人性化”，甚至情感的维度。一个简单的方法是使用表情符号象形图：它们中的大多数都是通用语言的一部分，需求工程师可以轻松地采用和利用这些象形图来评估和生成包含额外一层“政治”信息的模型，而不需要实际引入任何新的符号。在此提出了一些支持表情符号的UML和组织结构图的例子，更多的是作为一个平台来支持沟通和分享如何处理政治的思考，而不是作为一种实际的技术来采用。
2017-03-17 cs.SE
Integrating UML with Service Refinement for Requirements Modeling and Analysis
统一建模语言（UML）是需求建模和系统设计的事实标准。UML作为一种可视化语言，可以极大地帮助客户、项目经理和开发人员指定目标系统的需求。然而，UML缺乏精确描述需求的能力，如系统操作的契约，并验证需求的一致性和细化。这些缺点导致了软件开发过程的早期阶段很难发现软件的潜在缺陷，从而需要在软件测试中付出更多的努力来发现缺陷。服务精化是一种形式化的方法，可以作为对UML的补充。在本文中，我们展示了如何集成UML与服务细化来指定需求，并通过一个在线购物系统的案例研究，验证了一致性和细化的需求。特别地，需求建模通过UML图，其中包括a）用例图，b）系统序列图和c）概念类图。服务精化通过引入契约来增强需求模型。此外，通过服务精化可以验证需求模型的一致性和精化性。我们的方法表明，将UML与服务细化相结合，与仅使用UML进行需求建模相比，实现一致性需求所需的工作量更少。
2018-03-14 cs.SE
Automatic Debugging Support for UML Designs
大型软件系统的设计需要严格应用涵盖软件过程所有阶段的软件工程方法。在早期的设计阶段进行调试是非常重要的，因为后期的错误修复是昂贵的。在本文中，我们描述了一种方法，便于调试的UML需求和设计。统一建模语言（UML）是一组用于软件系统的面向对象设计的符号。我们已经开发出一种算法，翻译的形式，注释序列图到结构化的状态图的需求规格。该算法检测序列图之间的冲突和领域知识中的不一致。在从序列图合成状态图之后，这些状态图通常受到手动修改和细化。通过使用我们的合成算法的“向后”方向，我们能够将对状态图的修改映射回需求（序列图），并检查那里的冲突。反馈给用户的冲突检测我们的算法是基于演绎的调试的需求和域理论在非常早期的发展阶段的基础。我们的方法允许生成关于为什么存在冲突以及规范的哪些部分受到影响的解释。
2000-11-13 cs.PL cs.SE
Formalization and Verification of Hierarchical Use of Interaction Overview Diagrams Using Timing Diagrams
由于其图形化的符号和简单性，统一建模语言（UML）是一个事实标准，是工业界和学术界广泛使用的语言，尽管它的语义仍然是非正式的。交互概述图（IOD）是在UML 2中引入的;它允许以层次化的方式对行为进行规范。本文是一个正式的动态语义的UML 2的贡献。我们从正式化IOD的分层使用开始。然后，利用赋时着色Petri网（赋时CP-net）完成了IOD、时序图和时序图到层次着色Petri网（HCPNs）的映射。我们的方法可以帮助设计人员从抽象中获益，以及在两个以上的层次结构，降低验证复杂性的细化。
2014-01-22 cs.LO 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
A Language-theoretic View on Guidelines and Consistency Rules of UML
UML的准则和一致性规则用于控制语言提供的自由度以防止错误。准则用于特定领域（例如，航空电子设备），以建议正确使用的技术。一致性规则用于处理模型中的不一致性。然而，指南和一致性规则对语言的使用非正式的限制，这使得检查变得困难。在本文中，我们考虑这些问题，从语言理论的观点。我们提出了C系统的形式化，简称“形式语言控制系统”。C系统由受控文法和控制文法组成。准则和一致性规则被形式化为控制UML使用的控制语法，即使用UML语法的派生。这种方法可以实现为一个解析器，它可以自动验证XMI格式的UML用户模型上的规则。与相关工作的比较显示了我们的贡献：一个通用的自顶向下和基于语法的方法，在编译时检查语言级的约束。
2009-05-14 cs.FL cs.SE
Prior Bias in Vision Language Models on UML Diagram Interpretation
Dept. of Computer Science（计算机科学系）；William & Mary, USA（威廉玛丽学院）
研究视觉语言模型在UML图解释时是依据先验知识还是真正理解图表。通过引入对比基准测试，评估多个模型，发现反转关系箭头会降低开源模型关系方向准确率，不同模型表现有差异，揭示先验驱动的理解故障。
2026-07-07 cs.CV 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
Conceptual Modeling with Constraints
保证系统质量的一个重要因素是开发一个概念模型，该模型反映了关于其领域的知识以及关于其必须执行的功能的知识。在软件工程中，概念建模作为一门提供语言、方法和方法论来解决软件开发复杂性的学科已经变得重要起来。理解这种复杂性的关键是在不同的表示层次上使用图等工具。一个概念模型必须包括其领域的所有相关静态和行为方面。在UML中，静态方面包括表示系统内部架构的结构图，特别关注类，它们所具有的连接和交互，以及域状态的完整性约束。UML对于某些约束的完整规范没有足够的表达能力。约束有助于分析允许的设计要求和预期功能的限制。为了克服图形符号的限制，使用其他类型的语言来补充图解语言（例如，文本对象约束语言[OCL]）。在本文中，我们研究了如何表达约束图解使用思维机（TM）通过UML/OCL文献中的例子。这将有助于进一步理解概念建模中的约束概念。它也展示了TM的表现力和局限性。本文认为，TM可以提供一个图形化的约束语言的概念模型。
2022-06-05 cs.SE
An Institution for Simple UML State Machines
我们提出了一个没有层次状态的UML状态机的机构。与UML类图的交互是通过守卫和动作的机构来处理的，这些机构提供了状态的动态组件（例如属性的赋值），但抽象了类图的细节。我们还研究了交错产品的概念，它捕捉了几个状态机的相互作用。交错积构造是复合结构图的语义的基础，其可用于指定状态机的交互。这项工作是一个更大的努力，建立一个框架，正式的软件开发与UML的基础上，异构的方法，使用机构。
2014-11-17 cs.LO cs.SE
Collaborative Software Modeling in Virtual Reality
建模是概念设计和系统设计的关键活动。通过协作建模，最终用户、利益相关者、专家和企业家能够创建对系统表示的共享理解。统一建模语言（UML）是面向对象软件工程中主要的概念建模语言之一，但UML的建模质量及其工具支持越来越受到人们的关注。其中，其符号的二维表示的限制和缺乏自然的协作建模工具被报道是显着的。在本文中，我们探讨了使用虚拟现实（VR）技术的协同UML软件设计的潜力，通过比较它与经典的协同软件设计使用传统的设备（台式PC，笔记本电脑）。为此，我们开发了一个VR建模环境，为UML类图提供自然的协作建模体验。基于24名参与者的用户研究，我们比较了协作VR建模与传统建模的效率，有效性和用户满意度。结果表明，VR的使用在效率和效果方面存在一些缺点，但用户的乐趣，与远程协作者在同一个房间的感觉，以及协作的自然性都有所增加。
2021-07-27 cs.HC cs.SE
Towards Enabling Overture as a Platform for Formal Notation IDEs
形式化方法工具永远不会像流行的程序设计语言工具那样拥有那么多的用户，因此在构建集成开发环境（IDE）上所花费的精力将比诸如Java之类的程序设计语言低几个数量级。这意味着正式方法的新手无法获得与他们喜爱的编程IDE相同的用户体验。为了改善这种情况，有必要将各种努力结合起来，以便可以重用通用功能，而不是每次都从头开始。本文介绍了这样一个重用的哲学是目前的序曲平台。我们给出了平台本身的概述，以及支持大部分重用的可扩展性原则。本文还包含几个平台扩展的示例，包括新功能和支持新语言的新IDE。
2015-08-17 cs.SE
Towards a Semantics of Activity Diagrams with Semantic Variation Points
UML活动图已经成为一种建立在各种抽象层次上的模型控制和数据流的符号，从算法的细粒度描述到业务应用程序中的高级工作流模型。一个形式化的语义必须捕捉在真实系统中活动图的解释的灵活性，这使得它不适合定义一个固定的形式化语义。在本文中，我们定义了一个语义的语义变化点，允许一个可定制的，特定于应用程序的解释活动图。我们研究活动图语义的具体变体，这也可能需要语法的变体来反映当前的预期用途。
2014-09-08 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
B Maude: A formal executable environment for Abstract Machine Notation Descriptions
我们提出了B Maude，一个原型的可执行环境的抽象机器记法实现的Maude语言。B Maude是形式化定义的，它是将AMN的语义实现为$π$框架中的表示的结果，该框架是Mosses的基于一致性的语义和Plotkin的解释自动机的实现。B Maude赋予B方法重写执行、符号搜索和AMN描述的线性时态逻辑模型检验。
2021-08-17 cs.LO cs.SE
Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams
WeChat Pay, Tencent Inc（腾讯公司）；The Chinese University of Hong Kong（香港中文大学）；Wuhan University（武汉大学）
提出UML2Dep框架，通过增强UML顺序图显式形式化复杂需求，并引入数据依赖推断（DDI）任务构建依赖图，结合静态解析与剪枝降低复杂性，提升LLM代码生成的准确性与效率。
2025-11-05 cs.AI 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
User Centered Development of Agent-based Business Process Models and Notations
我们讨论了以用户为中心的业务流程建模符号的开发问题。在我们的研究中心有一个功能齐全的多企业业务流程平台（ME-BPP）的概念的基础上，基于代理的业务流程，它建立在面向主题的业务流程管理方法（S-BPM）的正式基础。该平台基于云技术使用商业服务实现。此外，我们开发了一个“块建模”技术，以找到一个语义透明的建模符号，可以使用新手用户建模面向主题的业务流程（S-BPM）模型。由于这是正在进行的研究，仍然存在严重的开放问题。但是，所提出的方法打破了一些典型的过程建模符号的规则，并希望刺激创新。此外，我们要继续我们的研究，对我们的建模方法，以用户为中心的“语法和语义自由”的建模技术，以开发用户和特定领域的建模符号的增强。
2014-05-13 cs.SE
Towards Integrated Modelling of Dynamic Access Control with UML and Event-B
基于角色的访问控制（RBAC）是一种流行的授权模型，用于管理各种系统中的数据访问约束。RBAC通常定义静态视图上的访问权。然而，为了确保系统的可靠性，通常需要对依赖于状态的访问权进行建模和验证。这样的建模允许我们显式地定义系统状态与访问和修改某些数据的权限之间的依赖关系。在本文中，我们提出了一个正在进行的工作相结合的图形化和形式化建模，以指定和验证动态访问控制。一个案例研究-一个报告管理系统-说明了这种方法。
2018-05-15 cs.LO cs.SE
Modeling Dynamic Component Interfaces
我们采用了一种基于面向对象系统的组件模型，介绍了组件的概念和结构。组件由一组动态变化的连接对象组成。这些对象中只有一部分是接口对象，因此可以从环境中访问。在组件的生存期内，不仅对象的数量会改变，接口对象的数量也会改变，它们之间的连接也会改变。为了描述这种情况，我们引入组件接口图（CID）-一个自适应的UML的UML图-作为一个符号来表征组件的接口，它们的结构，和它们的可导航性。我们将展示如何CID可以用来描述内部开发的开放式编辑器框架（OEF）。最后，我们给出了一些指导原则，这些指导原则允许将用CID描述的组件直接映射到几种组件技术，如ActiveX、CORBA或Java Bean
2014-09-24 cs.SE
UML Sequence Diagram: An Alternative Model
序列图的普遍接受可以归因于它们相对直观的性质和描述部分行为的能力（与状态图等图相反）。然而，研究表明，超过80%的毕业生无法创建软件设计，甚至无法创建部分设计，许多学生不知道序列图如何受到其他模型的约束。许多学生在识别有效的交互对象和用适当的参数构建消息方面表现出困难。此外，根据权威人士的说法，尽管已经为序列图提出了许多不同的语义（例如，转换到状态机），不存在所需序列图行为的合适的语义基础细化，因为直接样式语义不能精确地捕获所需序列图行为;转换到其他形式主义忽略了序列图的基本特征，例如保护条件和临界区域。本文提出了一种替代序列图，一个广义的模型，提供了进一步的理解序列图同化到一个新的建模语言称为思维机（TM）。序列图通过去除表面的仅垂直维度的扩展限制而水平扩展，以保留事件的逻辑年表。TM算法在动作方面是非线性传播的。事件及其年表是在第二个描述平面上构建的，该平面叠加在最初的静态描述上。其结果是一个更精确的表示，将简化建模过程。这是通过重建序列图的情况下，从文献中证明。
2021-05-31 cs.SE
A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems
针对BPMN执行语义非形式化导致的解读差异与属性验证难题，提出基于BPMN模型到图变换系统高阶变换的形式化方案，覆盖更多元素且便于验证，已实现为开源网页工具。
2024-10-04 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
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
Towards Conceptual Modeling Semantics: Eventizing Tarski's Truth Schema
软件工程中的建模语言（例如，UML）是从软件系统建模发展而来的，在软件系统建模中，指称和操作类型的语义是研究和实践的传统主题。根据一些作者，虽然大部分静态语义（例如，UML）似乎已经达成了共识，活动、交互和状态机的动态语义构成了一个重大挑战。语义学的核心是句子与（实际）世界之间的关系。仔细检查建模语言领域中与语义相关的问题以避免可能影响实际适用性的问题是很重要的。在这方面的一个努力是OMG发布的2020年基础UML（fUML）规范草案，其基本语义指定了与传统程序设计语言中的程序相同意义上的可执行。此外，学术界的努力已经寻求开发一种替代方法来使用形式语义（例如，使用罗素的类型理论和塔斯基的声明语义学）。本文旨在开发语义学的类似探索性冒险，只是为了一种更温和的图形建模语言，称为事物机器模型。该模型促进了对仔细审查的建模语言的深入理解，并导致相当富有成效的问题。构建thinging机器模型似乎有助于这一方向的进展，本文的初步结果表明该方法的可行性。
2020-11-03 cs.SE
YANG2UML: Bijective Transformation and Simplification of YANG to UML
Universität der Bundeswehr München（慕尼黑联邦国防军大学）；University of Twente（特文特大学）
软件定义网络目前正在通过将网络控制（控制平面）与转发功能（数据平面）解耦来革命性地改变计算机网络，从而使得网络控制能够变得可直接编程，并且底层基础设施能够被抽象用于应用和网络服务。除了众所周知的OpenFlow协议之外，基于XML的NETCONF协议也是用于从管理平台交换配置信息的重要手段，并且现在甚至是OpenFlow的一部分。与NETCONF结合，YANG是定义支持几乎所有网络配置协议的相关数据结构的相应协议。YANG本身是一种语义丰富的语言，为了便于熟悉相关主题，它经常被可视化为涉及其他专家或开发人员，并通过他们的日常工作（使用YANG编写应用程序）来支持他们。为了支持这一过程，本文提出了一种新的方法来优化和简化YANG数据模型，以帮助进一步讨论与管理和实现（特别是接口），以降低复杂性。因此，我们定义了一个双向映射的杨UML和开发一个工具，使创建的UML图。这结合了使用形式语言YANG和自动维护的UML图的好处，使其他专家或开发人员参与进来，缩小了技术上改进的数据模型和它们的人类可读性之间的差距。
2020-05-07 cs.CL cs.DC cs.NI
Automatization of building IT projects using composite consistency rules
University of Economics and Human Sciences in Warsaw（华沙经济人文大学）；Warsaw University of Technology（华沙理工大学）
本文提出复合一致性规则，通过整合简单规则提升UML建模的自动化水平，减少冗余，提高一致性和完整性，并支持模式驱动建模及AI辅助架构生成。
2026-03-25 cs.SE
Semantics and Analysis of DMN Decision Tables
决策模型和表示法（DMN）是一种标准表示法，用于捕获一般业务应用程序和特定业务流程中的决策逻辑。DMN中的一个核心结构是决策表。越来越多地使用DMN决策表来捕获关键业务知识，这就需要支持这些表上的分析任务，例如正确性和完整性检查。本文提供了DMN表的形式化语义、关键分析任务的形式化定义以及解决两个此类任务的可扩展算法，即，重叠规则和缺失规则的检测。该算法基于决策表的几何解释，可用于通过利用几何算法来支持其他分析任务。该算法已在开源DMN编辑器中实现，并在来自信贷数据集的大型决策表上进行了测试。
2016-03-24 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
