教学课程资源库 更多>>

关键词： 机动导弹系统   生存能力   概念模型   仿真评估  

摘要： 从机动导弹系统生存能力仿真需求出发,针对机动导弹系统生存能力概念建模问题进行研究。首先对机动导弹系统生存能力进行了系统分析,包括机动导弹系统的结构分析和任务目标分析。在此基础上,提出了机动导弹系统生存能力的新定义,从机动导弹系统作战全过程的角度对其生存能力概念进行了全面描述与分析,运用统一建模语言分别构建了机动导弹系统生存能力静态概念模型和动态概念模型。研究结果为机动导弹生存能力仿真评估奠定了基础。

关键词： 软件测试   面向对象测试   影响  

摘要： 为保证软件产品的质量,需要对软件过程进行控制,同时也需要对软件产品本身进行检测,在目前形式化方法和程序正确性证明还无望成为使用性方法的情况下,软件测试在将来的相当长一段时间仍然是软件质量保证的有效方法。面向对象软件的独有特性,如抽象、继承、封装、多态等,使得传统的软件测试技术不能直接应用于面向对象的软件测试。文章探讨了面向对象的测试方法,分析了面向对象的各种特征对软件测试造成的影响。

关键词： 面向对象的分析   面向对象分析   面向对象编程   编程过程   应用程序   设计标准   软件测试   软件开发   设计建  

摘要： 在面向对象的编程过程中,分析与设计问题域中出现的对象显得尤为重要。采用面向对象的分析与设计技术非常适用于目前日趋复杂的应用程序的实现。本文将针对面向对象编程中要进行的面向对象分析和设计作详细介绍,并提出一些重要的设计建议。

关键词： UML   云计算   软件建模  

摘要： 本文利用UML来构造基于云计算的机房小帮手分析与设计方法。包括使用UML用例图来做用例模型,用UML类图来做分析模型,用UML活动图和顺序图来做设计模型。

关键词： 微内核操作系统   形式化方法   模型检测  

摘要： 随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题。形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术。形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类。文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证。

关键词： 网格服务   计算网格   设计信息   资源层   异构信息   服务层   大容量存储设备   表示层   体系结构设计   业务逻辑  

摘要： 本文首先通过对网格技术和云计算的定义和特点进行分析,提出引入网格技术和云计算是数字图书档案馆建设的发展趋势,然后重点分析了数字图书档案馆网格体系中的多层架构问题及其实现设计方法,最后针对网格技术和云计算的关系,对数字图书档案馆的云计算体系结构进行了分析和初步设计。

关键词： Reverse engineering   Gene regulatory network   Formal methods  

摘要： Reverse engineering of gene regulatory relationships from genomics data is a crucial task to dissect the complex underlying regulatory mechanism occurring in a cell. From a computational point of view the reconstruction of gene regulatory networks is an undetermined problem as the large number of possible solutions is typically high in contrast to the number of available independent data points. Many possible solutions can fit the available data, explaining the data equally well, but only one of them can be the biologically true solution. Several strategies have been proposed in literature to reduce the search space and/or extend the amount of independent information. In this paper we propose a novel algorithm based on formal methods, mathematically rigorous techniques widely adopted in engineering to specify and verify complex software and hardware systems. Starting with a formal specification of gene regulatory hypotheses we are able to mathematically prove whether a time course experiment belongs or not to the formal specification, determining in fact whether a gene regulation exists or not. The method is able to detect both direction and sign (inhibition/activation) of regulations whereas most of literature methods are limited to undirected and/or unsigned relationships. We empirically evaluated the approach on experimental and synthetic datasets in terms of precision and recall. In most cases we observed high levels of accuracy outperforming the current state of art, despite the computational cost increases exponentially with the size of the network. (C) 2014 Elsevier Inc. All rights reserved.

关键词： 可执行   用例   域  

摘要： 可执行UML是UML的一个扩展,通过在UML中加入动作语言语法,使得建立的模型是可验证的.利用可执行UML与动作语言OAL,对高级运营管理系统进行建模,使得建立的模型是可执行的,可转换为任何语言.

关键词： 安全协议   BAN类逻辑   形式化方法   Otway-Rees协议  

摘要： 选取Otway-Rees协议作为研究对象,用一种改进的BAN类逻辑――安全协议分析本征逻辑(SPALL)作为协议分析工具展开研究。首先对SPALL系统进行扩展,针对Otway-Rees协议存在的缺陷,提出了改进方案。为了更好地描述改进协议,用SPALL系统对其安全属性进行了形式化描述,并做出安全分析。分析结果表明,改进协议能够确保密钥分发的正确性,并具有密钥机密性和强认证性,还能满足通信双方验证会话密钥一致性的要求。

关键词： 形式化方法   模型检测   Woo-Lam   协议   枚举法   打表法  

摘要： 形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于Promela语言,将***和***提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam协议为例,运用Spin工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。