基于模型的开发方法在多应用智能卡中的应用

安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的,提出了一种基于模型的开发方法学,包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求,同时明确层次化的精化策略;然后利用形式化方法建立抽象模型并对该模型进行形式化验证,在正确的抽象模型上逐层精化,并对每层模型进行验证;最后,基于满足需求的模型,进一步利用工具完成代码自动生成。该方法从抽象到具体,以逐层递增的方式明确被开发系统的需求及性质,进行形式化建模,通过反馈机制确保模型的正确性及可用性。为了证明该方法学的可行性,文章以多应用智能卡为开发实例,基于Event—B方法及Rodin平台给出了实际建模及证明的过程和结果。     

基于Event-B 方法的多应用智能卡的建模与开发

Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成。该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性。为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event-B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用。     

一个抽象机库中B方法的研究

B方法是支持规格说明到软件设计和执行的形式化方法。文章研究了B方法中一种抽象机库的实现模型和生成代码,对该方法的特点进行评述。验证了B的正确可靠的实现方法,充分利用B方法的精化原则,提高了B形式化方法的开发验证效率。     

面向嵌入式软件开发的UML到Simulink模型转换方法

模型驱动开发及其关键技术模型转换是近年来软件工程领域研究的热点。在嵌入式软件开发早期,不仅需要对设计模型进行静态分析,更需要对其进行动态仿真,验证系统设计的正确性。如何把设计模型和仿真模型无缝连接起来是工业部门亟待解决的问题。深入调研了UML和Simulink模型转换研究现状,详细分析了模型驱动开发中模型转换的相关技术,提出了一种UML到Simulink的模型转换方法,设计了UML元模型、Simulink元模型,撰写了UML元模型到Simulink元模型的映射规则。最后选取自动驾驶仪系统的飞行控制软件作为案例,验证了该方法的正确性。该方法能实现UML和Simulink两种异构模型同构化,提高嵌入式软件开发效率,丰富并且完善模型驱动开发,也为飞行控制系统、高速铁路控制、机载航电系统等嵌入式软件开发提供了技术支持。     

基于Event-B的自动化模块组合方法研究

Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用,改进PROG方法,开发自动精化工具原型。通过2个应用案例,验证了自动化组合工具能自动组合事件,自动精化工具能减少调用变量的数量,从而增强系统模型的可读性和可维护性。     

基于MDA的嵌入式软件开发平台设计

针对如何快速开发高质量的嵌入式软件的问题,实现了一种基于MDA的嵌入式软件开发平台EUP。该平台根据模型驱动的软件开发方法,集成UML建模、模型验证、模拟和自动代码生成技术等,为嵌入式软件的开发提供了一个统一的开发环境。分析了铁道交叉路口系统的实例,试验结果表明EUP平台能够方便、高效地实现模型模拟和验证,为快速开发高质量的嵌入式软件提供了一种可行的途径。     

UML类图的形式规约与精化研究

UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分。但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难。UML类图作为描述系统结构的静态模型,不具备完整的形式语义。从UML类图的机械语义中抽取出形式规约,将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义。此外,还提出了类图的结构精化操作,将模型间的精化关系在Coq中进行形式化定义,并且对精化操作的原子操作进行机械验证,保证其精化前后系统的结构和语义保持一致。将UML和形式化方法相结合,为可验证的软件设计精化框架提供了理论依据。     

T-CBESD:一个构件化嵌入式软件设计模型验证工具

现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.     

基于Event-B的可靠智能合约自动生成方法

智能合约是一种以代码的方式执行合同条款的可计算交易协议，其应用场景与规模日益增长，承载着多达数十亿美元的各类资产。由于其代码缺陷可能会造成严重的经济损失，因此智能合约的可信开发成为技术关键。为此，提出了一种基于集合论语言Event-B的智能合约可信验证与自动生成方法。Event-B方法是一种基于精化的形式化方法，可用于规约、设计和验证软件系统。通过对智能合约的模型验证和可执行代码的自动生成技术，研发了自动转换工具EB2S,打通了形式化模型和智能合约编程语言的语义鸿沟和技术壁垒。最后，选取典型的在线支付智能合约场景，应用基于Event-B的智能合约模型自动生成合约代码，验证了EB2S转换工具的有效性。     

基于CEGAR的Web应用验证

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.     

基于软件开发过程的软件缺陷管理研究

分析了软件缺陷管理的理论、方法及业务流程,指出了传统软件缺陷管理模式的不足。在此基础上提出了基于软件开发过程的软件缺陷管理模式,此模型在考虑测试者、开发者和评审者的基础上依据软件生命周期各阶段对缺陷进行了管理。最后对此管理模型的业务流程进行了详细的分析及应用,指出此管理模式很好的达到了尽早发现、预防与排除缺陷,改进软件过程的目的。     

A model for software reuse

Software reusability is widely believed to be a key to help overcome the ongoing software crisis by improving software productivity and quality. New computer technology and the demands of an advancing society require new and more complicated software. It is unrealistic to expect that every software system can be developed solely reusing existing software; however, software reusability has proven to be a way of enhancing software productivity and quality in different organizations. It is also believed that reuse of code segments alone does not significantly reduce software development effort.By creating reuse support information while software is being developed (when the software is best known to software developers), the reuse effort for both software development and maintenance can be potentially reduced.In this paper, five types of RSI are presented: Semantic Web, Horizontal Web, Vertical Web, Syntactic Web, and Alternative Web. We collectively call these five webs a Quintet Web. The Semantic Web enables software developers to locate a software segment. The Horizontal Web provides a means to reuse a block of soflware along with other types of software from other phases of a development process. The inter-phase integration of software can be performed through this Web. The Vertical Web identifies the vertical relationship of a software block to its operational environment. The Syntactic Web locates all statements in which a variable is used. The Alternative Web provides alternative software blocks that perform an identical operation.A prototype of the Quintet Web is presented.     

基于XML的软件总线设计的研究与实现

随着软件工程的不断发展,以及面向对象技术、软件组件技术和软件复用技术的开发与利用,软件总线的研究与开发已逐步成为关注的重点。软件总线也像计算机硬件总线一样,只要符合总线标准的软件组件均可以插接到软件总线上去,以实现组件的即插即用(plug-and-play)。在此,基于对软件总线技术的研究,介绍了一种基于XML的软件总线设计方案,通过使用软件总线技术开发和集成软件,不但可以大大地缩短开发周期,还可以进一步提高软件的开发效率和质量。     

软件体系结构研究与实践

软件体系结构的使用是提高软件开发质量、减少软件开销和促进软件生产率提高的最有效方法之一。对软件体系结构的研究也开始超出传统的对软件设计阶段的支持,并逐步扩展到整个软件生命周期。采用定性分析、比较研究等多种方法,阐述软件体系结构研究的基本内容及软件体系结构实践等相关内容。首先给出了软件体系结构的定义,介绍了软件体系结构风格,然后从软件生命周期的角度阐述了软件体系结构实践及相关内容,最后总结了软件体系结构的研究现状与发展趋势。     

软件体系结构研究与实践

软件体系结构的使用是提高软件开发质量、减少软件开销和促进软件生产率提高的最有效方法之一。对软件体系结构的研究也开始超出传统的对软件设计阶段的支持，并逐步扩展到整个软件生命周期。采用定性分析、比较研究等多种方法，阐述软件体系结构研究的基本内容及软件体系结构实践等相关内容。首先给出了软件体系结构的定义，介绍了软件体系结构风格，然后从软件生命周期的角度阐述了软件体系结构实践及相关内容，最后总结了软件体系结构的研究现状与发展趋势。     

软件体系结构风格研究现状及存在的问题*

针对现有软件体系结构风格定义在客观性和全面性方面存在的不足,从客观角度出发,站在软件工程的高度从多个方面对软件体系结构风格进行定义;同时通过研究分析软件体系结构风格的研究现状,发现并指出其四个重点研究方向及各自存在的问题。     

软件安全性技术在工程中的应用

载人航天工程等国家重大科技工程对软件安全性有着很高的要求.软件安全性技术在这些工程领域也在逐步得到推广应用.首先分析了软件安全性的概念,然后介绍了目前工程中主要应用的软件安全性技术,最后结合工程实际情况给出了一个软件关键等级的确定方法.     

开源平台下软件管理技术的研究*

基于开源软件平台基本特点的分析,对目前具有代表性的apt/dpkg、yum/RPM、BSD ports和portage等软件管理技术进行分析,对比和总结了现有技术特征和一般结构,探索了开源平台下软件管理技术可能的发展方向.     

Recent Progress in Software Testing, Debugging and Analysis: A Survey

This article is a survey on the recent progress of some hot topics of software engineering. The survey is based on the review on the papers of three premier conferences on software engineering from 2012 to 2013. Through the quantitative analysis on these papers, there are three hot topics identified, software testing, debugging, and analysis. Focusing on these three topics, this article summarizes some new achievements in these fields, analyzes the characteristics of these works, and points out some directions for future research.     

软件测试与软件设计方法分析

软件测试是软件工程中非常重要的一个环节,是保证软件质量的重要手段。本文从软件设计角度出发,提出如何在软件设计中就考虑易测试性,使得软件更易维护和修改,并针对软件设计和测试的现状和特点,提出提高软件易测试性和易维护性的一些建议,以达到软件复用的目的。