|
高安全系统的软件开发与验证技术工信部重点实验室
Key Laboratory for Safety-critical Software Development and Verification (Nanjing University of Aeronautics and Astronautics), Ministry of Industry and Information Technology |
|
主要从四个研究领域分别阐述高安全软件目前国内外技术进展和发展趋势。 领域1:高安全软件功能安全与信息安全基础的最新进展及发展趋势 在高安全软件功能安全与信息安全基础方面,欧美等发达国家一直致力于对高安全软件的功能安全需求分析基础、高安全软件的功能安全形式化验证方法以及高安全软件信息安全基础的研究。 在对高安全软件系统的功能安全需求分析方面,意大利的布鲁诺研究中心分析了典型系统需求的故障和失效模式,提出了扩展系统安全性需求模型的方法,并采用符号化模型检测进行故障分析。通过对扩展的需求模型所描述的系统状态空间的分析,提取导致安全属性失效的缺陷故障组合。相对于手工分析而言,这样的方法能够给出更加准确和完备的结果,提供安全关键软件系统更形式化的分析保障。但这种方法不支持层次化的安全需求模型,无法对复杂功能交互和约束行为进行有效分析。美国柯林斯公司高级技术中心与明尼苏达大学提出了针对安全关键软件系统中缺陷故障的传播进行需求建模的方法,通过追踪对象的可能故障源来提取软件系统的错误模型实例,然后将其存储在有向图里,对系统错误进行静态有向图分析。同时,根据形式化语义实现对系统需求模型进行严格分析,但目前仅仅提出了采用模型检测进行自动分析的思想,未提供具体的方法。法国波尔多第一大学的研究人员提出可用于对安全关键软件系统的功能以及失效模式进行描述的需求建模方法,并且得到了法国航空和航天工业界的支持和应用。该方法以节点的形式定义软件系统的功能构件层次,每个节点具备相应的数据流、状态、事件和迁移关系。安全性失效可定义为对节点状态的影响,相应的行为则通过与特定事件相关的迁移关系来描述。但该方法目前主要局限于对非时序的安全性需求分析,同时,其内部分析算法也只是对系统动态行为的有界搜索,可能导致分析结果的不完整性。 由此可见,对复杂安全关键软件系统进行需求失效分析研究,建立系统化的需求模型,并采用形式化方法进行严格的安全性需求分析是安全关键软件系统研究领域的一个重要发展趋势。而模型检测作为一种对并发系统的时序属性进行自动形式化分析的成熟技术,安全性需求分析的研究在国际上正越来越引起重视,并逐渐在航空等安全关键领域得到应用。国内虽然有采用模型进行安全性分析的工作, 但针对安全关键领域并采用形式化方法进行软件系统需求失效模式、需求模型和分析的研究尚未展开。 大量研究表明,在大型系统软件开发过程中,大部分错误都是在需求和软件设计阶段引入的,而错误在系统中存在的时间越长则越难发现,解决这些错误的代价也就越高。因此提高软件规格说明的质量是提高整个软件开发质量的关键。形式化方法是解决此问题的一个重要技术。所谓形式化方法是对系统建立数学模型,研究和提供一种基于数学的或形式语义学的规格说明语言,用这种语言严格地描述所开发的软件功能,并由自动程序设计的加工模型来得到可执行的代码。形式化方法包含形式化建模技术和形式化验证技术。 软件形式化描述一直以来是计算机界的一个研究热点。目前已有不少这方面的研究成果,如Hoare的程序逻辑、Pnueli的时序逻辑、Hoare的CSP、Milner的CCS及Pi演算、Petri网、I/O自动机、实时自动机、UML、Z语言、VDM、B和Event-B方法等。其中Hoare的程序逻辑、Pnueli的时序逻辑等是采用逻辑方法刻画程序的规范(需求描述),CSP、CCS、Pi演算、Petri网、I/O自动机、实时自动机、UML、AADL等采用类似于自动机的方式刻画程序的规范,Z语言、VDM、B和Event-B方法等采用逻辑公式与集合论结合的方式刻画程序的规范。这些系统从各种不同角度给出了软件的形式化描述。 国内从事形式化建模技术和形式化验证技术的主要有清华大学、中科院软件所、上海交通大学、南京大学、华东师范大学、国防科大、北京大学、北京航空航天大学、西安电子科技大学等高校。 为应对日益严峻的高安全软件系统中的信息泄露与数据安全保护问题,欧美日等发达国家一直致力于对高安全软件中信息安全的研究,重点突破了外包数据安全、物联网安全等科学技术领域内多项关键技术。斯坦福大学Dan Boneh教授研究组深入研究了双线性对和多线性映射的安全性质和运行方式,并基于它们提出了一系列外包数据安全的解决机制。美国UCLA的Amit Sahai教授和德克萨斯大学的Brent Waters提出了函数加密(Functional Encryption)的安全框架,从而实现了外包数据的精细化访问控制。普渡大学Elisa Bertino教授研究组通过改进的数据可靠度和节点声誉评估机制,实现了物联网环境下抗合谋攻击的安全数据聚合协议。 国内中科院软件研究所的冯登国教授研究组也深入分析了外包大数据的隐私性、可信性及访问控制问题。西安电子科技大学李晖教授研究组则研究了适用于大规模网络的轻量级安全机制,实现安全高效的大规模数据分析。清华大学、武汉大学、上海交通大学、信息安全国家重点实验室等也对高安全软件中的信息安全问题进行了一定的研究。 领域2:高安全软件设计与开发方法的最新进展及发展趋势 为应对高安全开放互联和网络化的发展趋势,欧美国家开始致力于对功能安全和信息安全融合的高安全软件设计与开发方法研究,重点突破融合功能安全和信息安全的一体化建模技术、功能安全与信息安全的验证与分析方法以及自动代码生成等多项关键技术。 近年来,模型驱动的设计与开发方法逐渐受到重视,并被工业界认为是切实可行的重要方法,例如航空适航认证国际标准DO-178C,增加了模型驱动开发方法扩展附件,即DO-331附件。该方法将模型作为整个系统开发过程的核心元素,在设计阶段就建立软件系统的体系结构模型,尽早进行验证和分析。同时,模型的重用以及基于模型转换的自动或半自动的逐步求精过程,都有助于降低系统开发时间和成本。 然而,目前模型驱动的设计与开发方法主要关注功能安全设计和验证,较少考虑信息安全设计,安全关键软件领域常用的建模语言有UML/SysML/UML Marte及其商业化工具Rhapsody、航空电子系统描述语言MetaH和HOOD(Hierarchical Object Oriented Design)、汽车电子系统描述语言EAST-ADL、同步语言SCADE等。 2004年,美国机动工程师协会SAE(Society of Automotive Engineers)在MetaH、UML、HOOD的基础上,提出嵌入式实时系统体系结构分析与设计语言AADL(Architecture Analysis and Design Language),并发布为SAE AS5506标准。安全关键实时系统是应用软件、运行时环境以及硬件平台深度融合的复杂系统,AADL语言与之对应地提供了软件体系结构、运行时环境以及硬件体系结构的建模概念。由于具有广阔的应用前景,AADL得到了欧美工业界,特别是航空航天领域(如Airbus, Honeywell, Boeing, Lockheed Martin, Rockwell Collins)的支持。CMU、MIT、UIUC、Pennsylvania大学、NASA以及法国IRIT、INRIA、Verimag等研究机构对AADL也展开了深入的研究和扩展。 为了在模型驱动设计与开发中加入信息安全设计,德国慕尼黑工业大学提出了UML语言的信息安全扩展UMLsec Profile。但UML使用的是多模型多分析方法,这样可能会导致UMLsec表达的信息安全模型与UML表达的功能安全模型存在信息不一致,较难对功能安全和信息安全做Trade-offs分析。 2016年,美国卡内基梅隆大学提出AADL信息安全扩展附件(Security Annex),以表达AADL构件之间的安全通信协议、加密、访问控制、资源隔离等信息。但是,AADL信息安全扩展附件还没有发布正式标准,目前也没有相关信息安全分析工具和代码生成工具。 美国范德堡大学(Vanderbilt University)在多个领域建模与分析语言(Domain Specification Modeling Languages, DSMLs)的基础上进行信息安全扩展,提出信息安全建模与分析语言SMAL(Security Model Analysis Language),SMAL是基于MILAN、SMoLES、AADL等语言的基本概念而定义的。 国内在嵌入式系统设计、模型驱动开发等相关方面有较多的研究。如北京大学、清华大学、北京航空航天大学、南京大学、国防科技大学、浙江大学、中科院、西北工业大学、华东师范大学、东北大学、中科大、电子科技大学、澳门UNU-IIST等科研院所以及航天502所、航空631所等一些国防研究所。但针对功能安全与信息安全融合的统一建模研究还较少,要最终形成成熟的应用技术,还可能需要更具创新性的研究以及大量细致的工作。 在早期阶段对软件模型进行验证和分析,能够尽早发现软件设计的潜在错误,而结合适当的形式化方法,对提安全关键关键软件的质量属性有很大帮助。 在模型驱动框架下,由于软件模型包含的特征和信息较多,一般不直接对模型进行验证和分析,而是主要采用模型转换的方式,即将软件模型(或子集)转换到另一个形式模型,或者直接转换到模型检测工具或定理证明器,目的是为了重用这些已有的验证和分析能力。例如,针对UML语言的形式化以及UML模型的验证和分析,很多学者对UML的不同子集进行了研究,分别转换到Petri网、重写逻辑Maude、Z语言、抽象状态机等形式模型,SMV、SPIN等模型检测工具,以及PVS、SAT求解机等定理证明器进行验证和分析。AADL模型则主要转换到BIP(Behavior Interaction Priority)、Fiacre、IF、动作时序逻辑TLA+、同步语言SIGNAL等模型进行验证和分析。 在考虑功能安全与信息安全相互影响的情况下,美国卡内基梅隆大学开始研究AADL体系结构模型的功能安全和信息安全Trade-offs分析。例如,如图6所示,在增加信息安全级别的情况下,使用更高安全级别的加密策略,分析体系结构模型中的构件通信延迟、构件执行时间、功耗、CPU时间、通信带宽等性质的变化情况。美国范德堡大学(Vanderbilt University)则提出基于图转换的方式,将其他建模语言的信息安全扩展模型转换到其提出的信息安全建模与分析语言SMAL,在SMAL模型上进行信息安全分析。 华东师范大学、北京航空航天大学、西北工业大学、电子科技大学、浙江大学、北京交通大学等相关院校以及航天502所、航空631所等一些国防研究所围绕AADL模型形式化验证和可靠性分析展开研究,例如西北工业大学提出了一种AADL模型可靠性分析评估工具,主要涉及AADL故障模型附件,电子科技大学将AADL模型转换到混成自动机模型,主要关注AADL模型的可调度分析。 UML方面,UModel工具支持Java、C#以及Visual Basic.Net的代码生成;Papyrus是建立在Eclipse之上的开源工具,支持UML建模以及C、C++和Java的代码生成,也支持UML Marte、East-ADL的建模和自动代码生成。Matteo Bordin等人研究了HRT-HOOD的Ada代码生成,分别给出了Protected Objects、Cyclic Objects、Sporadic Objects等语法元素到Ada的映射规则。Jonathan W.等人研究了MetaH的Ada代码生成,生成的代码由三部分组成:应用程序代码模块、标准内核模块以及硬件平台相关内核模块。和MetaH一样,AADL语言能够对应用软件、运行时环境以及硬件平台进行完整描述。因此,其生成的代码也可以分为三类:Ada、C、C++、实时Java等应用程序代码,实时中间件、虚拟机或实时操作系统的部分代码,以及硬件描述语言VHDL、Verilog的代码。例如,STOOD工具支持C、C++、Ada代码生成,还支持C、Ada代码到AADL描述的逆向工程;法国IRIT实验室研究了AADL到实时Java代码的生成,而实时Java被认为是未来航天领域的重要编程语言;Ocarina工具支持AADL模型生成运行在实时中间件PolyORB和PolyORB-HI(PolyORB High-Integrity)之上的Ada分布式应用代码;SPICES项目则研究了AADL模型到实时CORBA中间件及其之上的CCM(CORBA Component Model)应用构件生成。 与信息安全相关的代码自动生成方面,主要包括安全保障文档(Security Assurance Documents)的自动生成以及安全策略的可执行代码自动生成,但目前相关研究较少。华东师范大学、北京航空航天大学、西北工业大学、电子科技大学等相关院校以及航天502所、航空631所等一些国防研究所围绕AADL自动代码生成技术展开研究。 领域3:高安全软件智能化测试方法的最新进展及发展趋势 在高安全软件测试方法方面,国外先进国家一直致力于对信息安全漏洞及恶意软件检测、数据驱动的功能安全智能化分析以及功能安全测试与运行时验证的研究,尤其是为应对高安全软件的智能化趋势,基于数据驱动的智能分析方法得到重要关注。 安全漏洞检测技术包括基于动态扫描的技术、基于代码分析的技术、基于模糊测试(Fuzz Testing)的技术等。端口扫描是检测安全漏洞的一种经典方法,然而,该方法只能检出已知的漏洞,对于评估可能存在的未知安全性风险有较大局限。为此,人们研究了基于代码分析的安全性检测方法,这类方法的发展经历了多个阶段。上世纪末,许多漏洞检测技术研究主要关注缓冲区溢出等传统安全性问题,并以C程序等为主要研究对象。随着软件越来越复杂,新的漏洞类型不断被发现,例如整数溢出等,因此研究者提出了基于区间分析等的多种方法来检测这类漏洞。Web应用流行使得命令注入、SQL注入、跨站脚本、DDOS漏洞等得到了越来越多的关注。这类漏洞大量存在于PHP、JavaScript等脚本语言中,因此面向脚本语言的漏洞检测技术也得到了较多研究。近几年来,随着富客户端网页、移动应用等新型应用形态的崛起,越来越多的研究也开始关注这类新型应用结构。另一类检测安全漏洞的方法是进行模糊测试,通过随机篡改输入数据等来检测软件在异常输入下的安全性。然而,如何进行模糊篡改仍面临较多挑战,制约了该方法的应用范围。 在恶意漏洞检测方面,经典的方法是采用特征匹配技术。直接基于代码特征匹配的方法因恶意软件的反查杀功能越来越先进而越来越难发挥作用,因此目前更多的研究是在动态行为分析的基础上提取特征来识别恶意软件。其特征不仅包括了代码中的编码信息,API访问信息,还可能包括各类度量信息等。近年来,APT(Advanced Persistent Threat)攻击因其可能对工业系统等带来严重安全隐患,直接威胁国家安全等,而得到了越来越多关注。这类恶意软件潜伏期长,触发条件复杂,难以激发恶意特征。为此,人们还研究了一类强制执行技术,通过强迫触发某些条件来激发特殊行为,从而考察软件的安全性风险。因为能够检测隐蔽风险,该类技术也得到了越来越多的重视。 在安全漏洞及恶意软件检测领域,随着安全性问题涉及的面越来愈广泛,不仅普通应用软件,工业系统等都可能存在严重安全性风险,给研究带来了更大的难度。而且,新类型的漏洞和恶意软件形态仍不断出现,迫切需要我们不断研究新的检测方法。尽管有更多挑战需要应对,机器学习技术、强制执行技术等的发展,也为解决安全性问题提供了新的思路。我们将融合和发展新技术,以工业系统、军工软件等为突破口,研究安全性检测技术。 在软件质量分析领域,数据驱动的智能分析方法已经吸引了越来越多的研究兴趣。在软件缺陷挖掘方面,智能化分析方法大体可以分为描述型和预测型两类。描述型方法试图对正常程序需要遵循的模式进行建模,据此发现与此“正常模式”相违背的潜在软件缺陷,关联规则挖掘等是该类方法中常用的技术。预测型方法则通过对大量带有缺陷情况标注的软件模块进行学习,建立对缺陷情况的预测模型,据此判断当前模块是否包含缺陷,其中的关键技术则主要包括特征提取与选择以及分类等。在漏洞定位方面,现有技术可大致分为基于信息检索的方法和基于谱分析的方法。最近,也有少数工作综合两者进行漏洞定位。在测试用例生成方面,遗传算法则是常用技术,其针对性的设计出适应度函数,并将用例生成问题转化为数值优化问题,寻求覆盖度尽可能大的测试用例。 目前,数据驱动的软件质量分析也面临了一系列挑战,例如,软件缺陷标注过程复杂,导致标记样本稀缺;缺陷样本与正常样本比例严重失衡;软件判别性特征提取困难;漏洞难以定位等等。针对这些挑战,一些特殊的机器学习手段被越来越多的采用。比如半监督学习与主动学习技术可以有效减少对标记样本数量的需求;类别不平衡学习、代价敏感学习等技术可以缓解不同类别样本比例失衡的问题;特征选择、多模态学习等技术可以获得更为有效的特征表示等等。自70年代以来,人们对软件测试技术进行了广泛而持续的研究,取得了许多重要研究成果。在白盒测试方面,面向不同测试需求,提出了一系列测试充分性标准,并形成了围绕这些测试充分性标准的测试生成、评估、优化方法,包括数据流测试方法、变异测试方法、基于符号执行的测试用例生成方法等。在黑盒测试方面,提出了基于规约的测试方法、基于模型的测试方法、组合测试方法、模糊测试方法、蜕变测试方法等,并面向网络应用测试、GUI应用测试等,研发了一系列测试工具,大大提高了软件测试的效率。在单元测试、Web测试、回归测试等不同领域,新的测试方法和技术仍不断涌现。 美国伊利诺伊州立大学、马里兰大学、佐治亚理工学院、威斯康星大学、加州大学戴维斯分校等学术机构提出了关于白盒测试用例生成、GUI测试、回归测试、测试与故障定位、安全测试等的许多重要测试方法,引领了学术潮流。IBM、HP、Parasoft等公司研发了Rational Logiscope、Quick Test Pro、C++Test等著名测试工具,在测试工具市场处于领导地位。欧洲在软件测试领域也具有重要影响,提出了包括基于模型的测试方法、基于抽象解释的静态测试方法等许多重要测试理论和方法。英国的Micro Focus等公司研发了SilkTest、DevPartner等众多知名测试工具,覆盖了从静态测试到动态测试、测试管理的众多方面。法国以航空软件研发为背景,也研发了ASTREE等许多知名测试工具。 我国的软件测试行业近年来取得了长足进步。国内的611、301、716等工业研究所也开始研发软件测试及其辅助软件,以满足航空、航海等许多关键领域的质量保障需要。择众软件、绿盟、Testin、百度、阿里巴巴等企业也已经研发出了AutoTest等测试工具,为GUI测试、Web测试、移动应用测试提供了帮助。北京大学、南京大学、中科院、国防科技大学、北京航空航天大学等高校在软件测试理论研究方面也取得了许多有重要影响的成果。关于白盒测试方法、众包测试等的许多工作得到国际同行广泛认可。北京航空航天大学围绕嵌入式软件研发的测试工具已在国内工业界得到较为广泛的使用。 领域4:高安全软件应用研究的最新进展及发展趋势 自主可控的高安全软件需要系统软件、设计与开发环境等方面的支撑,也需要对不同关键信息领域展开典型应用研究。 在航空航天国防等领域,国产的控制、运行芯片逐渐替换国外芯片,但与之配套的开发语言编译器仍然处于缺失或初级阶段。目前,许多基于国产芯片的航空航天国防软件仍然使用机器指令进行控制编程,开发效率低、容易出错、难以保证程序的可靠性。GCC和LLVM是目前广泛使用的编译器,由于其开源、开放的特性,被大多数开源操作系统(如Linux、BSD、Mac OS X等)采纳为标准编译器。GCC和LLVM支持生成多个处理器的目标代码,为了简化对新的处理器的支持,其软件结构采用了前端/后端分离的结构,编译器前端将C语言源程序翻译成机器无关的中间代码,编译器后端将中间代码映射为对应平台的目标代码。理想情况下,为GCC/LLVM增加对一款新处理器的支持,仅仅需要修改编译器后端源代码,可以重用编译器前端的全部功能模块,从而降低了编译器的开发成本。“超大规模集成电路”重大专项中,专门支持开发了具备自主知识产权的处理器——方舟,其编译工具链基于LLVM后端移植而成。桌面计算用的CPU芯片方面,常见的通用处理器有X86、MIPS、ARM,尽管它们的指令集和指令格式不同,但是它们具备一定的共性,比如:至少32位的寻址空间、平坦的寻址方式、硬件堆栈(方便支持局部变量和递归函数调用)等特性。GCC和LLVM在通用处理器共性的基础上,设计了一套抽象的中间代码,编译器后端负责将抽象的中间代码转化为具体的目标处理器代码。但若处理器的体系结构不规则,则需要基于对编译器进行深度的个性化定制。由于航空航天国防领域国产芯片的特殊性,无法直接移植现有的GCC和LLVM,为了提高国产控制、计算芯片的开发效率,需为其开发一套自主可控、完整的编译器工具链。 工业过程控制领域包含对大量的数据进行实时采集、处理和管理的应用需求,现有实时数据处理系统在技术上主要有两类:基于文件系统的实时数据处理系统、基于传统数据库管理系统的实时数据库系统。基于文件系统的实时数据处理系统的实时性主要通过应用程序完成,导致系统开发复杂,可移植性和通用性差。实时数据库管理系统是指事务和数据都具有定时特性或显式的定时限制的数据库管理系统,既支持大量数据的共享,维护数据的一致性、完整性,又支持数据和事务的时间限制。实时数据库管理系统的理论研究起源于20世纪80年代后期,R. K. Abbott等首次提出了数据库中的事务可以具有实时限制,并提出了相关CPU和I/O调度算法、并发控制协议等。其后实时数据库技术随着应用的需求逐渐得到重视,研究了实时数据模型、实时事务处理、历史数据压缩与解压、实时SQL语言等。而且,针对工业过程控制应用领域提出了各种实时数据处理系统解决方案。目前国外实时数据处理系统主要有:OSI公司的PI,Aspen Tech公司的Infoplus.21,Honeywell公司的Uniformance(PHD),InStep公司的eDNA等。这些系统主要是基于文件系统的实时数据处理系统或基于传统数据库的实时数据库系统。此外,国外高校也研究了实时数据库管理系统的原型,主要有美国Virginia大学的BeeHive、Rhode Island大学的RTSORAC、Stanford大学的STRIP、Michigan大学的MDARTS系统等。随着国内工业界对集散控制系统(Distributed Control Systems, DCS)的大量引进和应用,国内也相继出现一些面向专用领域的商用实时数据库系统,如北京紫金桥公司的RealDB系统,浙大中控的ESP-iSYS系统,中国科学院软件研究所的Agilor系统等。此外,国内高校对实时数据库管理系统也进行了研究,主要有华中科技大学的ARTS-I、国防科技大学的KMMDB、南京航空航天大学的NHRTDB等原型系统。 目前比较典型的MBSE方法学包括IBM Telelogic的Harmony-SE方法学、国际系统工程学会的面向对象系统工程方法学(INCOSEOOSEM)、IBM Rational的系统工程方法学RUP SE、Vitech公司的基于模型的系统工程方法学(Vitech MBSE)和Dori的对象-流程方法学(Dori OPM)。而在商业领域中对MBSE理念的研究和推广中最具影响力产品则是IBM公司推出的Rhapsody工具以及一套系统工程方法——Harmony,并在国外的航空、航天、电子等领域得到了成功的应用。作为一款商业的、面向通用领域的系统工程方法,Harmony基于OMG组织提出的UML/SysML建模语言,提出基于模型驱动的系统工程,旨在规范化系统工程的活动和语言,从而保证系统设计的精确性、完整性和可验证性。 美国麻省理工大学的Nancy Leveson教授提出了基于系统论的安全性理论(STAMP: System-Theoretic Accident Modeling and Processes),构造了安全性分析工具STPA(System-Theoretic Process Analysis);英国约克大学的John McDermind教授提出了系统安全性举证(Safety Case)方法,开发了目标结构化构造符号(GSN: Goal Structuring Notation)系统。Nancy Leveson、John McDermid的研究对欧美的学术研究和工业实践都有较大影响。德国比勒费尔德大学的Peter Ladkin研究团队开发了事故分析的形式化方法(WBA:Why-Because Analysis)和基于本体论的危险分析方法(OHA:Ontological Hazard Analysis),并将此方法与安全性需求分析结合应用。美国明尼苏达大学的Mats P.E. Heimdahl研究团队研究了形式化建模语言,开发了需求状态机语言RSML和支持静态与动态需求分析的需求工程环境NIMBUS。爱荷华州立大学的Robyn R. Lutz研究团队则着重对需求工程,尤其是对关键软件产品线的安全性分析以及形式化方法进行了研究。斯坦福大学John Rushby研究团队开发了支持形式化方法的工具原型验证系PVS(Prototype Verification System),用以支持安全关键系统的开发。维吉尼亚大学的John Knight研究团队开发了形式化验证工具Echo并且研究了基于保证的开发(Assurance Based Development),以形式化的方法保证所开发软件的安全性。在美国和欧盟,航空电子系统安全性受到了极大重视。2005年2月,欧盟投资5300万欧元,启动FLYSAGE研究计划;NASA也在2000年开始进行航空安全计划(Aviation Safety Program, AVSP),着重研究:航空系统建模和监测,事故预防、避免和消除事故“复发”,事故损伤减轻、降低事故造成的危害程度。在工业实践上,产生了系列指导性标准,如ARP4754《高度综合复杂系统的审定考虑》、ARP4761《民用飞机机载系统及设备的安全性评估过程指南和方法》、DO-178B/C《机载系统和设备审定的软件考虑》、DO-254《机载电子硬件设计保证指南》、DO-160F《机载设备的环境考虑和测试程序》等。 我国也制定了在综合化航空电子系统技术安全性技术方面的参考标准,如GJB 900、GJB102、GJB142等。随着ARJ21、C919等国产大飞机型号研制,我国对航空电子系统安全性给予了极大重视,特别是民机适航问题已经成为了大型民机研制的瓶颈,对新的安全性分析验证方法需求迫切。 |
联系人:陶传奇,谢健 编码:211106 地址:江苏省南京市将军大道29号南航计算机科学技术学院 |
电话:025-84892848 传真:025-84892848 E-mail:taochuanqi@nuaa.edu.cn, xiejian_5@nuaa.edu.cn |
|||||
友情链接: | 站内文章检索: | |||||
版权所有(C)南京航空航天大学高安全系统的软件开发与验证技术工信部重点实验室 | |