面向SysML的系统安全性分析工具与实例研究

基于模型的安全性分析方法能够提高对目前复杂安全关键系统的建模与分析能力。系统建模语言(System Modeling Language,SysML)是一类在工业领域被广泛应用的非形式化系统功能建模语言,AltaRica是面向系统安全性分析的形式化建模语言。针对国内目前缺乏面向SysML的系统安全性分析工具的现状,设计实现了一个面向SysML的系统安全性分析工具并进行了实例研究。首先建立了SysML设计模型到AltaRica分析模型的映射规则;同时根据映射规则设计算法实现两种模型的自动转换,并集成了Altarica的分析引擎对系统模型进行自动化安全性分析;最后以SAE-AIR6110标准中的一个复杂的机轮刹车系统(Wheel Brake System,WBS)为实例,验证了所提工具的可行性和有效性。实验结果表明,对于包含25个组件类型、34个组件实例的复杂系统,该工具可有效地完成SysML模型到AltaRica模型的转换并进行正确的安全性分析。     

一种AltaRica3.0模型中类的平展化方法

AltaRica是一类面向复杂安全关键系统的建模语言,卫士转换系统(Guarded Transition System,GTS)是最新的Al-taRica 3.0的执行语义模型.AltaRica 3.0层次结构语法模型中类的平展化是将AltaRica 3.0语法模型转换为等价的平展化GTS语义模型过程中的一个重要步骤....     

面向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进行自动化地模型检验和模拟仿真,从而提高软件系统的安全性和可靠性。该方法验证了"缓冲区数组下标越界"的这一失效模式,从而说明该方法的有效性。     

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

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

一种面向SCR需求模型的形式化验证方法研究

在需求层级进行建模分析与验证是复杂安全关键软件开发过程中的核心关注点.本论文工作面向航空领域中典型安全关键软件的需求层级,提出了一种基于形式化模型检验技术的需求模型验证方法.首先分析了形式化需求模型(SCR)的建模工具(T-VEC)中所定义的递归结构形式的模型语法与语义,提出了一种对模型变量关系进行平展化的方法,将SC...     

从2.0到3.0，简化USB设计的调试和验证

USB已经成为连接个人电脑和外部设备的事实上的工业标准。USB 3．0技术的出现满足了不断增长的数据带宽需求，同时也带来了新的设计和测试的挑战。本文将重点介绍一致性测试方法以及如何获得发送端精确、可重复的测量结果。为了提供完整的测试策略，还会介绍额外的技术特征和调试技巧。     

基于模糊免疫PID控制的飞机防滞刹车研究

研究飞机防滞刹车系统优化控制问题,由于飞机防滞刹车系统存在非线性特点,影响刹车系统的稳定性和控制的性能,造成飞机的着陆安全控制的较大困难。采用传统PID(比例、积分、微分)控制的飞机刹车参数整定困难,刹车效率低下,系统的鲁棒性差,现代飞机的起降重量与速度越来越大,在刹车低速阶段存在机轮抱死打滑现象,影响降落安全。针对于此,使用模糊免疫PID控制方法,以期改善飞机刹车低速阶段性能。仿真结果表明,可以较显著的改善飞机刹车的低速阶段性能,减少刹车低速阶段机轮打滑时间,缩短刹车距离,为飞机防滞刹车优化系统的设计提供了可靠依据。     

基于AltaRica的故障自动化建模和分析

随着系统规模和复杂性的增加,系统安全性建模和分析技术在关键安全系统中得到了广泛应用.AltaRica是用于安全性分析的高级建模语言,AltaRica模型能够更好地反映系统功能和逻辑结构,消除传统安全性分析手段与系统设计的隔阂,提高安全性模型的可维护性和重用性.文章将AltaRica与计算机可视化建模技术相结合,开发了支...     

密码协议的Promela语言建模及分析

给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例,对Needham Schroeder 公钥密码协议用Promela语言建模,并利用SPIN进行了分析验证,发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析     

一种SysML模型到AADL模型的自动转换方法

安全关键系统的实现需要通过需求、设计、集成、验证和测试等多个阶段。近年来,模型驱动开发方法逐渐成为安全关键系统设计与开发的重要手段。由于还没有一个建模语言能够支持整个安全关键系统开发生命周期,因此选择集成使用2种广泛使用的标准语言:系统建模语言(SysML)和嵌入式实时系统体系结构分析与设计语言(AADL)。SysML和AADL提供了同一系统的2个不同视图,SysML模型为系统工程师提供了一个系统视图,AADL为架构设计师建立一个较低层次的设计视图,它结合了实现所有功能的硬件、操作系统和代码。提出一种SysML模型到AADL模型的自动转换方法。首先,定义SysML子集SubSysML,主要包括模块定义图(BDD)、内部模块图(IBD)、活动图(ACT)子集和从IBD和BDD扩展的AADL Profile;其次,定义SubSysML到AADL的转换规则并设计转换算法;然后,对生成的AADL初始模型进行精化;最后,使用EMF框架技术实现SubSysML到AADL的模型转换工具并通过雷达案例验证所提方法的有效性。     

利用ActionScript3.0技术构建虚拟交通系统

该文介绍了如何利用Flash CS3.0中的ActionScript3.0技术构建一种全新的虚拟交通系统,从而为人们提供更多的出行参照信息,以解决传统电子地图的一些弊端,并且具有一定程度上的实用性和可移植性。人们可以通过该虚拟交通系统获得更加直观的道路信息,从而可以更加方便准确的找到自己想要到达的地方。     

一种基于航电系统架构模型的故障树自动建模方法

航电系统作为安全关键系统,利用故障树对其进行安全性分析十分必要。然而,传统的故障树依靠手工构建,主要依赖于分析人员对系统的理解程度;同时由于安全性分析人员与系统设计人员对系统的理解不同而很难保证失效模式与系统架构的一致性。针对上述问题,提出了一种基于航电系统架构模型的故障树自动建模方法:通过向系统设计模型中添加相应的安全性属性,并嵌入高级形式化语言AltaRica中的断言机制描述故障转移过程,由此形成安全性分析模型;基于此模型利用路径追溯的方法完成故障树自动建模。以某飞机驾驶舱显示系统为案例的研究结果表明,所提出的方法能基于航电系统架构模型有效进行故障树自动建模,从而确保了故障树分析结果的完整性。     

A high-accuracy method for filling voids and its verification

A new method for filling voids is developed by improving the approach to high- accuracy surface modelling (HASM), which is based on the first fundamental coefficients and the second fundamental coefficients of surfaces. The first fundamental coefficients are used to calculate the lengths of curves, angles of tangent vectors, areas of regions and geodesics on the surface. The second fundamental coefficients reflect the local warping of the surface, namely its deviation from the tangent plane at the point under consideration, which can be observed from outside the Earth. Nine regions with different landform complexities in hilly, plateau and mountainous areas are selected for testing the performance of HASM by comparing those ones of the classic methods such as triangulated irregular network (TIN), inverse distance weighted interpolation (IDW), advanced Spline method (ANUDEM), Spline and Kriging. The results demonstrated that the HASM void filling always has the highest accuracy regardless of the landform complexity, void area and auxiliary data.     

基于项重写系统的联锁系统模型检测方法研究

模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。     

一种嵌入式操作系统运行时验证方法

作为测试、模型检验等开发阶段所用技术的有效补充,运行时验证技术越来越受到广泛的关注。然而,当前的运行时验证技术主要用于应用软件,很少专门针对操作系统进行研究。对面向嵌入式操作系统的运行时验证框架和关键技术进行了研究,并结合一个开源嵌入式操作系统FreeRTOS进行了设计与实现。首先提出了一种面向嵌入式操作系统的运行时验证和反馈调整框架,然后针对框架中的关键技术部分,完成了规约语言的设计、三值语义监控器的生成、FreeRTOS嵌入式操作系统相关接口的实现等主要工作。