嵌入式软件中一种修正QoS值的构件选择方法

CBSD(Component-Based Software Development)已经成为嵌入式软件开发的主流技术。在嵌入式环境下,有大量功能相似的构件,在开发过程中基于QoS的构件选择已成为研究热点。然而这些构件的QoS声明与提供者给出的往往并不一致。为此,提出一种基于修正QoS值的构件选择方法,该方法将QoS信任度作为权重,修正QoS值,再结合模糊逻辑,推理出该构件的综合服务能力。通过嵌入式VOD仿真实验,验证了算法的有效性,保证了构件选择的客观性和准确性。     

医院虚拟化服务器部署

随着医院信息化的发展,需要有一种更有效率的方式来调配管理服务器资源。虚拟化能使服务器的资源被更有效地利用起来。通过虚拟化的技术,能将不适宜放在同一台服务器中的应用整合于一台物理服务器中。通过虚拟化软件的调配,能将一台服务器的资源利用率最大化。虚拟化服务器还能解决由于硬件、环境不足造成的资源紧张,提高医院信息系统管理的效率。     

基于完备抽象解释的模型检验CTL公式研究

在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.     

Efficient model checking for LTL with partial order snapshots

Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. Recently, a modest extension for LTL by an operator that expresses snapshots, has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one.     

Word level bitwidth reduction for unbounded hardware model checking

In this paper we present a word-level model checking method that attempts to speed up safety property checking of industrial netlists. Our aim is to construct an algorithm that allows us to check both bounded and unbounded properties using standard bit-level model checking methods as back-end decision procedures, while incurring minimum runtime penalties for designs that are unsuited to our analysis. We do this by combining modifications of several previously known techniques into a static abstraction algorithm which is guaranteed to produce bit-level netlists that are as small or smaller than the original bitblasted designs. We evaluate our algorithm on several challenging hardware components.     

基于Python的实时嵌入式软件测试脚本

基于Python语言设计一种实时测试脚本,开发扩展模块,实现测试脚本与嵌入式软件仿真测试环境（ESSTE）的接口。该测试脚本使用简便,实时性高、描述能力强、具有良好的可复用性,目前已成功应用到ESSTE中。对多个实时嵌入式软件进行测试,结果验证了该测试脚本的正确性和实时性。     

基于Citrix的异地软件共享系统的设计与实现

针对国家科技基础条件平台中大型仪器、设备等共享的需求,提出基于思杰（Citrix）的异地软件共享解决方案,其中包括系统原理、设计与实现的描述。经过用户试用,证明该方案可行,有助于提高大型软件的利用率,减少大型软件的购买费用,符合科技基础条件平台资源共享与整合的建设原则。     

基于OPNET的AdHoc网络建模与仿真

利用OPNET软件自带的支持IEEE802．11标准的节点模型构建AdHoc网络模型。合理配置输入输出接口的参数,使网络达到最佳性能,并对网络的性能进行比较分析。仿真结果表明,网络参数之间存在关联性,网络最优化参数具有唯一性,通过网络负载与标准负载的比较,可选择出网络性能最优化状态。     

GPS软件接收机的模块设计与信号处理

采用Zarlink公司的GP2015对GPS射频前端进行下变频处理,将得到的中频模拟信号转换成数字信号,结合DSP开发技术对中频数字信号进行捕获、跟踪与定位解算,用软件无线电的方法实现GPS软件接收机的模块设计与信号处理。实验结果表明,软件无线电思想能实现算法与软件的高度灵活性,可有效提高GPS接收机的信号处理能力与系统性能。     

软件可靠性度量方法

分析软件故障暴露率与软件测试次数之间的关系,提出在保证可靠性测试结果客观准确的前提下,有效减少验证测试次数的方法。结合软件可靠性和体系结构相关理论,提出基于组件的软件失效率定量计算方法。研究并利用软件可靠性度量方法,提高了软件可靠性测试效率和可靠性评估准确性。