俞烈彬,王立杰
(江苏自动化研究所,江苏 连云港 222061)
现代装备中大部分电子设备的关键功能由软件来完成,随着系统自动化、智能化水平的不断提高,软件规模和复杂度也不断提高,比如在F-22战机的综合航电系统中,软件实现的航电功能高达80%,软件代码达到170万余行。而在F-35战机的先进综合航电系统中,软件代码达到500万~800万行。这表明,越来越多的安全性关键系统软件日益密集化。另一方面,由软件引发的事故或事件却频发不断:如2004年12月20日,一架F-22因飞行控制软件故障而坠毁;2007年2月11日,12架F-22在穿越国际日期变更线时又因软件缺陷问题造成导航故障,战机被迫在无导航和通信能力下危险返航。由此可见,武器装备中的软件是否具备包括可靠、可用、安全等特性在内的可信特征已成为衡量和影响武器装备效能的最重要的指标,构建可信的装备软件,对抢占未来信息化战争制高点有着重要的作用。
近十年来软件的可信性研究一直受到广泛重视。美国政府的“网络与信息技术研究发展计划(NITRD)”[1]中,列出了8个重点领域,有4个与“可信软件”密切相关。美国自然科学基金会(NSF)在加州大学伯克利分校建立了科学与技术研究中心TRUST[2],其研究内容围绕可信系统的设计、构建和运行展开。国家自然科学基金的“可信软件基础研究”重大研究计划[3]是目前国内可信软件研究的主要研究计划之一,其重点支持对嵌入式软件和网络应用软件领域的软件可信性进行研究。
如果一个软件系统的行为总是与用户预期的行为和结果相一致,在受到干扰时仍能提供连续的服务,则称该软件可信[4]。目前可信软件的研究方向主要集中在软件可信性度量与评估、可信软件的构造与验证、可信软件的演化与控制等。
软件的可信性是软件提供服务时符合用户期望的能力,不仅涵盖了软件质量特性中功能性、可靠性、易用性、效率、可维护性和可移植性等,还应包括安全性、实时性、可生存性等其他特性。国外研究可信软件比较有成效的是德国达姆施塔特大学的Databases and Distributed Systems Group 的“可信计划”[5],该计划的目标是解决可信分布式系统的若干问题。他们的结论是可信是一个综合的性质,包含以下特征:端到端安全,可用性,可靠性,时效性,一致性,可预测性,可扩展性等。可信组织Trustie制定的可信规范中定义软件可信属性包括[6]:可用性(Availability),可靠性(Reliability),安全性(Security),实时性(Real Time),可维护性(Maintainability)和可生存性(Survivability)。上述每个特性又由若干子特性构成,这些属性构成了软件可信属性模型,如图1所示。
图1 软件可信属性
软件可信评估是通过分级的方式对用户的主观感受进行评价,用户根据证据描述软件对某种可信属性的满足程度。一种可信属性可能通过多个可信证据从不同的角度反映出来。一个软件所有可信证据的集合以某种结构进行组织后,就构成了软件可信证据模型。Trustie组织在文献[6]中提出了一种证据模型,将可信证据分为开发阶段证据、提交阶段证据和应用阶段证据三个部分,如图2所示。
图2 软件证据分类
软件可信评估是对软件可信属性的综合分析评估,是一个多属性决策分析[7](MADA,Multiple Attribute Decision Analysis)问题。软件评估过程如图3所示。针对MADA问题,传统的方法有字典序法、简单加性加权法、层次分析法[8]等。数学评估模型通过模糊理论将定性指标定量化,很好地解决了现有评估模型中指标单一、原始信息模糊的评估问题。由于属性权重和偏好等决策要素的不确定性,近年来,研究热点逐渐转向对模糊多属性决策问题[9](FMADM,Fuzzy Multattribute Decision Making)的研究。
图3 软件可信评估过程
可信软件构造主要分为工程化方法和形式化方法。工程化方法的核心思想是建立严格的工程规范,在软件生命周期内的各个阶段,通过规范管理和辅助工具,最大限度地减少人为错误的机会,或尽可能早地发现人为错误。但随着对软件可信性要求的提高,工程化方法渐渐不能满足高可信软件开发的要求。统计表明,传统的非形式化的软件工程技术对软件质量的保证具有一个难以逾越的鸿沟,而形式化方法是提高软件质量的重要途径。形式化方法的研究分为两类:一类是直接为以UML为代表的面向对象语言增加形式化语义,如英国的pUML组(precise UML group)就致力于运用数学知识将UML发展为一种具备精确数学语义的描述语言;另一类是通过模型转换得到模型对应的形式化语言描述。目前常用的形式化语言工具有自动机、进程代数、Petri网、逻辑学等。形式化方法研究早期,研究者一般都是手动给出系统形式化描述。模型驱动架构(MDA)[10]提出以后,基于模型驱动的可信软件构造与验证迅速成为一个研究热点,模型驱动方法可以很好地支持形式化的描述和说明,可以较为方便对软件可信需求进行抽象建模,给出形式化的归约,进行模型转换、逻辑推理。模型驱动的形式化方法如图4所示。澳大利亚昆士兰大学的Soon-Kyeong Kim等[11]采用MDA方法,通过模型转换集成形式化建模语言(Object-Z)与非形式化建模语言(UML),对于集成Object-Z和UML的建模语言,使用可重用的MDA转换框架。A.MEKKI[12]在MDA框架下完成了时间限定系统模型到时间自动机的自动转换。
图4 模型驱动的形式化方法
对于软件的可信验证,在传统软件工程中,主要通过软件可靠性测试来实现。在高可信软件工程领域,常采用形式化的验证方法。形式化验证的主要技术有模型检验和定理证明。模型检验技术[13]是通过搜索待验证软件系统模型的有穷状态空间来检验系统的行为是否具备预期性质的一种有穷状态系统自动验证技术,其过程如图5所示。RWTH Aachen University的Schlich B提出了一种基于嵌入式软件汇编码的模型检验方法[14],该方法结合了模型检验、静态分析和抽象解释等手段,同时使用一个定制的模拟器建立了状态矢量空间来控制不确定性。随着国内外对模型检验技术的深入研究,为了验证系统以及系统性质,出现了SPIN、DESIGN/CPN、UPPAAL等模型检验工具。
图5 模型检验过程
模型检验过程与模型检验技术不同,定理证明方法可以直接处理无限的状态空间。定理证明技术将软件系统和性质用逻辑方法来规约,通过基于公理和推理规则组成的形式系统,以类似数学中定理证明的方法来证明软件系统是否具备所期望的关键性质[15]。明尼苏达大学软件学院数字科技中心针对引导规则被划分为同步阶段和异步阶段的一阶规约与联合规约逻辑定义,提出了一种集中证明系统[16],集中证明方法中定理证据搜索被集中在一个交叉的、可计算的区间内,而且更具有一般推导性。我国在几何定理及其证明方面处于国际领先地位,吴文俊院士提出数学机械化证明方法推动了定理机器证明的研究[17],通过该方法可在微机上很快地证明困难的几何定理。但目前定理证明方法的效率还较低,很难用于大系统的验证。
软件的动态演化是指软件系统投入运行后,随环境和需求变化而进行的变更[18]。在开放环境下,随着软件多变性的发展,新技术与新功能的演变越来越复杂,因此必须对软件的动态行为进行监控,形成对软件动态演化中的可信性控制方法。软件行为监控和控制的基本框架如图6所示。
图6 软件行为监控和控制框架
目前研究者一般采用形式化方法进行软件行为描述,如Petri网、自动机和进程代数等。得到系统行为描述后,一般需要进行形式化验证。软件行为监控是行为可信评估的基础,为了对软件行为进行全面、准确、实时的监控,很多研究者提出了相应的软件监控方法。Diakov[19]等人提出了一种基于CORBA中间件平台的软件行为监控框架,能自动生成监测代码来监测构件之间的交互行为。Li Jun[20]提出了一个软件行为监测框架,基于全局因果跟踪技术捕获多维软件系统行为。Chen Feng[21]等人提出了一种运行时行为监测框架MOP,该框架能根据给定的行为规约自动生成监测器,动态监测系统运行行为,一旦发现违约行为,能立即触发用户定义的操作进行容错处理。为了提高软件的持续可用性和软件行为的可信性,有必要对软件行为进行控制,其主要包括异常行为控制和演化行为控制。Garlan[22]等人研究了基于运行时体系结构的自适应系统Rainbow。它采用外置运行时体系结构,通过Probe-Gauge-Consumer三层监控机制,获取和度量系统变化来触发自适应规则实现自适应演化。文献[23]也提出了一种面向体系结构的自适应系统Artennis-ARC。它采用内置运行时体系结构,通过Agent-Gauge-Monitor三层监控机制,驱动软件系统进行自适应演化。
现代装备软件大部分是以嵌入式软件的形式存在。嵌入式软件具有高复杂性的特点,同时对以实时性、可生存性、安全性为代表的高可信特征具有迫切需求,这些都对传统的软件可信技术提出了挑战。目前研究可信装备软件技术中存在的问题主要为以下三个方面。
1)可信性度量和评估:目前装备软件没有形成完整统一的可信指标体系,缺乏软件评估技术标准或规范;可信属性单独进行度量评估,没有形成正确性、可靠性、安全性等属性的综合度量空间。
2)可信软件构造与验证:模型驱动技术为可信软件构造提供了一个极好的基础架构,但是针对现代国防武器领域中复杂嵌入式软件系统的高可信需求,目前已有的模型驱动相关技术中并没有提供有效的模型精化、转换以及生成可信代码的有效方法,以及全过程连接方法;缺少异构模型语义保持和一致性理论和方法;缺少装备软件可信构造与验证的系统方法,缺少可信软件开发工具和支撑平台;模型检验应用面临的主要挑战是状态爆炸问题,必须设计可以处理大型搜索空间的算法和数据结构,因此这方面的研究主要针对模型抽象技术和系统状态空间的存储和搜索技术[24]。
3)传统软件监控需求表达能力不强,监控代码分散。没有形成开放和复杂环境下的可信软件运行监控模型和体系结构;缺乏可信软件演化的保障机制;在行为描述方面,需要建立软件可信性与软件行为之间的内在联系和严格描述;在行为监测方面,需要设计有效的收集可信性相关数据的行为监测机制;在行为可信管理方面,需要研究基于行为监测的可信评估方法,构建基于行为监测的可信管理框架;在行为控制方面,需要研究支持行为可信的软件动态演化机制。
高可信软件技术已成为国防信息技术及武器装备中嵌入式软件研发与应用过程中最为关键的核心技术。目前国内非常缺乏这方面的基础理论、实现技术以及工具的研究。我国可信软件的标准大多参考国外标准,整体落后于发达国家水平,从长远发展来看,不利于我国国防基础技术研究能力的提高和创新能力的培养。因此,为了适应武器装备的快速发展,加强和提高我国在国防领域中高可信装备软件的基础技术研究能力和创新能力,提高军工高精尖装备产品的质量,需要展开高可信相关技术的研究,构建拥有自主知识产权的装备软件可信平台,这对于减少因软件缺陷带来的巨大损失与生命伤害,以及有效保障和提升我国国防武器装备的作战效能具有极其重要的意义。
[1]网络与信息技术研究发展计划(NITRD).http:∥www.nitrd.gov
[2]TURST.http:∥www.truststc.org/
[3]刘克,单志广,王戟,等.可信软件基础研究重大研究计划综述[J].中国科学基金,2008,22(3):145-151.
[4]WANG Huai min,LIU Xu dong.etc.Software trustworthiness classification specification(TRUSTIE STCV2.0)[EB/OL],2009.
[5]T.Anderson,A.Avizienis,W.Carter,et al.Dependability:basic concepts and terminology[J].Series:Dependable Computing and Fault-Tolerant Systems,1994,5
[6]Trustie Group.A trustworthy software production environment for large scale software resource sharing and cooperativedevelopment[EB/OL].2008:http:∥ www.trustie.org.
[7]J.B.Yang,Y.M.Wang,D.L.Xu,et al.The evidential reasoning approach for MADA under both probabilistic and fuzzy uncertainties[J].European Journal of Operational Research,2006,171(1):309-343.
[8]J.B.Yang,J.Liu,J.Wang,et al.Belief rule-base inference methodology using the evidential reasoning approach-RIMER[J].Systems,Man and Cybernetics,Part A:Systems and Humans,IEEE Transactions on,2006,36(2):266-285.
[9]姚爽,郭亚军,黄玮强.基于证据距离的改进 DS/AHP多属性群决策方法[J].控制与决策,2010,25(6):894-898.
[10]OMG MDA Guide Version 1.0.1.http:∥www.omg.org/cgi-bin/doc?omg/03-06-01,retrieved at 2009.
[11]Soon-Kyeong Kim,Damian Burger,David Carrington.An MDA Approach towards Integrating Formal and Informal Modeling Languages[J].Formal Method,2005,LNCS P:448-464.
[12]A.MEKKI,M.GHAZEL.Time-constrained Systems Validation Using Mdamodel Transformation.A Railway Case Study.8th International Conference of Modeling and Simulation.May,2010:10-12.
[13]E.Clarke,K.Mcmillan,S.Campos,et al.Symbolic Model Checking[A];Proceedings of the LNCS 1102[C],1996.Springer:419-422.
[14]Schlich B.Model Checking of Software for Microcontrollers[J].ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS,2010,9(4).
[15]COOK S A.The Complexity of Theorem-Proving Procedures[A];Proc.3rdAnnu.ACM sympos.On Theory of Computing(NewYork),assoc.Comput,1971:151-158.
[16]David Baelde,Dale Miller,Zachary Snow.Focused Inductive Theorem Proving[J].Lecture Notes in Computer Science,2010,6173:278-292.
[17]吴文俊.初等几何判定问题与机械化证明[J].中国科学,1977(7):507-516.
[18]万灿军等.动态演化环境中可信软件行为监控研究与进展.计算机应用研究.2009,26(4):1201-1204.
[19]DIAKOVK.etc.Monitoring of Distributed Component Interactions.Proc of IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing.NewYork,2000:229-243.
[20]LI Jun.Monitoring and Characterization of Componentbased Systems with Global Causality Capture[C].Proc of the 23rd International Conference on Distributed Computing System,2003:422-431.
[21]CHEN Feng.etc.MOP:An Efficient and Generic Run Time Verification Framework. Proc of OOPSLA2007,2007:569-588.
[22]GARLAN D.etc.Rain-bow:Architecture-based Self-adaptation with Reusable Infrastructure.IEEE Computer,2004,37(10):46-54.
[23]徐锋,吕建,郑玮.一个软件服务协同中信任评估模型的设计[J].软件学报,2003,14(6):1043-1051.
[24]薛克.基于SPIN的UML活动图验证[D].华东师范大学,2008.