面向AltaRica模型的嵌入式系统安全性验证方法

嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛,Alta Rica是一种描述安全关键系统的建模语言,同时基于Alta Rica模型的安全性分析已成为欧洲的工业标准。提出了一种面向Alta Rica模型的嵌入式系统安全性验证方法,包括:使用Alta Rica语言对嵌入式系统进行建模;给出Alta Rica模型到Promela模型的转换规则;对转换规则进行形式化证明,得到嵌入式系统的Promela模型;使用模型检验工具SPIN进行安全性验证。通过机轮刹车系统中的机轮刹车控制单元进行实例分析,验证了转换规则的正确性和有效性。     

支持SPIN验证的详细级SFMEA方法研究

随着软件系统的规模和复杂度不断增大,以软件为核心的安全关键系统的可靠性和安全性越来越难以保证。软件失效模式与影响分析SFMEA(Software Failure Modes and Effect Analysis)是军工业中常用的一种安全分析方法,其依赖人工分析、缺乏形式化语义、无法支持验证。针对SFMEA方法的不足,提出一种结合SPIN的详细级SFMEA方法,对软件失效模式进行形式化建模与分析,并结合模型检验工具SPIN进行自动化地模型检验和模拟仿真,从而提高软件系统的安全性和可靠性。该方法验证了"缓冲区数组下标越界"的这一失效模式,从而说明该方法的有效性。     

设备自动巡检控制逻辑的层级时间自动机建模与验证

地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠地运行,需对设备进行定期的自动巡检。在自动巡检的过程中,设备自动巡检控制逻辑起到了举足轻重的作用。为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(HFA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性,也未验证其正确性与可靠性。现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再利用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性。这种建模与形式化验证方法弥补了之前无时间约束的漏洞,有效确保了设备自动巡检控制逻辑的正确性与可靠性。最终,该模型通过了模拟和验证,这充分证明了设备自动巡检控制逻辑是正确可靠的。     

基于SPIN的SSL3.0握手协议模型检测

文章介绍了密钥交换协议SSL3.0协议,并利用模型检测工具SPIN对其进行了形式化分析、建模和验证。实验结果表明此验证方法的正确性,证明了协议本身的安全性与可行性,并且提高了协议的验证效率。     

基于SPIN／Promela的并发系统验证

并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一，其成功应用归功于有效验证工具的支持。SPIN是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述SPIN工作机理的基础上，详细分析了基于SPIN的系统建模语言Promela中通道操作、基本数据结构及其功能，并设计了SPIN形式化验证软件系统的基本算法，最后运用SPIN对一个并发系统实例进行验证，得出了相应验证输出图。     

一种基于场景的需求验证方法

在软件需求分析工作中,需要检验获取的需求是否同客户的需求相一致.文章提出一种基于场景的软件需求验证方法,给出了基于场景的系统模型检验验证算法,并通过一个实例对其进行了检验.该方法运用有限状态自动机对软件需求进行建模,以消息序列图描述作为验证条件的场景,对获取的需求的正确性和完备性进行验证.     

面向方面自监控软件的行为正确性验证

嵌入监控代码方法一般是在原程序中嵌入监控代码后生成自监控软件,实现安全策略对软件行为的约束,受自监控软件实现方式等具体研究方法限制,目前验证自监控软件行为符合目标安全策略的方法验证能力有限。提出一种灵活的基于面向方面编程的自监控软件实现方式,并设计了相应更全面的自监控软件行为正确性验证方法。该方法基于交替转换系统描述自监控软件的行为,使用时间交替时序逻辑定义软件行为正确的性质公式,通过给定算法在模型上检测性质公式满足与否,从而验证软件行为是否符合"安全性"、"活性"等类型监控策略,并可以分析监控代码对原程序的影响。     

基于LSC的模型检验研究

LSC是一种表达能力很强的顺序图建模语言,模型检验技术是验证软件模型正确性的重要方法,提出了一个对LSC模型进行模型检验的方法,并实现了相关支持工具。首先分析了LSC语言,然后基于其语义提出了生成LSC等价状态模型的方法,进而对生成的状态模型进行模型检验;最后进行了实例研究,利用给出的实现工具检验了用CTL描述的验证性质。     

基于SPIN的HMSC模型自动检验方法

自动检测与验证HMSC (high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义，为此提出一种为HMSC模型进行自动检验的方法，并将其实现。利用转换规则为HMSC模型生成Promela检测语言，借助SPIN工具对需求进行验证。该方法不仅支持模型检测，同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具，通过一个实例展示其自动建模检测分析的效果，表明了其有效性和实用性。     

基于程序运行形式化分析的软件故障监控技术

关键软件要求极高的可靠性和安全性,然而当前的技术途径尚不能完全消除软件故障——软件测试不能保证软件正确性,模型检查等形式化验证技术也存在着诸多局限。文章提出了基于监控程序运行途径来捕获软件故障和验证程序性质正确性,构建了基于程序运行形式化分析的软件故障监控（SFMRFA）模型,在监控逻辑表达、程序插桩、multi-agent设计等关键技术的基础上开发计算机辅助工具来监控、分析和引导程序执行,使软件运行当中可测、可控,避免软件失效。     

基于LonWorks网络和工控组态软件的地下建筑监控系统

本文主要介绍了基于LonWorks网络和工业控制组态软件开发地下建筑监控系统的实现方法。首先文章概述了一种Lonworks网络控制系统的特点,接着介绍了组态软件“组态王”,最后详细说明了Lonworks控制系统和组态软件在地下建筑控制系统中的应用。     

一个基于COP的控制软件安全性增强方法

控制软件往往是安全攸关系统的核心,其正确性对系统安全起着至关重要的作用。然而由于系统面对的环境因素越来越复杂,软件设计之初不可能考虑到所有可能面对的环境变化因素,系统的安全性面临新的挑战。因此在软件维护阶段,以环境变化为中心,增量式地增强软件的安全性显得非常重要。面向上下文编程方法(Context-Oriented Programming,COP)正是一种以软件运行上下文环境为中心的编程方法。现有的支撑COP思想的运行机制可以使得系统根据精确的上下文信息动态地调整系统的行为,但是有些上下文引发的系统行为调整会导致系统执行器的现有运行被打断,对于这类影响系统执行器行为的上下文,现有的COP运行机制还没有提供有效处理方法。根据现有的COP方法,给出了一个基于软件上下文保存与恢复的控制软件安全性增强的编程模型,并在LegoNXT控制器上实现了相应的运行支撑和编程工具,通过一个产品分拣系统的安全性增强实例,初步验证了该编程模型的合理性。     

一种基于故障扩展SysML活动图的安全性验证框架研究

随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。     

煤矿井下高压降尘供水系统监控装置的研制

根据煤矿井下高压降尘系统对供水的要求,研制了一种基于PIC18F4580单片机的井下高压降尘供水系统监控装置,介绍了该装置的硬件和软件设计。该装置可实时监测水箱水位、压力、运行状态,并可将这些保护状态信息通过CAN总线接口和转换单元并入煤矿监测监控网,实现远程监测。实验结果表明,该监控装置达到了设计要求,能保证高压降尘供水系统的实时监测与安全运行。     

软件安全核的可信性问题

软件的大量应用,使控制系统面,临严峻的安全考验,陷入了安全危机中,迫切需要新的安全保障技术。安全核就是应运而生的一种安全保障新概念,其可信性直接关系到安全核的有效性和系统的安危。面对安全核可信性问题,测试和限制安全核尺寸是当前采用的方法,它们极大地制约了安全核技术在复杂系统中的应用。本文分析了安全核可信性的本质;结合安全关键系统的基本构架,提出了从安全需求分析开始到安全核生成过程中,如何通过形式化的方法采提高安全核可信性的方法,为安全核技术在复杂系统中的应用提供了一种新思路;以交通灯控制为例全过程地实现和验证了所提出思想的正确性和可行性。     

设备驱动程序可靠性和正确性保障方法与技术研究进展

随着计算机技术的不断发展,计算机系统在安全攸关领域得到了广泛应用,其中的软件系统正逐渐成为重要的使能部件.在计算机系统中,设备驱动程序扮演了软件与硬件设备之间桥梁的角色.由于与计算机平台、操作系统、设备3个方面同时关联所导致的复杂性,设备驱动程序的开发难度大、成本高,程序中所存在的错误和缺陷常常导致系统失效,在安全攸关领域造成不可挽回的损失.以设备驱动程序可靠性和正确性保障为目标,分别从故障的隔离与恢复、正确性分析和验证、设计建模与复杂性控制这3个方面对当前相关方法和技术进行分析,为开展进一步深入的研究工作打下基础.     

基于 KingSCADA 的运动控制状态监测系统

分布式运动控制大量应用于激光装置的自动准直控制组件中,针对大型激光装置运动系统规模大、诊断要求高的特点,独立于运动控制系统之外,基于KingSCADA组态软件构建运动控制状态监测系统,实现控制对象的运行记录归档、故障查询,提升运动控制系统在线诊断分析能力;状态监测系统在大型激光装置自动准直控制组件中得到了应用,实现了电机故障的记录和查询,并通过状态监测系统的历史数据积累,为运动控制系统的智能故障诊断和预测提供了分析数据基础.     

ESpin*：基于SPIN的Eclipse模型检测环境

信息化社会中人们对软件可信性的要求越来越高,传统的测试技术已经不能充分保证系统的安全性,基于模型的形式化验证技术成为解决此类问题的重要途径。SPIN作为典型的模型检测工具,在学术界和工业界都得到了广泛应用。在Eclipse平台上设计并实现了一个基于SPIN的易扩展的模型检测环境ESpin,通过一个优化了的代码分区算法和可迅速支持SPIN升级的文法分析器,构造了一个高效、易扩充的Promela编辑器。编辑器除了支持Promela的全部语法规则外,还提供了包括实时语法反馈、关键字高亮、大纲视图、代码折叠、代码提示、代码补全在内的多种功能,提高了复杂模型的建模效率。ESpin还为用户提供了多种运行模式和特有的向导、配置界面,简化了SPIN的操作过程。     

基于SPIN内核的SDL模型检验工具设计

规格描述语言SDL目前广泛应用于复杂通信协议和软件系统的建模。使用模型检验技术对SDL进行分析和验证可以检测出模型中的逻辑错误,大大提高SDL建模结果的精确性。论文研究了SDL的形式化语义SDL/PR中常用部分与模型检验工具SPIN的输入语言Promela之间的语义映射规则,并以此为基础开发了一个基于SPIN内核的SDL模型检验器SSMC Tool。