【摘 要】
：
针对嵌入式实时系统缺乏有效的软件能耗建模与分析的方法，提出一种基于进程代数的嵌入式实时系统软件能耗建模与分析的方法。通过在时间通信顺序进程上扩展价格信息得到价格时间通信顺序进程，将嵌入式实时系统指令的功耗映射成为价格时间通信顺序进程的价格，利用价格时间通信顺序进程对嵌入式实时系统软件能耗建模并进行量化分析，提出的最优路径算法可以对建模结果进行指令功耗可满足性检查并计算当前最低能耗可达路径。本方法可
【机 构】
：
江苏师范大学计算机科学与技术学院 徐州 221116 南京航空航天大学民航学院 南京 210016
【出 处】
：
第十一届全国软件与应用学术会议(NASAC2012)
论文部分内容阅读
针对嵌入式实时系统缺乏有效的软件能耗建模与分析的方法，提出一种基于进程代数的嵌入式实时系统软件能耗建模与分析的方法。通过在时间通信顺序进程上扩展价格信息得到价格时间通信顺序进程，将嵌入式实时系统指令的功耗映射成为价格时间通信顺序进程的价格，利用价格时间通信顺序进程对嵌入式实时系统软件能耗建模并进行量化分析，提出的最优路径算法可以对建模结果进行指令功耗可满足性检查并计算当前最低能耗可达路径。本方法可以从很大程度上提高嵌入式实时系统软件能耗计算和分析的准确性，计算结果有助于嵌入式实时系统软件能耗的量化分析和优化设计。
其他文献
X86 虚拟化环境逐渐成为Web 服务器重要的部署环境，该环境中虚拟机不能直接访问硬件资源，如I/O 操作等必须通过虚拟机管理软件(VMM)，因而当I/O 访问密集时会极大地增加VMM 的性能开销。本文研究了一种面向X86 虚拟化环境的Web 服务器I/O 优化方法，该方法通过在VMM 加入一种缓存机制，减少虚拟机内部网络数据包的交换次数，从而降低I/O 虚拟化的开销。实验结果表明，该方法能有效降
通常程序的不变式验证可转化为不动点求解问题,但直接计算不动点是非常困难的,故验证时态性质p 常依赖于找到合适地辅助不变式q,使之满足Reach(M)(∈)[q](∈)[p]。本文提出了两种解决方法：(1)基于抽象解释及不动点抽象定理,在抽象域中通过前向或逆向转换求解抽象不动点,并采用widening和narrowing 操作加速收敛,从而完成不变式的自动验证。(2)通过Tableau 方法构造所验
组合服务的可信性是由组件服务和业务流程共同决定的。然而组合服务需要经常进行修改演化，如何分析各种演化操作对组合服务可信性的影响是一项值得研究的课题。本文提出了一种基于可信性依赖图和控制流图的可信性影响分析模型。针对某种演化操作，首先，根据可信性依赖图可以找出所有受影响的组件服务集合；然后，根据组合服务可信性计算方法量化组件服务可信性受影响的程度；最后，结合控制流图量化对整个组合服务可信性的影响。案
针对Web服务异常处理中存在缺乏异常处理逻辑开发方法支持的问题，提出了一种基于着色Petri网描述的Web服务异常处理逻辑开发方法。该方法通过构建了一个服务层异常处理框架(EHF-S)实现对一个正常的Web服务调用响应消息进行处理，产生一个带异常处理的Web服务响应消息，其中带异常处理的响应消息是在SOAP消息中加入异常信息和WS-Addressing路由协议。首先介绍了带异常处理的SOAP消息定
基于构件层的在线演化技术能够在更新的同时不影响事务的执行和服务的状态.但是，动态更新并不容易，程序员必须考虑更新前后版本一致性和数据迁移等问题.WS-BPEL(Web Service Business Process Execution Language)是一种强大的事务流程描述语言，当意欲更新WS-BPEL刻画的系统时，我们就必须关注流程对其伙伴的调用情况.在本文中，我们基于WS-BPEL流程提
物联网是嵌入式计算机与物理设备紧密耦合的系统，在智能交通、智能医疗、智能煤矿等领域的应用日益广泛。然而，如何有效地设计出基于ZigBee技术的人员定位算法成为具有挑战性的研究课题。本文在分析国内外现有定位技术优势和缺陷的基础上，提出了一种一维环境下基于Zigbee技术的井下人员定位算法。该算法利用滤波、惯性导航等算法对计算结果进行优化，在保证定位信息实时性的同时，提高了定位精度和人员运动轨迹的真实
软件产品线由于其高效的重用性已经成为当今软件开发的趋势，越来越多的项目采用软件产品线的思想来进行开发。而在软件产品线工程中，如何利用核心资产高效的进行产品配置生成是应用工程中最重要的问题。在传统的产品配置生成过程中，由具体产品需求产生的，对核心资产的修改是一个需要手工进行、非常耗时且容易出错的重复性工作。本文针对此问题给出了一种基于面向方面技术和正交变化模型的软件产品线产品配置生成方法。本文方法将
信息化社会中人们对软件可信性的要求越来越高，传统的测试技术已经不能充分保证系统的安全性，基于模型的形式化验证技术成为解决此类问题的重要途径.SPIN作为典型的模型检测工具，在学术界和工业界都得到了广泛应用.本文在Eclipse平台上设计并实现了一个基于SPIN的易扩展的模型检测环境ESpin.环境通过一个优化了的代码分区算法和可迅速支持SPIN升级的文法分析器，构造了一个高效的、易扩充的Prome
Innovative software-intensive systems are increasingly developed in an incremental and iterative manner.The requirements engineering of such kinds of systems has become a continuous activity through s
目前有色Petri网在Web组合服务的建模和验证方面有了广泛的应用。但由于缺乏时间信息而无法对组合服务的性能进行分析。本文在Petri网研究的基础上，对有色Petri网扩展了时间信息，定义了时间有色Petri网——TCPN网。给出了基于有色Petri网的有色性对Web服务的多态性建模方法，进而可以满足对Web服务多态性的建模需求；给出了Web组合4种控制结构的基于时间有色Petri网的形式化建模方