共查询到19条相似文献,搜索用时 78 毫秒
1.
采用形式化技术的软件再工程 总被引:4,自引:0,他引:4
形式化技术为软件再工程提供了完备的理论基础,该文对基于软件再工程的形式化方法进行了探讨,提出了一个统一的面向软件再工程的形式化方法。 相似文献
2.
需求工程的形式化途径 总被引:1,自引:0,他引:1
1.引言需求工程是软件工程的初始阶段,其总的目标是从用户的模糊而又不完整的要求生成准确的、完整的规格说明。需求工程的研究主要有形式化途径和非形式化途径,后者的出发点是认为需求主要是用作系统开 相似文献
3.
4.
MPLS流量工程及其形式化研究 总被引:1,自引:0,他引:1
MPLS被认为是下一代IP骨干网络技术,而流量工程是合理使用网络资源保障QoS的关键.支持MPLS的路由器可以使用新的机制实现流量工程,通过在线或离线的算法计算LSP确保QoS.在综述了MPLS应用于流量工程的优势、QoS路由、接纳控制、重新路由、容量设计和部署等问题及其形式化研究等方面的最新工作的基础上,对几种MPLS QoS路由的算法进行了对比和总结,并分析了进一步的研究方向和问题. 相似文献
5.
6.
在机器人迅速发展的时代,人机协作型机器人安全性问题是人们关注的焦点.机器人逆运动学的建模与求解是决定其安全性的必要因素之一.旋量法是一种机器人逆运动学建模的常用方法,它可以解决传统D-H参数法的奇异性问题.然而,在建模过程中,旋量法会因人为因素或软件系统缺陷导致模型出现漏洞,从而威胁操作人员安全.因此,本文在旋量高阶逻... 相似文献
7.
8.
嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的困难。其根本性难点在于缺少一种系统化的工程方法来引导工业界软件实践者,从原始需求开始最终完成形式化需求规约,并能确认该规约真实、充分地反映了人们对软件期望的功能。针对上述挑战,提出了一种面向机载控制软件需求建模的形式化工程方法ACSDL-MV,以形式化方法为理论基础,结合软件需求工程的基本原理,引导工程人员从原始需求出发以演化式的过程逐步完成需求规约的构建;定制了航空控制软件的形式化描述语言ACSDL,用以构建形式化规约;为了确认软件需求规约准确、充分地描述了人们对软件期望的功能,该方法给出了基于图形的静态审查和基于模型的动态模拟技术。在航空发动机公司中的实验结果表明,该方法相比传统方法探测到了更多的潜在错误。 相似文献
9.
10.
关键软件要求极高的可靠性和安全性,然而当前的技术途径尚不能完全消除软件故障——软件测试不能保证软件正确性,模型检查等形式化验证技术也存在着诸多局限。文章提出了基于监控程序运行途径来捕获软件故障和验证程序性质正确性,构建了基于程序运行形式化分析的软件故障监控(SFMRFA)模型,在监控逻辑表达、程序插桩、multi-agent设计等关键技术的基础上开发计算机辅助工具来监控、分析和引导程序执行,使软件运行当中可测、可控,避免软件失效。 相似文献
11.
李梦君 《计算机工程与科学》2016,38(Z1):143-145
形式化软件工程是软件工程的重要组成部分。Event-B方法是一种软件形式化开发方法,Rodin是支持Event-B方法的开放工具集。基于Event-B方法和Rodin开展形式化软件工程教学,有益于学生正确理解精化等重要的软件工程概念,理解并掌握开发可信软件的方法,是软件工程教学的重要补充。 相似文献
12.
Shimba is a reverse engineering environment to support the understanding of Java software systems. Shimba integrates the Rigi and SCED tools to analyze and visualize the static and dynamic aspects of a subject system. The static software artifacts and their dependencies are extracted from Java byte code and viewed as directed graphs using the Rigi reverse engineering environment. The run‐time information is generated by running the target software under a customized SDK debugger. The generated information is viewed as sequence diagrams using the SCED tool. In SCED, statechart diagrams can be synthesized automatically from sequence diagrams, allowing the user to investigate the overall run‐time behavior of objects in the target system. Shimba provides facilities to manage the different diagrams and to trace artifacts and relations across views. In Shimba, SCED sequence diagrams are used to slice the static dependency graphs produced by Rigi. In turn, Rigi graphs are used to guide the generation of SCED sequence diagrams and to raise their level of abstraction. We show how the information exchange among the views enables goal‐driven reverse engineering tasks and aids the overall understanding of the target software system. The FUJABA software system serves as a case study to illustrate and validate the Shimba reverse engineering environment. Copyright © 2001 John Wiley & Sons, Ltd. 相似文献
13.
Anthony C Davies 《Microprocessors and Microsystems》1988,12(10):547-553
The potential benefits of using formal methods in the design of software are discussed. Concepts are illustrated by several small examples, with the objective of helping to bridge the gap between theory and practice. The paper introduces and explains some of the terminology, symbols and notation for the discrete mathematics used in the formal methods literature, intended to assist the reader in further study. 相似文献
14.
The advantage of COOZ(Complete Object-Oriented Z) is to specify large scale software,but it does not support refinement calculus.Thus its application is comfined for software development.Including refinement calculus into COOZ overcomes its disadvantage during design and implementation.The separation between the design and implementation for structure and notation is removed as well .Then the software can be developed smoothly in the same frame.The combination of COOZ and refinement calculus can build object-oriented frame,in which the specification in COOZ is refined stepwise to code by calculus.In this paper,the development model is established.which is based on COOZ and refinement calculus.Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement,since data refinement usually has to be done on a large program component at once.As to the implementation technology of refinement calculus,the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered. 相似文献
15.
逆向工程发展现状研究 总被引:7,自引:1,他引:6
随着软件产业的发展,越来越多的遗产系统需要维护和改善,逆向工程已经成为遗产系统维护与演化的关键技术之一。介绍了逆向工程的定义,综述了逆向工程的研究进展。通过对现有工具的分析探讨了逆向工程研究中的不足之处,给出了未来的发展趋势。 相似文献
16.
17.
针对逆向工程中曲面数字化与模型重建的信息交互方式单一,一些对后续建模有用的辅助信息(隐式信息)流失(目前的数据文档格式无法保存与传递),造成后续模型重建困难的问题,提出一种基于语义的测量信息传递方法,分析测量过程中有利于模型重建的隐式信息,建立语义信息模型,采用类IGES数据格式存储语义信息,阐述语义信息的封装、解析方法以及基于语义的数据预处理、模型重建过程。实验研究表明,基于语义的测量信息传递方法能够有效提高CAD模型重建效率。 相似文献
18.
Integrated reverse engineering and rapid prototyping 总被引:16,自引:0,他引:16
Reverse engineering is a methodology for constructing CAD models of physical parts by digitizing an existing part, creating a computer model and then using it to manufacture the component. When a digitized part is to be manufactured by means of rapid prototyping machines such as stereolithography apparatus (SLA) and selective laser sintering equipments (SLS), etc., it is not necessary to construct the CAD model of a digitized part. This will be described by the proposed novel method which can construct STL file (the de facto file format for rapid prototyping machines) directly from digitized part data. Further more, the STL file can even be constructed in a way that significant data reduction can be achieved at the users' discretion. 相似文献