基于有限状态机的操作系统需求层形式化验证

操作系统是航天器必备的基本软件，操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障，但仍存在不能完全排除缺陷的情况，因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分，本文在分析操作系统需求的基础上，采用有限状态机在操作系统需求层进行形式化描述，并针对应用在某航天器上的SpaceOS2在需求层进行了建模，相应地在定理证明工具Coq中进行了描述建模；然后定义了六条操作系统应满足的全局性质并进行了形式化描述，给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的，为进一步全面形式化验证奠定了基础.     

基于扩展Petri网的除冰软件安全需求建模和验证

Petri网是形式化的系统建模方法,以严格的数学基础来保证系统的正确构建,但在支持复杂软件建模和自动化验证方面存在不足.扩展了Petri网的形式语义,区别定义了状态型和数值型库所,区别定义了变迁的激发和抑制状态,引入了无前置、一元和组合判断规则,同时根据形式化定义将模型自动转换为检验程序实施安全性验证.最后给出了以上方法在典型安全关键软件-除冰系统上的应用,过程和结果表明扩展的模型和方法增强了Petri网对复杂软件系统的建模能力,提高了软件的安全性,从模型到验证代码的自动转换解决了完善模型时人工修改相应代码的工作量和因此而引入人为错误的重复工作量的问题.     

基于Event B的中断管理需求和设计形式化建模与验证方法

随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.     

基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的.     

C程序缓冲区溢出漏洞精确检测方法

C程序中的缓冲区溢出漏洞是影响系统安全性的严重问题,利用工具有效地检测并消除出这一漏洞,可以大大提高系统的安全性.针对现有工具在检测缓冲区溢出漏洞上的不足,提出了一种利用模型检测技术对C语言代码中潜在的缓冲区溢出漏洞进行精确检测的新方法.该方法首先将对缓冲区漏洞的检测转化为对程序某个位置可达性的判定,再使用模型检测工具对可达性进行验证.使用这一方法建立了一个精确检测C程序中缓冲区溢出漏洞的原型系统,并使用该原型系统进行了试验.结果表明该方法可以较为精确地检测并定位出代码中的漏洞.      

基于能力的工作流任务组织化

为解决一般工作流模型中"活动-成员"的紧耦合链,改进任务分配的柔性和适应性,提出了工作流活动和成员的能力概念.描述了能力本体模型和基于能力的任务组织化原则,建立了"活动-能力-成员"三层结构的过程元模型,给出了一系列能力匹配策略的形式化描述.上述概念和方法在开放边界工作流系统ABCflow中得到应用和验证.      

航天器测试需求描述及其自动生成

航天器作为一个典型的安全苛刻系统,其可信性研究需求迫切,支持可信性评估的数据来自于航天器测试用例的执行,而航天器测试需求是测试用例生成的重要依据.在实际应用中,对航天器这类复杂系统,面临测试需求庞杂、测试需求编制周期长、人工经验编制方式难以保证测试需求的充分性、完备性及可复用性等问题.针对这些问题,通过分析航天器组织结构特点,建立航天器形式化模型,基于航天器测试任务流程,给出了航天器静态测试需求和动态测试需求形式化描述规范,并给出航天器测试需求自动生成方法,保证了测试需求的充分性和完备性,提高了测试需求复用性,与人工编制方式相比,缩短了测试需求编制周期.最后设计并实现航天器测试需求生成应用系统,验证所提出方法的有效性.      

密码协议的分层安全需求及验证

将密码协议的安全需求分为浅层需求和深层需求2个层面,阐述了密码协议的分层安全需求.采用近世代数和时序逻辑的方法定义了形式化描述语言,并形式化地描述了密码协议的分层安全需求.将类BAN逻辑与模型检查相结合,在Abadi-Tuttle模型的基础上建立密码协议的计算模型.以Otway-Rees协议为例,利用该计算模型和定理证明技术对密码协议进行了多层需求验证.     

基于场景控制特征的安全性需求分析方法

安全性需求是系统安全性保证的关键。随着系统复杂度和耦合度的剧增,安全性需求的分析提取日益困难。通过对系统需求场景的控制结构和过程分析建模,提出描述控制过程中系统变量间关系的变量影响图模型,进一步给出了安全性需求分析方法。通过该方法,使用变量影响图等对控制过程进行分析,生成基于系统理论事故模型和过程（STAMP）的危险性控制活动,并以此获得系统安全性需求。经实验验证,所提出的安全性需求分析方法在正确性和一致性方面具有较好的效果。      

基于知识本体的资源管理平台框架设计与实现

针对大量领域信息资源缺乏有效内容分析这一问题,设计、开发了通过构建领域本体来充分发掘信息资源之间内在关系,实现信息资源增值服务的原型系统.首先构造了服装知识本体CO(Costume Ontology)用来表示服装领域知识.利用CO对被管信息资源进行语义描述,在描述数据库的基础上,实现基于语义的信息检索.讨论了服装知识本体的建模过程,本体的形式化表示以及存储方式.实验系统采用J2EE架构,开发了存储组件、语义查询接口组件、语义分析组件和语义推理组件.通过使用资源描述框架RDF,实现被管信息资源到知识本体层的映射.通过语义分析和语义推理,可以充分利用信息资源之间的关系实现相关信息资源检索与语义融合.     

基于OWL-S的测试用例生成

提出了一种基于OWL-S(OWL Web Ontology Language for Services)需求模型的测试用例自动生成方法,针对被测系统需求特性产生测试用例,以提高Web服务系统交互测试的自动化程度和效率.测试用例的生成通过3个步骤完成:①对需求特性进行分析,获取与需求特性相关的具体事件集的集合;②对OWL-S描述的应用流程进行搜索,寻找所有与需求特性相关的测试路径;③对测试路径上相关原子过程的IOPE(Inputs,Outputs,Preconditions and Effects)属性及路径条件进行分析,产生相应的测试用例.以金融行业ATM(Automated Teller Machine)示例系统为例对本方法进行了验证,结果表明本方法按要求产生了与需求特性相关的测试用例,覆盖了所有给定的需求特性公式,并有效的检测出被测系统中存在的错误.      

数字多用表自动检定系统设计

数字多用表型号多、功能多、检定项目多,每项具有多个量程,且各量程准确度不一,同一量程在不同检定点其技术指标也不尽相同,采用传统手动检定耗时耗力、误差大、错误几率高、工作效率低.在VEE Pro软件开发平台上,设计开发出一套数字多用表自动检定系统.该系统包括仪器信息记录、带接口数字多用表检定、不带接口数字多用表检定及打印输出四个模块,测试过程采用实时测试显示,自动进行数据处理并存档.使用结果表明:该系统操作简便,提高了工作效率及准确度,减小了人为误差,确保了测试数据准确可靠.     

基于本体的仿真系统全生命周期管理

建模与仿真(M&S)作为一门新兴的综合性技术,已成为继理论分析和实验实践之后第3种认识和改造客观世界的方法.首先针对M&S的需求,提出了仿真系统全生命周期管理(SSLM)的概念,进而指出SSLM作为仿真系统支撑环境的一项关键技术,能对仿真系统全生命周期中的过程和信息进行全面管理,实现目前产品全生命周期管理(PLM)尚未实现的功能.建立了基于本体的面向全生命周期三维模型,提出了基于本体论的SSLM内容管理方法,定义了面向SSLM的本体,它包括基本本体、领域本体和应用本体.在此基础上,用SSLM本体定义中的谓词构成查询语句,实现了基于语义的模型查询.      

一种集成化的卫星PCM测控与时间同步性能测试系统设计

卫星平台电子系统中遥控、遥测与时间同步性能的优劣关系到卫星安全与实用效能。针对以往平台电子系统对接采用单机自检设备,存在设备零乱、软件系统性较弱的缺点,设计开发了一套集成化的应用于卫星系统级测试的PCM测控与时间同步性能测试系统。系统具备适应不同PCM测控码率与格式要求的能力,可无缝集成功能丰富的综合测试软件,完成测控数据处理,并基于触发时间锁存原理,实现了高精度的卫星时间同步性能测试。     

一种集成化的卫星PCM测控与时间同步性能测试系统设计

卫星平台电子系统中遥控、遥测与时间同步性能的优劣关系到卫星安全与实用效能。针对以往平台电子系统对接采用单机自检设备，存在设备零乱、软件系统性较弱的缺点，设计开发了一套集成化的应用于卫星系统级测试的PCM测控与时间同步性能测试系统。系统具备适应不同PCM测控码率与格式要求的能力，可无缝集成功能丰富的综合测试软件，完成测控数据处理，并基于触发时间锁存原理，实现了高精度的卫星时间同步性能测试。     

UML在软件可靠性测试数据自动生成中的运用

为了自动生成实时嵌入式软件的可靠性测试数据,利用UML(统一建模语言)提供的建模机 制,从软件可靠性测试的角度建立use-case剖面、接口模型和测试数据实现模型,然后根 据 这些模型的描述进行随机抽样,自动生成可靠性测试数据.利用该方法能够开发出相应的测 试数据自动生成工具,在软件可靠性测试领域有着较大的实用价值.     

基于遗传算法的软件结构测试数据生成技术研究

首先介绍了软件结构测试数据生成的研究现状，然后探讨了用遗传算法解决该问题的方法和技术，在上述研究成果的基础上，已开发了一个用遗传算法实现最优搜索，生成测试数据的工具原形，初步实验表明该方法是有效的可行的。     

基于本体的软件需求缺陷模式应用

提出软件缺陷模式的概念,给出其正交属性、说明及需求缺陷模式产生模型.对领域相关需求缺陷模式进行本体描述,并着重分析其发生的直接场景.直接场景能够帮助测试人员熟悉用户的实际使用情况及现实系统的各种行为和目的,并能指导审查和测试过程.通过实例应用证明了基于需求缺陷模式直接场景进行审查和测试的有效性,并通过缺陷模式的正交属性对软件开发及测试质量进行了分析.     

可复用的需求建模方法

提出了一种特征驱动的可复用需求建模方法(RRM,Reusable RequirementMethod),此方法定义了一个可复用的需求建模过程(RRMP,Reusable Requirement Modeling Process),在领域工程和应用工程两个层面上都提出了相对完整的需求建模方法并将两个阶段有机地融合在一起.将主要研究方向着眼于领域模型的正确建立、合理剪裁和对象化过程,从而得到针对于具体应用的需求模型.在RRMP的过程指导下还将设计一个需求定制与应用开发平台(RAP,Requirement customing Application developing Platform).RAP平台立足于需求获取阶段,以用户易理解的图形化方式灵活直观地与用户进行需求交互,根据用户定制的需求自动生成具体应用的标准需求开发文档和开发过程中所产生的统一建模语言(UML,Unified Modeling Language),并最终开发出用户所需的领域内特定应用的原型系统.RAP平台主要包含3个部分:图形化需求定制工具,需求开发文档生成工具和目标应用开发工具.