2014, 25(2):177-178. DOI: 10.13328/j.cnki.jos.004543 CSTR:
摘要:
2014, 25(2):179-199. DOI: 10.13328/j.cnki.jos.004529 CSTR:
摘要:实时系统时间分析的首要任务是估计程序的最坏情况执行时间(worst-case execution time,简称WCET).程序的WCET 通常受到硬件体系结构的影响,Cache则是其中最为突出的因素之一.对面向WCET计算的Cache分析研究进行了综述,介绍了经典Cache分析框架与Cache分析核心技术,并从循环结构分析、数据Cache分析、多级Cache分析、多核共享Cache分析、非LRU替换策略分析等角度介绍了Cache分析在不同维度上的研究问题与主要挑战,总结了现有技术的优缺点,展望了Cache分析研究的未来发展方向.
2014, 25(2):200-218. DOI: 10.13328/j.cnki.jos.004530 CSTR:
摘要:嵌入式软件在安全关键系统中的应用,使得保障软件安全性成为软件工程领域的研究热点之一.以典型嵌入式软件系统机载软件为基础,对机载软件安全性保障的标准、方法及工具进行综述.首先,对机载软件领域所采用的软件安全性相关的标准进行简介,并给出机载软件安全性分析框架;其次,从机载软件安全性分析框架出发,将机载软件安全性保障方法划分为3个方面,即,机载软件安全需求的提取与规约、面向标准的机载软件开发、机载软件安全需求验证.对这3个方面的现有研究工作以及工业应用进行了综述;然后,针对当前适航标准的要求对机载软件安全性保证过程中软件安全证据的收集方面的研究工作进行了总结;最后,提出机载软件安全性领域存在的挑战和未来的研究方向.
2014, 25(2):219-233. DOI: 10.13328/j.cnki.jos.004535 CSTR:
摘要:混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.
王博 , 白晓颖 , 贺飞 , XiaoyuSONG
2014, 25(2):234-253. DOI: 10.13328/j.cnki.jos.004533 CSTR:
摘要:可组合嵌入式软件以构件开发技术为基础,研究嵌入式构件的建模、组合性质、构件间组合机制以及组合验证等理论、方法和技术.从组合理论、建模与验证技术这3个方面对可组合嵌入式软件的研究现状进行调研分析.组合理论研究给出构件可组合性的乐观定义和悲观定义,从组合操作、组合规则两个方面定义构件间的组合机制.针对嵌入式构件的特点,着重调研了非功能特性和异构构件的建模与组合技术,分析了非功能特性约束、面向多特性的模型等方法.分析了基于契约的验证、基于不变量的验证、基于模型检查的验证等多种嵌入式软件组合验证技术.最后,探讨了需要进一步研究的问题.
2014, 25(2):254-266. DOI: 10.13328/j.cnki.jos.004537 CSTR:
摘要:与不断提升的计算能力相适应,移动手持设备上的存储系统结构越来越复杂,容量越来越大.这种趋势导致存储系统,主要是片上缓存和主存,在系统总能耗的占比中不断攀升.在当前手持设备多由电池驱动并且电池容量十分有限的情况下,存储系统的低功耗设计就显得十分重要.虽然现有的存储器件提供了一定的硬件节能支持,但是只有与应用程序的访存行为的规律相结合,才能充分发挥硬件的节能潜力.对现有的各种低功耗存储技术进行了梳理和总结,给出程序的访存模式的概念,归纳出访存模式在3个方面的内涵,并进一步详细介绍了程序的访存模式在片上缓存和主存低功耗技术中的应用.最后,展望未来结合访存模式进行低功耗存储系统研发的可能方向.
荣国平 , 刘天宇 , 谢明娟 , 陈婕妤 , 张贺 , 陈道蓄
2014, 25(2):267-283. DOI: 10.13328/j.cnki.jos.004539 CSTR:
摘要:伴随着计算机技术的迅速发展,嵌入式系统软件的应用领域得以不断拓宽,这使得嵌入式系统开发面临着日益严峻的质量、成本以及项目周期等方面的压力.另一方面,敏捷方法已在传统的软件项目当中得到越来越多的应用.很多研究都表明,敏捷方法在适应需求变更、提升生产效率和最终产品的质量方面都发挥出显著的作用.因此,在嵌入式系统软件开发中应用敏捷方法,自然也得到研究者和实践者的日益关注.应用系统评价(systematicreview)方法,试图尽可能系统地了解嵌入式系统开发过程中敏捷方法的应用状况和研究进展.通过对敏捷宣言提出以来12年间49篇相关文献的概况和分析,试图回答如下3 个问题:1) 在不同类型的嵌入式系统开发中,敏捷方法的总体应用情况如何? 2) 敏捷方法或实践是如何解决各类嵌入式软件开发中的挑战的? 3) 敏捷方法(实践)该如何通过扩展和改进,以更好地适应嵌入式系统开发?研究表明,尽管应用程度存在一定的差异,但敏捷方法已在不同类型的嵌入式开发中得到了应用.传统的敏捷方法也需要进行多种改变,以适应这些不同类型的嵌入式开发项目的特征.
2014, 25(2):284-297. DOI: 10.13328/j.cnki.jos.004534 CSTR:
摘要:多核处理器正越发广泛地应用到现代嵌入式系统的设计与实现当中,其强大的计算能力为将多个不同关键性级别的功能子系统集成到统一的共享资源平台提供了支持.混合关键性系统的调度问题即便在单处理器平台中都极具挑战性,在多处理器平台则更为困难.将目前资源利用率最高的单处理器混合关键性调度算法EY-VD扩展到多处理器平台中.首先,结合传统的划分调度策略提出了适用于多处理器混合关键性系统的MC-PEDF(mixedcriticality partitioned earliest deadline first)划分调度算法.尽管比之前的算法有更好的可调度性能,但传统的划分策略不能有效地平衡不同关键性级别下的负载,故其不完全适用于混合关键性系统.为了克服传统策略的不足,提出了划分调度策略OCOP(one criticality one partition).OCOP允许系统在关键性模式切换时对实时任务集进行重新划分,进而更好地平衡各个处理器在不同关键性模式中的资源利用率.基于OCOP,提出了第2种划分调度算法MC-MP-EDF(mixed-criticality multi-partitioned EDF).基于随机生成任务集的仿真实验结果表明,与MC-PEDF和已有的算法相比,MC-MP-EDF能够显著地提高系统的可调度性,尤其是在处理器数量较多的系统中.
2014, 25(2):298-313. DOI: 10.13328/j.cnki.jos.004527 CSTR:
摘要:随着硬件功能的不断丰富和软件开发环境的逐渐成熟,GPU(graphics processing unit)越来越多地被应用到通用计算领域,并对诸多计算系统(尤其是嵌入式系统)性能的显著提升起到了至关重要的作用.在基于GPU的计算系统中,大规模并行负载同时进行数据传输和加载的情况时常发生,数据传输延时在系统性能全局最优化中变得不容忽视.综合考虑负载的传输时间和执行时间,以总负载makespan最小化作为系统性能的全局优化目标,研究了GPU上负载“传输-执行”联合调度问题.首先,将负载的时间信息和并行任务数与矩形域的二维空间联系起来,建立了负载的2D双层矩形域模型;然后,将GPU上负载调度问题归结为一类Strip-Packing问题;最后,基于贪婪策略给出了近似度为3的多项式时间近似算法,算法复杂度为O(nlogn).该近似算法的核心是对数据传输阶段进行负载排序调度.这从理论层面上证明了GPU系统采取“传输-执行”两阶段调度的有效性,即,在数据传输阶段采取负载排序调度,在负载执行阶段采取先来先服务(first-come-first-serve,简称FCFS)调度,能够使GPU 性能达到全局最优或近似最优.
2014, 25(2):314-325. DOI: 10.13328/j.cnki.jos.004528] CSTR:
摘要:近年来,NAND闪存广泛应用于各类嵌入式系统.由于“异地更新”的限制,闪存中需要地址映射方法将来自文件系统的逻辑地址转换为闪存中的物理地址.随着闪存存储空间的日益增长,如何使地址映射表占用较小的内存而又不损失较多性能,成为一个重要的问题.基于需求的页级地址映射方法能够有效地解决这个问题,然而该方法会产生地址转换页操作的额外开销,影响系统性能.从基于需求的地址映射方法出发,从两方面进行优化:首先,为了减少转换页的频繁更新,提出了页级地址映射缓存技术以统一在闪存和内存中的地址映射信息的粒度;其次,设计了基于地址转换页的数据聚集技术.通过该技术,每个数据块在垃圾回收时产生的地址转换页的更新开销被降至最低.实验用一系列基准数据集并与之前代表性的工作进行比较,结果表明,优化的地址映射方法能够大量减少额外地址转换页的开销,并提高闪存存储系统的性能.
2014, 25(2):326-340. DOI: 10.13328/j.cnki.jos.004531 CSTR:
摘要:无线传感网的发展,使其需要具有高效地更新其上运行的应用软件的能力.为了解决这个问题,提出了一种面向无线传感网应用重编程的逻辑式编程语言及其处理系统ReLog.ReLog语言根据无线传感网应用的普遍特点,基于传统逻辑式语言进行扩展,并提供合适的编程抽象,方便程序员高效地构建、修改程序.同时,语言的处理系统使用中间代码将应用程序与系统软件解耦,从而减少应用更新时所需传输的更新代码的规模,提高更新效率.通过一个数据收集应用案例评估了ReLog语言及其执行机制,结果表明:使用ReLog语言能够获得简洁、易修改的程序;同时,语言的执行机制能够显著降低传输应用更新代码的能量和时间开销.
石刚 , 王生原 , 董渊 , 嵇智源 , 甘元科 , 张玲波 , 张煜承 , 王蕾 , 杨斐
2014, 25(2):341-356. DOI: 10.13328/j.cnki.jos.004542 CSTR:
摘要:同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.
2014, 25(2):357-372. DOI: 10.13328/j.cnki.jos.004532 CSTR:
摘要:为了提高程序的静态分析精度,提出了一种应用基于区域的符号化三值逻辑(region-based symbolic threevaluedlogic,简称RSTVL)的静态分析方法.RSTVL能够描述C程序运行时内存中数据结构的形态信息与变量的存储状态,以及可寻址表达式间的各种关系,包括指向关系、层次关系与取值逻辑关系.为了提高静态分析的精度,提出了一种基于RSTVL的流敏感、域敏感的过程内分析与基于符号化函数摘要的上下文敏感的过程间分析,能够精确地分析出每个程序点上的形态信息、数据流信息与指针指向关系.实验结果表明,相对于基于符号化三值逻辑的方法,该分析方法在保证一定分析效率的前提下,能够实现较高准确度的分析.
2014, 25(2):373-385. DOI: 10.13328/j.cnki.jos.004541 CSTR:
摘要:随着嵌入式计算机系统应用的不断扩展,嵌入式系统的可靠性引起了学术界和工业界的广泛关注,也提出了很多增进可靠性的方法和技术.然而,现有的方法和技术在测试套生成方面论述不多,所以在处理大批量嵌入式系统测试工作中遇到了挑战.讨论抽象测试套生成方法和适配技术,提出了LTS(labeled transition system)到BT(behavior tree)的转换算法,从而使TTCN(test and testing control notation)测试套可以通过转换嵌入式软件的LTS描述产生.还介绍了基于上述转换算法的嵌入式软件测试工具包,以及一个嵌入式物联网识读器测试案例研究.
张大林 , 金大海 , 宫云战 , 王前 , 董玉坤 , 张海龙
2014, 25(2):386-399. DOI: 10.13328/j.cnki.jos.004538 CSTR:
摘要:缺陷检测一般包括静态分析与人工审查两个阶段.静态检测工具报告大量缺陷,但是主要的缺陷确认工作仍由人工完成,这是一件费时、费力的工作.巨大的审查开销可能会导致软件开发人员拒绝使用该静态缺陷检测工具.提出一种可靠的基于缺陷关联的静态分析优化方法,能够分组静态检测工具所报告的缺陷,在分组后的任意一组缺陷中,如果其主导缺陷被证明是误报(或者是真实的),就能确认其他缺陷也是误报(也是真实的).实验结果表明,基于缺陷关联的静态分析优化方法在较小的时间和空间开销下减少了22%的缺陷审查工作,能够较好地适应于大型的关键嵌入式系统程序缺陷检测.
2014, 25(2):400-418. DOI: 10.13328/j.cnki.jos.004540 CSTR:
摘要:信息物理融合系统(cyber-physical system,简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用,应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先,构建了CPS软件的时间需求概念模型,提供时间需求和功能需求的基本概念,并给出了概念模型的形式化语义;然后,在模型制导下,从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义,定义了时间需求规约的一致性特性.为了支持形式化验证,将时间需求规约转换成NuSMV模型,用CTL公式表述要检测的特性,并使用NuSMV工具实施了一致性检测.
2014, 25(2):419-438. DOI: 10.13328/j.cnki.jos.004536 CSTR:
摘要:以降低分布式嵌入式系统整体能耗为目标,立足设备属性及其关系,从系统的启动设备集和设备动态供电电压两个方面着手,提出一种基于Agent的自适应能耗管理及其分析方法.在此基础上,给出分布式嵌入式能耗网(DE-Net),并利用DE-Net模型对系统的基本组件进行建模,根据组件间关系形成能耗模型,以刻画系统的执行流程和能耗属性.最后,利用CTL描述系统性质,并借助Petri网的操作语义来验证方法的正确性和有效性.具体实例应用及实验结果表明:该方法能够有效地降低分布式实时系统的能耗,正确描述能耗自适应调整过程,简化建模和分析过程,对开发具有低能耗DES具有重要的理论意义和实用价值.