航空机载嵌入式控制软件需求建模的形式化工程方法

嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的困难。其根本性难点在于缺少一种系统化的工程方法来引导工业界软件实践者,从原始需求开始最终完成形式化需求规约,并能确认该规约真实、充分地反映了人们对软件期望的功能。针对上述挑战,提出了一种面向机载控制软件需求建模的形式化工程方法ACSDL-MV,以形式化方法为理论基础,结合软件需求工程的基本原理,引导工程人员从原始需求出发以演化式的过程逐步完成需求规约的构建;定制了航空控制软件的形式化描述语言ACSDL,用以构建形式化规约;为了确认软件需求规约准确、充分地描述了人们对软件期望的功能,该方法给出了基于图形的静态审查和基于模型的动态模拟技术。在航空发动机公司中的实验结果表明,该方法相比传统方法探测到了更多的潜在错误。     

形式化技术应用于软件逆工程的实践研究

形式化技术为软件逆工程提供严格和完备的理论基础,但应用于实践的非常少。介绍了一种将形式化方法应用于逆工程的具体实现方法,应用最强后条件的形式化技术对命令语言进行逆工程的具体初步实践,分三阶段对源程序进行抽象以得到严格保证正确性和一致性的软件结构规格说明,并且给出了具体的实现方法。     

基于问题模式的形式化软件规格说明生成方法

精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明.     

面向构件的系统开发及其形式化

回顾了软件构件与形式化方法的基本概念,介绍了软件构件的形式化,根据典型的面向构件的开发流程和基于形式化方法开发软件的特点,提出了一个基于形式化方法的面向构件的系统开发模型.针对目前面向构件的软件开发形式,提出了一些建议和方向.     

基于RUP和VDM++的软件形式化开发方法的研究

形式化方法是软件开发过程中用于保证软件系统具有高度正确性和可靠性的一个重要手段。但形式化软件规范不直观,不容易被开发人员所接受。该文将较为直观地统一软件过程和VDM++形式化方法结合在一起,提出了一种软件形式化开发方法,并通过开发一个实际的文件设备记账系统说明了该方法的可行性与有效性。     

基于SOFL形式化方法的需求分析

介绍了形式化方法在需求分析中的运用,并且介绍了SOFL作为一种优秀的形式化工程方法的一些特点.SOFL在需求分析阶段中采用从informal到semi-formal再到formal的逐步过渡和演化,并采用CDFD进行功能分解和数据流的精确定义,有助于精确且逻辑严密地描述需求,消除需求说明文档隐含的不一致性、二义性、不完整性,从而生成高质量的形式化描述的需求文档.     

基于UML的软件形式化需求分析与验证

针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言（UML）模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。     

2008年全国软件与应用学术会议（NASAC2008）征文通知

由中国计算机学会系统软件专业委员会和软件工程专业委员会联合主办、华南理工大学软件学院承办的“2008年全国软件与应用学术会议(NASAC2008)”将于2008年11月6日至8日在广州举行.会议录用的论文将出版论文集并评选优秀学生论文,择优论文将推荐到核心学术刊物(EI检索源)发表.欢迎踊跃投稿.征文范围(但不限于下列内容)①需求工程②构件技术与软件复用③面向对象与软件Agent④软件体系结构与设计模式⑤软件开发方法及自动化⑥软件过程管理与改进⑦软件质量、测试与验证⑧软件再工程⑨软件工具与环境10○软件理论与形式化方法11○操作系统…     

双重软件体系结构描述框架XYZ/ADL

体系结构设计在软件开发过程中扮演着重要角色.工程中常用图形语言为软件体系结构建模,它们有直观、半形式化的优点;但是语义不够精确,难以对它们表示的模型进行分析,在这方面,形式化方法可与之互补.但在工程使用中仅用形式化语言建模又不太现实,所以如何结合二者之长以提高软件的可靠性已成为工业界和学术界共同关心的问题.提出了双重软件体系结构描述框架XYZ/ADL:支持工程中软件体系结构的基本概念,前端用一般的体系结构框图作为结构描述,用UML活动图、状态图作为抽象行为表示;后端用既可表示系统动态语义又可表示系统静态语义的时序逻辑语言XYZ/E作为一致的语义基础.前端的图形语言便于软件工程师的交流和使用,后端的形式语言是进一步的形式化分析验证的基础.     

PAR平台中若干软件构件形式化验证技术研究

PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。     

基于RWSL的软件再工程

为基于遗留系统特征的软件再工程提出了一种统一的方法。该方法基于一种名为RWSL广谱语言的构架。该语言具有很好的形式语义。提出了该方法从源代码到规约的体系结构和工作流，并定义了RWSL的结构。     

IMPROVED SOFTWARE MAINTENANCE MANAGEMENT

A formal procedure for managing software maintenance—from the submission of a work order through the postimplementation review—opens a window of opportunity for the IS manager who sees systems as candidates for reverse engineering, reengineering, and restructuring. This article describes a set of procedures for improving maintenance management.     

Aufwandsschätzung von Software-Reengineering-Projekten

Prediction of costs and duration of software reengineering projects Costs and duration of projects to reengineer existing software are much easier to predict than the respective figures for software development projects. Moreover, in reengineering projects costs, risks and duration are much smaller. This article presents a tool-based method to calculate the three most important reengineering project types: encapsulation projects, renovation projects, and conversion projects. The method comprises eight consecutive steps — starting from reengineering requirements and ending with risk assessments and adjustments. A set of well-known prediction methods are incorporated, among them COCOMO, component analysis, function point analysis, data point analysis, and object point analysis. The method lays particular focus on the size of the projected software as well as on its complexity and quality.     

Web-based business process reengineering

Software reengineering is not a widely accepted practice, but its methods and tools are critical to the success of business process reengineering (BPR). Reengineering software starts with an understanding of the existing system and an identification of those components that support the new business processes “as-is” and those that may have to be changed. Software reengineering would become widely used if the technology was more automated, more accessible and less complicated. Transformational reengineering encompasses available techniques for reverse engineering, reengineering and reuse, as well as the new medium of the World Wide Web (WWW). Using the WWW, the “as-is” and “to-be” designs can be made available for viewing and distribution. The author provides insight into the future of BPR and software reengineering using the WWW     

软件过程的模型化研究

由于软件开发组织不能很好地定义和管理其软件过程，以致在实际开发过程中产生诸多问题。在对传统开发过程分析的基础上构造了一个有效可行的过程模型，即生命周期分阶段、每个阶段进行多次受控迭代、工作流活动有计划进行，并根据CMM(Capability Maturity Model)标准对软件过程进行了形式化描述。最后给出了对抽象模型进行重用和剪裁再工程的一般原则，从而能根据不同需求制定合适的开发过程来指导软件开发。     

基于Java的软件再工程支持工具研究

Internet的发展和构件化的软件开发为再工程指明了新的方向。面向对象软件再工程将以构件库为中心,并关注于将遗产系统改造为B/S结构的Internet应用。论文提出了一个面向对象软件再工程模型,分析了面向对象软件再工程支持工具的特性,然后介绍了基于Java的再工程支持工具原型。     

一种面向OSGi的构件化软件再工程方法

面向服务的构件模型可以解决当前大型软件系统难于管理、维护困难和缺乏动态性等问题,而OSGi框架为基于构件系统的服务化开发提供了有力支持。把OSGi作为基础框架对遗留软件系统进行再工程,设计了OSGi化软件的总体框架,提出了软件系统构件化方法,并针对再工程过程中普遍存在的问题给出了相应的解决方案。最后,通过对Web容器再工程的实例研究,验证了面向OSGi的构件化软件再工程方法的有效性。     

软件再工程助手

随着越来越多成功的软件系统成为遗留系统,软件再工程已日益显现其重要性。但对原系统理解的难度影响了软件工程师对原系统进行再工程的效率,特别是从源代码获取设计规约。在软件维护和软件再工程中大量的工作是围绕着源代码的变换,这种变换将程序代码文本或规约文本从一种形式转变成另一种形式,从而使其具有更好的可读性和可理解性。论文介绍了作者与英国DeMontfort大学的研究人员开发的一个非常方便的用于从程序抽取规约(也就是从源代码文本到规约文本的变换)的再工程助手(RA)工具,并使用RA进行一个实例研究。     

递归子程序的依赖性分析及其应用

程序依赖性是一种重要的程序分析、理解与维护方法,广泛应用于软件工程及软件逆向工程的各个方面,但递归子程序间的依赖分析一直是依赖性分析中的难点。为此,该文提出了一种新的递归子程序间的依赖性分析方法,它首先分析子程序内部的各种依赖关系;然后,结合子程序调用图分析子程序参数间的依赖关系;最后,通过模拟递归子程序的执行过程来分析它们之间的依赖关系。利用该文提供的方法可得到比较精确的递归子程序间的依赖关系。     

Software reengineering for complex systems

Reengineering complex software is a difficult task that requires the expenditure of significant resources. To reduce associated costs and improve resultant systems, automated techniques have been developed that can be used throughout all phases of the reengineering process. Three systems are described that have been used successfully for reengineering at The Johns Hopkins University Applied Physics Laboratory. The first system automatically transforms software written in CMS-2 to software written in Ada. The second system supports database design and automated query formulation, and employs conceptual-level intermediate representations for reverse and forward engineering as well as reengineering. The final system utilizes automated techniques to reengineer critical functions for performance enhancement. The systems described are evolving, and will provide a basis for future reengineering efforts.