Modularizing Behavioral and Architectural Crosscutting Concerns in Formal Component-Based Systems - Application to the Behavior Interaction Priority Framework
我们定义了一种方法来模块化的横切关注的行为交互优先级（BIP）框架表示的基于行为的系统（CBS）。我们的方法是从面向方面编程（AOP）的范式，最初设想支持在单片系统的开发过程中的关注点分离的启发。BIP有一个正式的操作语义，并在体系结构和行为之间进行了明确的分离，以允许系统的组合和增量设计和分析。我们区分地方和全球方面。局部方面在组件级别对关注点建模，并用于细化组件的行为。全局方面在体系结构级别对关注点建模，因此改进了组件之间的通信（同步和数据传输）。我们通过严格的转换基元将局部和全局方面以及它们的组成和集成形式化到BIP系统中。我们提出了AOP-BIP，一个面向AEE的BIP系统的编程工具，演示了它的使用模块化的日志记录，安全性和容错性的网络协议，并讨论其可能的使用在运行时验证的CBS。
2018-05-22 cs.SE
A Rule-Based Change Impact Analysis Approach in Software Architecture for Requirements Changes
软件系统通常运行在一个动态的环境中，他们的需求不断变化，新的需求经常出现。单个需求很难孤立存在：它与其他需求以及实现它的软件开发工件相关。当引入需求变更时，需求工程师可能不得不手动分析单个变更的所有需求和架构元素。这可能会导致忽略变更的实际影响。我们的目标是通过使用需求关系、需求变化和需求与体系结构之间的痕迹的形式化语义来改进软件体系结构中需求变化的变化影响分析。在我们以前的工作中，我们提出了一种技术，用于需求中的变更影响分析。该技术使用了需求关系和变更的形式化语义。它的输出是一组候选需求，这些候选需求会对所提出的变更产生影响，并且会在需求模型中产生传播路径。在本文中，我们提出了一种补充技术，传播需求变化的软件架构，并找出这些变化的影响架构元素。R&A之间的需求关系、变更和跟踪的形式化用于确定候选架构元素，以应对架构中需求变更的影响。工具支持是我们的需求推理和一致性检查工具（TRIC）的扩展。我们的方法有助于消除一些错误的积极影响，在变化传播。我们说明了我们的方法在一个工业的例子表明，需求关系，变化和痕迹的形式语义，使候选人的建筑元素的识别与减少一些假阳性的影响。
2016-08-09 cs.SE
UML 2 Semantics Symposium: Formal Semantics for UML
本次研讨会的目的，与MODELS 2006年举行，是目前的UML 2语义项目的研究现状。从专家听众那里获得反馈同样重要的是，有机会邀请该领域的研究人员讨论他们自己与统一建模语言的正式语义相关的工作。本次研讨会是我们与ECMDA 2005联合举办的第一次研讨会的后续研讨会。
2014-09-22 cs.SE
Architectural Software Patterns for the Development of IoT Smart Applications
软件开发人员通常在没有正式架构的情况下开始编写应用程序，并依赖直觉和经验，而不是众所周知的设计模式。推荐一种不同的方法来开发物联网智能应用程序，因为它结合了传感器，执行器，通信技术和大数据分析的高度复杂性，以及它跨越不同领域，雾和云基础设施层的分布式性质。文献报告了物联网智能应用程序软件开发的许多经验。然而，架构解决方案的提出没有合理的选择软件组件和它们之间的相互关系。本文提出了软件组件及其关系的分类，以便为特定的物联网智能应用程序建模软件架构。我们选择了城市、建筑和农业的三个智能应用程序作为使用一些组件、连接器和众所周知的设计模式的示例。最后，讨论了物联网软件架构选择中涉及的问题和挑战。
2020-03-17 cs.SE
Formal Semantics of the CDL Language
我们逆向工程的组件定义语言（CDL），这是高度可配置的，嵌入式操作系统eCos的一部分的正式语义。这项工作提供了基础上的分析和比较的两个可变性建模语言Kconfig和CDL。本文档中给出的语义是基于对CDL文档的分析、对工具链源代码的检查以及对特定示例的工具测试。
2022-09-23 cs.SE
Training Software Engineers for Qualitative Evaluation of Software Architecture
软件架构师使用质量需求来设计系统的架构。但是，必须确保系统的最终架构设计达到标准质量要求。现有的架构评估框架需要基本的技能和经验，以实际使用，新手软件架构师缺乏。我们提出了一个框架，使新手软件架构师推断系统的质量要求和策略，使用软件架构块线图。该框架将图像作为输入，提取各种组件和连接，并将其映射到可行的架构模式，然后识别系统相应的质量属性（QA）和策略。该框架包括基于图像处理和语义相似性方法的专门训练的机器学习模型，以帮助软件架构师通过以下方式评估给定设计：a）基于输入架构设计中存在的架构模式评估输入架构设计，b）列出设计在QA方面的优点和缺点，c）推荐必要的架构策略，这些策略可以嵌入到设计中，以实现缺乏的QA。为了训练我们的框架，我们开发了一个包含2，035个架构图像的数据集，这些架构图像来自14种架构模式，如客户端-服务器，微服务和模型视图控制器，可在https://www.doi.org/10.6084/m9.figshare.14156408上获得。该框架在识别建筑模式方面达到了98.71%的正确识别率。我们评估了所提出的框架的有效性和实用性，通过使用控制组和实验组，其中实验组的表现比控制组好约150%。实验作为工程学院计算机科学硕士课程的一部分进行。
2021-05-20 cs.SE
Recovering Architectural Variability of a Family of Product Variants
软件产品线（SPL）的目标是应用预先计划的系统重用大粒度的软件工件，以提高软件生产率，降低开发成本。SPL的思想是通过分析产品族的业务领域来识别产品之间的共性和可变性。然而，公司通常以特别的方式（例如克隆和拥有）开发一套产品，这些产品具有共同的功能，但在其他方面有所不同。因此，许多最近的研究成果提出了重新设计现有的产品变体的SPL。然而，这些贡献主要集中在管理需求级别的可变性。很少有贡献解决的可变性，在建筑水平，尽管它的主要重要性。从这一观察，我们提出，在本文中，一种方法来逆向工程的一组产品变体的架构。我们的目标是在架构级别上识别架构元素变体之间的可变性和依赖性。我们的工作依赖于形式概念分析（FCA）来分析变异性。为了验证所提出的方法，我们在两个开源产品变体系列上进行了实验：移动媒体和健康观察者。结果表明，我们的方法是能够识别架构的可变性和依赖关系。
2016-06-01 cs.SE
Formal Semantics and Soundness of a Translation from Event-B Actions to SQL Statements
EventB 2SQL工具将Event-B模型转换为持久化Java应用程序，后者将模型的状态存储在关系数据库中。大多数Event-B赋值直接转换为SQL数据库修改语句，然后可以对数据库执行这些语句。在这项工作中，我们提出了一个正式的语义，并证明了合理的翻译集合的赋值语句代表的动作的事件B事件。这使得生成的代码可以在其正确性方面有信心地使用。
2016-06-08 cs.SE
Formal Semantics of the Kconfig Language
Kconfig语言定义了一组符号，在配置中为它们分配一个值。我们根据xconfig配置器中的行为描述Kconfig语言的语义。我们假设Kconfig语言中概念的抽象语法表示，并将具体到抽象语法的转换细节委托给以后的文档。
2022-09-11 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
Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
Maynooth University（梅努斯大学）
本文提出学习融合形式推理框架，通过自然语言要求自动合成合同、利用图匹配和学习嵌入重用验证成果，并基于UTP和机构理论建立数学语义基础，推动验证从孤立证明转向知识驱动过程。
2026-04-14 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
Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs
School of Computer Science and Technology, Xidian University（西安电子科技大学计算机科学与技术学院）；Guangzhou Institute of Technology of Xidian University（西安电子科技大学广州研究院）；China Academy of Space Technology（中国空间技术研究院）
本文提出Req2LTL框架，通过层次中间表示OnionL将自然语言需求转换为LTL，实现88.4%的语义准确性和100%的语法正确性。
2025-12-19 cs.SE
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models
领域特定语言（DSL）的语义的正式定义是验证使用这种DSL指定的模型和应用于这些模型的转换的正确性的关键先决条件。出于这个原因，我们实现了一个原型的DSL的语义规范的系统组成的并发，通信对象。使用这个原型，在DSL中指定的模型可以被转换为标记转换系统（LTS）。这种将模型转换为LTS的方法使我们能够将现有的可视化和验证工具应用于模型，只需很少或无需进一步的努力。该原型是使用ASF+SDF元环境，代数规约语言ASF+SDF，它提供了有效的执行转换以及读取模型和生产LTS的能力，没有任何额外的前或后处理的IDE实现的。
2011-06-30 cs.SE
Managing Separation of Concerns in Grid Applications Through Architectural Model Transformations
网格能够通过称为虚拟组织（VO）的临时协作，使用文件、应用程序和存储设备来聚合、虚拟化和共享大量异构和地理上分散的资源，以解决跨机构和国家的计算和数据密集型问题。大多数实现都会导致软件层的复杂叠加，通常会带来较低的服务质量和应用程序质量。因此，基于网格的应用程序的设计和开发越来越复杂，使用最经典的工程实践是不成功的。不仅是这样的应用程序的开发是一项耗时，容易出错和昂贵的任务，而且由此产生的应用程序往往是硬编码的特定网格配置，平台和基础设施。在基于网格的应用程序的设计中既没有指导方针也没有规则是一个矛盾，因为有许多现有的分布式计算的体系结构方法，这些方法可以简化和促进基于软件组件重用的严格工程方法。我们相信，目前使用的ad-hoc和半正式的工程方法，不足以满足未来的网格开发需求。由于基于网格的应用程序解决多学科和复杂的领域（健康，军事，科学计算），他们的工程需要严格和控制。因此，本文主张一个正式的模型驱动的工程过程和相应的设计框架和工具，用于建设下一代网格。
2007-07-05 cs.DC cs.SE
Detecting Architectural Erosion using Runtime Verification
系统的架构捕获系统的重要设计决策。随着时间的推移，系统实现中的更改可能会导致违反特定的设计决策。这个问题在工业中很常见，被称为建筑侵蚀。由于它可能会对系统的质量产生严重的后果，研究的重点是开发工具和技术来解决所提出的问题。到目前为止，大多数检测建筑侵蚀的方法都采用静态分析技术。虽然这些技术非常适合于分析静态架构，但当涉及到动态架构时，它们就达到了极限。因此，在本文中，我们提出了一种基于运行时验证的替代方法。为此，我们提出了一个系统的方法来翻译一个正式的规范的建筑约束的监视器，它可以用来检测违反这些约束。该方法是在Eclipse/EMF中实现的，通过一个运行的例子证明，并使用两个案例研究进行评估。
2019-09-12 cs.DC cs.LO cs.SE
An Architectural Style for Self-Adaptive Multi-Agent Systems
现代分布式软件系统通常运行在动态环境中，其中运行条件连续变化，子系统可以随意进出，例如智能交通管理和多机器人系统。为了管理这些动态，这些系统必须动态地自适应其结构和行为。虽然我们看到过去十年来在设计这种系统的方式方面取得了重大进展，但仍然存在持续的挑战。特别是，处理分布和分散控制仍然是自适应系统的主要挑战之一。该报告提出了一种架构风格，支持软件架构师为一系列分散自适应系统设计架构。体系结构风格的结构中的一些相互作用的自治实体（代理），合作实现系统任务的软件。多智能体系统从建筑风格派生实现灵活性（代理适应他们的行为和相互作用，以可变的操作条件）和开放性（代理处理自主与其他代理进入和离开系统）。架构风格由五个相关的模式，提取领域特定的架构知识，从开发各种多代理系统的丰富经验。使用pi-ADL，一个正式的体系结构描述语言，支持规范的动态体系结构的体系结构模式。该规范为架构师提供了对模式的架构元素、它们的交互和行为的严格描述。我们说明了我们如何应用的建筑风格与摘录的两个案例，从我们的实践：一个实验系统预期的交通路线和工业物流系统的自动化运输在仓库环境。
2019-09-08 cs.MA cs.SE
K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
本文提出K-CIRCT，首个针对CIRCT硬件中间表示子集的分层、可组合且可执行的形式语义，支持RISC-V处理器模拟，并通过全规则覆盖测试和riscv-mini验证了其有效性与实用性。
2024-04-29 cs.PL cs.SE
AI-Assisted Engineering Should Track the Epistemic Status and Temporal Validity of Architectural Decisions
DeepThought Solutions；Department of Computer Science University of Florida（佛罗里达大学计算机科学系）
本文提出第一原理框架（FPF）以跟踪架构决策的epistemic状态和时间有效性，通过epistemic层、保守聚合和自动证据衰减机制，解决AI辅助工程中证据过期和信任膨胀的问题。
2026-01-28 cs.AI cs.SE
Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
Department of Computer Science（计算机科学系）
提出将形式化方法与人工智能融合的长期研究愿景，通过自动化合约合成、语义工件复用和精化理论，构建知识驱动的验证生态系统，加速未来保障。
2026-06-17 cs.AI cs.SE
Automated Analysis of Multi-View Software Architectures
软件架构通常由不同的视图组成，用于捕获静态、运行时和部署方面。然而，目前缺少的是在软件开发生命周期的早期阶段对多视图体系结构进行正式的确认和验证技术。因此，本文的主要贡献是一个单一的正式模型（在Promela）的建设，为某些程式化的，广泛使用的，多视图架构，通过适当的解释和融合子模型从不同的UML图。由模型检验产生的可能反例被反馈作为用于调试多视图架构模型的测试场景。我们已经实现了这个算法作为一个插件的企业架构师开发工具，并成功地使用SPIN模型检验调试一些工业建筑多视图模型，通过识别一些不良的角落情况。
2017-04-24 cs.LO cs.SE
Formal Semantic Annotations for Models Interoperability in a PLM environment
如今，企业内部或企业之间对系统互操作性的需求变得越来越普遍。人们在信息交换、转换、发现和重用方面进行了大量的研究工作。这些研究的主要挑战之一是克服企业应用程序之间的语义异构性沿产品的生命周期。语义标注作为辅助语义互操作的一种可能的解决方案，得到了越来越多的关注，并被广泛应用于各个领域。在本文中，调查的背景和相关工作的基础上，我们发现了一些现有的缺点，并提出了一个正式的语义标注方法，以支持在PLM环境中的模型的语义丰富。
2014-11-13 cs.DB cs.SE
Industrial Experiences with a Formal DSL Semantics to Check Correctness of DSL Transformations
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的一致性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件之间的一致性。我们利用工业项目中的形式化语义，并使用形式化技术的基础上，等价性检查和基于模型的测试的一致性检查。我们报告我们的经验，这种方法在一个工业发展项目。
2015-11-25 cs.LO cs.PL cs.SE
Industrial Experiences with a Formal DSL Semantics to Check the Correctness of DSL Artifacts
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的正确性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件的正确性。我们利用工业项目中的形式语义，并使用基于等价性检查和基于模型的测试验证生成的工件的正确性的形式化技术。我们报告我们的经验，这种方法在一个工业发展项目。
2016-03-29 cs.LO cs.PL cs.SE
A Tool for Automated Reasoning About Traces Based on Configurable Formal Semantics
本研究提出支持可配置迹语义的Tarski工具，可自动推导迹并检查一致性，已在汽车领域三个工业案例中验证有效。
2024-03-09 cs.PL cs.SE
Toward a Formal Semantics for Autonomic Components
自治管理可以提高并行/分布式应用提供的QoS。在CoreGRID组件模型中，自主管理被定制为组件组装的自动监控驱动的变更，因此被定义为（分布式）管理代码的效果。这项工作产生了一个语义的基础上超图重写适合建模的动态演化和非功能方面的面向服务的架构和基于组件的自主应用程序。在这方面，我们的主要目标是提供一个正式的描述，通常只有非正式指定的适应操作。我们认为，我们的方法更容易提高自主和自适应应用程序中的管理代码的抽象层次。
2010-07-02 cs.DC cs.SE
Simulator Semantics for System Level Formal Verification
Sapienza University of Rome（罗马第一大学）
本文提出系统级形式验证中模拟器的正式语义，以解决模拟器行为未被形式化建模的问题，确保验证方法的正确性。
2015-09-24 cs.SE cs.SY eess.SY
Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
School of Computing and Information Systems（计算与信息系统学院）；The University of Melbourne（墨尔本大学）
本文引入综合基准 FormalBench 评估 LLM 对程序语义的推理能力，发现其在复杂结构（如循环）和语义保持变换上表现不佳，并设计自修复提示将成功率提升 25%。
2025-05-29 cs.AI cs.PL cs.SE
Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
本文利用形式化ISA语义实现二进制代码的精确符号执行，构建了可扩展的RISC-V原型，并通过实验发现angr中的五个未知缺陷。
2025-01-20 cs.CR cs.PL cs.SE
