首页/论文/1409.7241

arXiv 1409.72412014-09-25cs.SE

数据流体系结构的逐步细化

Stepwise Refinement of Data Flow Architectures

Jan Philipps, Bernhard Rumpe

备注：: 18 pages, 1 figure. arXiv admin note: substantial text overlap with arXiv:1409.6932
发表信息：: Software Architectures and Design Patterns in Business Applications Technische Universität München, TUM-I9746. 1997

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文的目的是将实际软件开发方法中使用的异构文档集成到一个基于形式化精化的软件开发过程中来描述视图。因此，我们提出了一个集成的语义异构文档的基础上，一个共同的系统模型和一组语法的发展步骤与一个定义良好的语义文档的演变。在一个小例子中演示了开发步骤的使用。

英文摘要：

This paper aims at integrating heterogeneous documents used in pragmatic software develpoment methods to describe views with a formal refinement based software development process. Therefore we propose an integrated semantics of heterogeneous documents based on a common system model and a set of syntactic development steps with a welldefined semantics for document evolution. The use of the development steps is demonstrated in a small example.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

SR-Eval: 评估在逐步需求细化下的LLM代码生成能力

SR-Eval: Evaluating LLMs on Code Generation under Stepwise Requirement Refinement

Sichuan University（四川大学）；The Chinese University of Hong Kong（香港中文大学）

SR-Eval是一个针对迭代代码生成的评估基准，通过多轮交互模拟真实开发流程，评估LLM在逐步需求细化下的表现，发现最佳模型在功能级任务中仅达到22.67%的完成率。

2026-03-17cs.SE

可解释且可验证的硬件生成：基于LLM驱动的逐步细化

Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement

The University of Texas at Austin（德克萨斯大学奥斯汀分校）；Fudan University（复旦大学）；USA（美国）

提出结合LLM创造力与形式化方法可解释性的硬件生成框架，通过迭代应用变换规则将设计规范转换为正确性有保证的RTL程序。

2026-07-15cs.AIcs.SE

从单体到微服务架构的逐步迁移：性能和迁移工作量评估

Stepwise Migration of a Monolith to a Microservices Architecture: Performance and Migration Effort Evaluation

当今业务固有的敏捷性促进了软件架构的定义，其中业务实体被解耦为模块和/或服务。然而，具有丰富的领域模型是有优势的，其中领域实体紧密连接，因为它促进了最初的快速开发。另一方面，将业务逻辑拆分为模块和/或服务，通过定义良好的接口进行封装，以及引入服务间通信，都会带来性能方面的成本。在本文中，我们分析了使用富域对象将单体逐步迁移到微服务架构中，其中模块化单体架构用作中间步骤。这两个步骤对迁移工作和性能的影响都进行了测量。目前的技术水平分析了整体系统向微服务架构的迁移，但我们观察到，迁移工作和性能问题在迁移到模块化整体系统时已经很重要了。因此，为每个步骤建立了明确的区别，这可以告知软件架构师关于整体系统迁移的规划。特别是，做所有的迁移过程或只是迁移到一个模块化的整体的权衡。

2022-01-17cs.SE

信息流体系结构的改进

Refinement of Information Flow Architectures

一个演算的抽象信息流体系结构的逐步完善。我们给出了一个数学模型的信息流组件之间的关系的基础上输入和输出的通信历史，并描述系统架构使用两个视图：玻璃盒视图是一个网络的基本组件，而黑箱视图网络本身作为一个组件。这使我们能够分层地组成系统。演算包括添加或删除组件和通道的基本规则，以及用子网络替换组件，反之亦然。从体系结构的黑箱观点出发，通过精化关系证明了规则的正确性。

2014-09-24cs.SE

事件B中的飞机着陆系统建模（完整报告）

Modelling an Aircraft Landing System in Event-B (Full Report)

关键系统中的硬件或软件故障可能导致生命损失。在系统开发过程中，设计错误可能是引入故障的主要原因。形式化技术是验证关键系统正确性的一种替代方法，克服了传统验证技术如仿真和测试的局限性。日益增加的复杂性和故障率给航空电子系统的验证和确认领域带来了新的挑战。由于软件的可靠性无法量化，因此\textit{correct by construction}方法可以实现可靠的系统。精化在从抽象规范到具体系统的增量式构建大型系统中扮演着重要角色。本文是对某型飞机着陆系统的逐步形式化开发。正式的模型包括复杂的行为，时间行为和起落架系统的操作顺序。模型的形式化事件B建模语言，支持逐步细化。该案例研究被认为是专门用于验证系统行为特性的技术和工具的基准。该报告是为ABZ 2014案例研究发表的论文的完整版本。是

2014-07-03cs.SE

基于精化的规格说明：需求和体系结构

Refinement-Based Specification: Requirements and Architecture

本文介绍了系统的需求和体系结构w.r.t.它们的分解和提炼它还介绍了细化层和基于细化的验证的想法。

2014-04-29cs.SE

更多相关论文收起更多论文

事件B细化的CSP解释

A CSP Account of Event-B Refinement

事件B通过细化为逐步的系统开发提供了一个灵活的框架。该框架支持以下步骤：（a）细化事件（逐个），（b）拆分事件（逐个），以及（c）引入新事件。此外，在每一个步骤中，事件都可能被预见或收敛。所有这些步骤都附有确切的举证义务。尽管如此，仍然不清楚Event-B机器和它的细化之间的确切关系-在面向行为的语义方面。在本文中，我们给出了CSP帐户的事件-B细化，与治疗的第一次分裂事件和预期的事件。为此，我们定义了一个CSP语义的事件-B，并显示如何不同形式的事件-B细化可以被捕获为CSP细化。

2011-06-21cs.LOcs.SE

Isabelle中安全工程的形式化开发周期

A Formal Development Cycle for Security Engineering in Isabelle

在本文中，我们展示了一个安全工程过程的基础上，完善的正式概念完全正式的证明助手伊莎贝尔。这个改进-风险循环侧重于由交互式定理证明支持的攻击分析和安全改进。由于我们使用了一个完全形式化的模型与演员和政策的基础设施，我们可以支持一种新的方式正式的安全细化系统规范。这个正式的过程实际上是建立作为一个扩展的Isabelle基础设施框架的攻击树。我们定义了基础设施模型细化的正式概念。由于Kripke结构和Isabelle基础架构中的分支时间时序逻辑的形式化基础，这些逐步转换可以与攻击树分析交织，从而提供完全形式化的安全工程框架。该过程在介绍GDPR要求和区块链的物联网医疗保健案例研究中进行了说明。

2020-01-04cs.CRcs.SE

管道和过滤器体系结构的改进

Refinement of Pipe-and-Filter Architectures

软件和硬件架构易于修改。我们演示了如何数学上成立的强大的细化演算一类的架构，即管道和过滤器架构，可以用来修改一个系统中可证明是正确的方式。演算由向系统添加和删除过滤器（组件）和管道（通道）的基本规则组成。一个网络示例演示了我们的微积分的一些特性。微积分是简单的，灵活的和组合的。因此，它允许我们构建更复杂和更具体的规则，例如嵌入现有架构的模型或将设计模式定义为转换规则。

2014-11-10cs.SE

经验教训/分享地铁系统开发案例研究的经验

Lessons Learned/Sharing the Experience of Developing a Metro System Case Study

在本文中，我们分享了在地铁系统案例研究的整个开发过程中所获得的经验。该模型在Event-B中使用其各自的工具集罗丹平台构建。从需求开始，通过细化逐步向模型添加更多细节，我们确定了一些关键点和大型系统建模所需的可用插件（需求工程，分解，通用实例化等），这些都是缺乏的，加上工具的优点和缺点。

2012-10-26cs.SE

基于Event-B细化的责任感知自动驾驶汽车安全架构形式化建模

Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement

本文针对自动驾驶汽车在复杂交通场景下的安全形式化证明难题，提出利用Event-B细化机制建模并推导安全条件，结合目标感知责任敏感安全模型与Simplex架构引入AI黑盒控制器，证明了该机制能逐步有效开发复杂系统。

2024-01-10cs.SE

使用大语言模型进行语义增强的架构恢复结果自动优化

Semantic-Enhanced Automatic Refinement of Architecture Recovery Results Using LLMs

Nanyang Technological University（南洋理工大学）；Imperial Global Singapore（帝国理工学院新加坡分校）；Huazhong University of Science and Technology（华中科技大学）；Xi’an Jiaotong University（西安交通大学）

研究旨在简化架构恢复流程，提出Semref框架结合大语言模型与依赖分析自动优化架构，经在9个项目和10个工具上测试，采用5个指标评估，结果表明该框架提高了恢复架构的准确性。

2026-07-28cs.SE

迈向对话式开发环境：使用心智理论与多智能体架构进行需求细化

Towards Conversational Development Environments: Using Theory-of-Mind and Multi-Agent Architectures for Requirements Refinement

Centre for Software Excellence, Huawei Canada（华为加拿大卓越软件中心）；Queen's University（女王大学）

本文提出名为AlignMind的FM驱动多智能体系统，结合心智理论认知架构，在需求细化阶段迭代澄清利益相关者意图并转化为可执行工作流，经150个用例评估证明能显著提升软件开发中的需求捕捉准确性。

2025-05-28cs.AIcs.SE

关键实时的嵌入式系统软件开发的体系结构模型精化

Architecture Models Refinements for Software Development of Critical Real-time Embedded Systems

网络物理系统是由基于计算机的程序、紧密集成的网络、传感器和执行器控制或监控的系统。CPS的软件开发已经变得如此困难，以至于它代表了CPS生产的大部分成本。此外，值得注意的是，CPS中软件的集成、验证和确认需要比分析、设计和实现活动更多的努力。主要原因是，这些活动是在开发过程的后期进行的，在该过程的这一阶段发现的问题将需要对先前活动（即分析、设计和/或实现）中产生的工件进行返工。在本文中，我们提出了我们的工作，旨在提高可靠性的软件开发领域的CPS。在这种情况下，我们将开发过程的可靠性定义为交付中间工件的能力，其中返工工作将尽可能小。这个问题对于通用软件（即在台式计算机或服务器上使用的软件）来说非常困难，并且对于CPS中的软件来说甚至更困难。主要原因是CPS中的软件通常是关键的、实时的【形】并且嵌入在特定于域的执行平台上。因此，CPS中软件应用程序的非功能属性（也称为质量属性）通常与这些应用程序的逻辑正确性一样重要且难以满足。为了提高CPS领域软件开发的可靠性，提出了一种基于逐步细化软件体系结构描述的模型驱动工程（MDE）方法。本文总结了用这种方法得到的结果。

2019-11-24cs.SEcs.SYeess.SY