AADL 测试模型的构造研究

目前,结构分析和设计语言AADL在任务关键嵌入式系统领域有着良好的应用.为了保障任务关键软件的质量,文章提出基于AADL测试模型对AADL设计模型进行测试,以发现设计模型中存在的错误.研究给出了体现系统拓扑结构的AADL测试模型的形式定义及由AADL构造该测试模型的算法,基于该测试模型可以对AADL设计模型中构件交互的输入、输出端口序列和连接的正确性进行测试,并以飞行控制系统的AADL设计模型为例,阐释了研究成果.     

网格工作流研究

网格工作流是随着网格计算技术的发展而产生的一种新型协同计算技术。文中对国外的一些网格工作流的建模、体系结构和流程描述语言作了进一步的研究，介绍了网格和工作流的相关技术，然后给出了网格工作流的定义和网格工作流与传统工作流的区别，最后简要介绍了4个比较典型的网格工作流，并提出网格工作流的未来发展趋势。     

乐观嵌套工作流事务模型的形式化描述

本文对乐观嵌套工作流事务的基本概念及其规则进行形式化描述，并对乐观嵌套工作流事务的层次化、可串行性进行了讨论。最后得出结论：1）利用乐观嵌套模型来调度事务是可以串行调度的，它能够保证数据的一致性。2）在乐观嵌套工作流事务执行过程中采用多版本的数据管理机制来处理并发事务访问同一数据及其中间状态，是无联级回退的。     

一种基于大数定律的软件测试方法

随着软件规模越来越大,复杂程度越来越高,软件测试也变得越来越复杂。由于人力、经费、时间等测试资源有限,穷尽测试显然是不划算的。故需要从数量众多的可能测试数据中精心挑选出尽量少的测试数据来设计测试用例,通过这样设计的测试用例可以高效地把隐藏在软件中的错误、缺陷检测出来。文中根据历史数据和以往的经验,利用统计学中的大数定律提出了设计测试用例的“测试用例优先值向量法”。该方法的思想是当软件开发的资源、技术条件、开发过程管理等影响软件质量的因素相同时．软件产品中的各种缺陷、错误发生的概率也是基本一定的,因此,可以根据历史数据来推断出各类错误的分布情况,并由此来设计测试用例。该方法具有客观性、高效性和可复用等特点,在软件测试过程中可以节省大量的资源,提高软件测试的效率。     

业务流程管理与集成系统SynchroFLOW的软件体系结构

信息技术的快速发展和应用改变着企业的商业环境。面对市场竞争越来越激烈,如何提高系统柔性,以支持企业重组和业务流程再遣;如何集成异构系统,对原有系统资源的利用和保护。本文从业务域的角度提出了一种企业应用业务流程管理和集成系统SynchroFLOW的软件体系结构,该体系构架以企业业务需求的抽象与描述为基础,通过对企业应用业务流程、活动功能和活动参与者的信息交换机制的独立的封装,降低业务逻辑、业务数据和业务操作实体三者间的耦合,实现业务流程的柔性管理和异构环境下不同应用的功能集成。这样的系统不但具有较高的柔性和集成性,同时减轻需求确认和设计验证的难度和工作量,进而延长应用系统的生命周期。     

AADL软件容错系统建模与评估

提出了一种解决软件客错系统的可靠性评估方法,该方法基于AADL,对嵌入式软件系统进行建模,详细分析了软件系统内部各种构件的各种错误状态和其之间的错误传播,构建了AADL软件系统错误模型,并根据基本的转换规则将其转化为广义随机Petri网模型,使用现有工具对其进行了计算,从而实现了软件客错系统的可靠性评估;以航空交通控制(ATC)为应用场景进行实验.根据经验数据适当的假设了部分构件的失效率,收到了较好效果.     

一种面向AADL架构的模型测试方法

鉴于模型在软件系统开发中日趋重要的地位和AADL模型在嵌入式软件建模中的良好应用前景,为了在嵌入式软件系统开发前期保证AADL模型的质量,提出了一种基于模型测试的AADL架构验证方法;该方法应用马尔可夫链描述AADL架构的行为,然后根据得到的马尔可夫链模型以及系统设计要求标准生成相应的测试用例和测试预言,并通过测试用例执行输出和期望值的比较判断AADL模型的正确性,实现对系统AADL模型的测试;最后通过案例分析证明了该方法的有效性。     

一种面向CPS的控制应用程序协同验证方法

信息-物理融合系统是一种新型嵌入式系统计算模式,它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.本文基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求,提出了对该模型进行形式化验证的算法：基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高可验证系统的规模.另外结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.     

一种能量收集嵌入式系统自适应调度算法

能量收集嵌入式系统(energy harvesting embedded system,简称EHES)的任务调度算法需要考虑能量收集单元的能量输出、能量存储单元的能量水平和能量消耗单元的能耗.实时任务在满足能量约束的条件下,才可能满足时间约束.在这个背景下,传统固定优先级调度算法不再适用于EHES.提出一种基于分组的自适应任务调度算法,它能根据能量收集单元由于能量输出的不确定性而造成的非能量约束情况和能量约束情况,自适应地选择任务调度算法.在非能量约束的情况下,减少任务抢占次数,增强任务的可调度性;在能量约束情况下,减少电池模式切换次数,提高能量存储单元的平均能量水平,从而降低系统能量约束.在一个可进行大范围任务集合仿真的实验环境下对提出的算法进行验证,并将基于分组的自适应调度算法与现有的两个经典算法进行了对比.     

改进的局部ART测试算法研究

局部ART算法虽然克服了测试样本点与样本生成区域已测试顶点有可能距离很近的问题,但它对生成区域周围的已测试样本点对样本选择的影响考虑不足.本文针对局部ART算法的缺陷,提出了改进的局部ART算法,将生成区域周围一定范围内的已测试顶点都加入到临近已测试样本集中,在保持时间复杂度的同时,使测试样本的分布更加均匀.实验结果表明,改进的局部ART算法的错误检测能力得到了提升.