第４３ 卷 第１ １ 期２０２０ 年１１ 月计 算机 学 报ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳＶｏｌ．４３Ｎｏ．１ １Ｎｏｖ．２０２０一种面向安全关键软件的ＡＡＤＬ模型组合验证方法张博林ｕ杨志斌ｕ’ ２＞周 勇ｕ马燕燕ｎ黄志球＾薛 垄３＞南京航空航天大学计算机科学与技术学院 南京 ２１１ １０６）２＞（高安全系统软件开发与验证技术工信部重点实验室 南京 ２１１１０６〉３ ）（上海航天电子技术研究所 上海 ２０１１０９）摘 要 安全关键软件变得越来越复杂， 这类软件的形式化验证是一个具有挑战性的问题． 本文针对火箭发射控制子系统实例， 提出一种组合验证方法， 该方法采用组合验证与模型转换相结合的方法完成对该系统的验证与分析． 首先， 使用体系结构分析与设计语言ＡＡＤＬ对火箭发射控制子系统进行层次化构造系统的体系结构模型， 将系统各个层次的组件需求形式化为组件契约， 然后通过组合验证确保系统体系结构的正确性； 其次， 提出了ＡＡＤＬ２ＵＰＰＡＡＬ的模型转换方法， 然后基于ＵＰＰＡＡＬ对该模型中组件的功能行为进行验证与分析， 确保组件的功能行为的正确性； 最后， 实现了ＡＡＤＬ模型验证原型工具， 支持基于ＡＧＲＥＥ的体系结构模型的组合验证和支持基于ＵＰＰＡＡＬ的组件功能行为验证， 通过对火箭发射控制子系统案例的验证和分析表明本文所提方法的有效性与局限性．关键词 安全关键软件； 火箭发射控制子系统； 组合验证； ＡＡＤＬ；ＵＰＰＡＡＬ中图法分类号ＴＰ３１１ＤＯＩ号１０．１ １８９７／ＳＰ．Ｊ．１０１６． ２０２０．０２１ ３４ＡＣｏｍｐｏｓｉｔｉｏｎａｌＶｅｒｉｆｉｃａｔｉｏｎＭｅｔｈｏｄｆｏｒＡＡＤＬＭｏｄｅｌｓｏｆＳａｆｅｔｙ－ＣｒｉｔｉｃａｌＳｏｆｔｗａｒｅＺＨＡＮＧＢｏ－Ｌｉ ｎ１ １ＹＡＮＧＺＨ－Ｂｉｎ１ ，２）ＺＨＯＵＹｏｎｇ１ ＊ＭＡＹａｎ－ＹａｎｕＨＵＡＮＧＺｈｉ－Ｑｉｕ１ Ｋ２）ＸＵＥＬｅｉ３＞ｌ ）ｉ Ｃｏｌｌｅｇｅ ｏｆＣｏｍｐｕｔｅｒＳｃｉ ｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙｔＮａｎｊｉｎｇＵｎｉｖｅｒｓｉ ｔｙｏｆＡｅｒｏｎａｕｔｉ ｃｓａｎｄＡｓｔｒｏｎａｕｔｉ ｃｓｔＮａｎｊｉｎｇ２１１１０６）（． ＫｅｙＬａｂｏｒａｔｏｒｙｏｆＳｏｆｔｗａｒｅＤｅｖｅｌｏｐｍｅｎｔａｎｄＶｅｒｉｆｉｃａｔｉｏｎＴｅｃｈｎｏｌｏｇｙ Ｍｉ ｎｉｓｔｒｙｏｆＩｎｄｕｓｔｒｙａｎｄＩｎｆｏｒｍａｔｉｏｎＴｅｃｈｎｏｌｏｇｙｆｏｒＨｉ ｇｈＳｅｃｕｒｉ ｔｙＳｙｓｔｅｍｓ， Ｎａｎｊｉｎｇ２１００９３）｛ＳｈａｎｇｈａｉＡｅｒｏｓｐａｃｅＥｌｅｃｔｒｏｎｉｃＴｅｃｈｎｏｌｏｇｙＩｎｓｔｉｔｕｔｅ９Ｓｈａｎｇｈａｉ２０１１０９ ）ＡｂｓｔｒａｃｔＴｈｅｃｏｍｐｌｅｘｉｔｙｏｆｓａｆｅｔｙ－ｃｒｉｔｉｃａｌｓｏｆｔｗａｒｅｈａｓｂｅｅｎｈｉｇｈｅｒａｎｄｈｉｇｈｅｒｗｉｔｈｔｈｅｄｅｖｅｌｏｐｍｅｎｔｏｆｒｅｑｕｉｒｅｍｅｎｔｓｐｅｃｉｆｉｃａｔｉ ｏｎ．Ｔｈｅｒｅｆｏｒｅ，ｉ ｔｉ ｓａｓｅｒｉｏｕｓｃｈａｌｌｅｎｇｅｔｏｖｅｒｉ ｆｙｗｈｅｔｈｅｒｔｈｅｓｅｃｏｍｐｌｅｘｓｙｓｔｅｍｓｓａｔｉｓｆｙｅｘｐｅｃｔｅｄｐｒｏｐｅｒｔｉｅｓｏｒｎｏｔ．Ａｃｃｏｒｄｉ ｎｇｔｏｔｈｅｅｘａｍｐｌｅｏｆｔｈｅｒｏｃｋｅｔｌａｕｎｃｈｃｏｎｔｒｏｌｓｕｂｓｙｓｔｅｍ，ｔｈｉ ｓｐａｐｅｒｐｒｏｐｏｓｅｓａｃｏｍｂｉ ｎａｔｉｏｎｏｆｃｏｍｐｏｓｉｔｉｏｎａｌｖｅｒｉｆｉｃａｔｉｏｎａｎｄｍｏｄｅｌｃｈｅｃｋｉ ｎｇｔｏｃｏｍｐｌｅｔｅｔｈｅｖｅｒｉ ｆｉｃａｔｉｏｎａｎｄａｎａｌｙｓｉｓｏｆｔｈｅｓｙｓｔｅｍ．Ｆｉｒｓｔ，Ａｒｃｈｉ ｔｅｃｔｕｒｅＡｎａｌｙｓｉｓａｎｄＤｅｓｉｇｎＬａｎｇｕａｇｅ（ＡＡＤＬ）ｉｓｕｓｅｄｔｏｈｉｅｒａｒｃｈｉｃａｌｌｙｃｏｎｓｔｒｕｃｔｔｈｅａｒｃｈｉｔｅｃｔｕｒｅｍｏｄｅｌｏｆｔｈｅｒｏｃｋｅｔｌａｕｎｃｈｃｏｎｔｒｏｌｓｕｂｓｙｓｔｅｍ，ａｎｄｔｈｅｃｏｍｐｏｎｅｎｔｒｅｑｕｉｒｅｍｅｎｔｓｏｆｅａｃｈｌｅｖｅｌｏｆｔｈｅｓｙｓｔｅｍａｒｅｆｏｒｍａｌｉｚｅｄｂｙｃｏｎｔｒａｃｔｔｈｅｏｒｙ， ａｎｄｔｈｅｎｔｈｅｃｏｒｒｅｃｔｎｅｓｓｏｆｔｈｅｓｙｓｔｅｍａｒｃｈｉｔｅｃｔｕｒｅｉ ｓｖｅｒｉｆｉｅｄｔｈｒｏｕｇｈｃｏｍｐｏｓｉｔｉｏｎａｌｖｅｒｉｆｉｃａｔｉｏｎ．Ｓｅｃｏｎｄｌｙ，ｔｈｅｆｕｎｃｔｉｏｎａｌｂｅｈａｖｉｏｒｏｆｔｈｅｃｏｍｐｏｎｅｎｔｓｉ ｎｔｈｅｍｏｄｅｌａｒｅｖｅｒｉ ｆｉｅｄｂａｓｅｄｏｎＵＰＰＡＡＬｔｏｅｎｓｕｒｅｔｈｅｃｏｒｒｅｃｔｎｅｓｓｏｆＣｏｍｐｏｎｅｎｔｂｅｈａｖｉｏｒｓ；Ｆｉ ｎａｌｌｙ，ｔｈｅＡＡＤＬｍｏｄｅｌｖｅｒｉｆｉｃａｔｉｏｎｐｒｏｔｏｔｙｐｅｔｏｏｌｉｓｉｍｐｌｅｍｅｎｔｅｄｔｏｓｕｐｐｏｒｔｔｈｅｃｏｍｐｏｓｉｔｉｏｎａｌｖｅｒｉｆｉｃａｔｉｏｎｏｆＡＧＲＥＥ－ｂａｓｅｄａｒｃｈｉｔｅｃｔｕｒｅ收稿日期．．２０１９－１２－２４； 在线发布日期：２０２０￣０４－１６． 本课题得到国家自然科学基金（６１５０２２３１） 、国家重点研发计划（２０１６ＹＦＢ１０００８０２） 、ＧＦ基础科研重点项目（ＪＣＫＹ２０１６２０３Ｂ０Ｕ） 、航空科学基金（２０１９１９０５２００２）、南京航空航天大学研究生创新基地（ 实验室）开放基金（ＫＦＪＪ２０１８１６０３ ） 资助． 张傅林， 硕士研究生， 中国计算机学会（ＣＣＦ） 学生会员， 研究方向为形式化验证、 软件工程等． Ｅ－ｍａｉｌ ：ｍｌ８７５６８０１９９６＠１６３． ｃｏｍ． 杨志斌（通信作者）， 博士， 副教授， 中国计算机学会（ＣＣＦ）会员， 研究方向为安全关键软件、 形式化验钲等．Ｅ－ｍａｉｌ ：ｙａｎｇｚｈｉｂｉｎｌ６８＠１６３． ｃｏｍ． 周 勇， 博士， 副教授， 中国计算机学会（ＣＣＦ＞会员， 研究方向为软件工程、形式化方法等？ 马燕蒸， 硕士研究生， 中国计算机学会（ＣＣＦ）学生会员， 研究方向为形式化验证、软件工程等． 黄志球， 博士， 教授， 中国计箅机学会（ＣＣＦ）理事， 研究领域为软件工程、形式化方法． 薛 垒， 硕士， 髙级工程师， 研究方向为嵌人式软件验证、嵌人式软件系统设计．１１ 期张博林等：一种面向安全关键软件的ＡＡＤＬ模型组合验证方法２１３５ｍｏｄｅｌｓａｎｄＵＰＰＡＡＬ－ｂａｓｅｄｃｏｍｐｏｎｅｎｔｆｕｎｃｔｉｏｎａｌ ｂｅｈａｖｉ ｏｒｖｅｒｉ ｆｉｃａｔｉｏｎ，ｔｈｅｒｏｃｋｅｔｌａｕｎｃｈｃｏｎｔｒｏｌｓｕｂｓｙｓｔｅｍｃａｓｅｉ ｓｕｓｅｄｔｏｓｈｏｗｔｈｅｅｆｆｅｃｔｉ ｖｅｎｅｓｓａｎｄｌｉ ｍｉｔａｔｉｏｎｓｏｆｔｈｅｐｒｏｐｏｓｅｄｍｅｔｈｏｄａｒｅｄｅｍｏｎｓｔｒａｔｅｄ．Ｋｅｙｗｏｒｄｓｓａｆｅｔｙ－ｃｒｉｔｉｃａｌｓｏｆｔｗａｒｅ；ｒｏｃｋｅｔｌａｕｎｃｈｃｏｎｔｒｏｌｓｙｓｔｅｍ；ｃｏｍｐｏｓｉｔｉｏｎａｌｖｅｒｉ ｆｉｃａｔｉｏｎ；ＡＡＤＬ；ＵＰＰＡＡＬｉ 引 言安全关键软件（Ｓａｆｅｔｙ－ＣｒｉｔｉｃａｌＳｏｆｔｗａｒｅ）［１］在航天、航空、交通等领域的安全软件系统中有广泛应用， 且Ｊｒ 有高安全性的、 高可靠性的、 交互频繁的、资源受限的、实时响应的特征的软件． 安全关键软件一般为安全关键系统的关键部分， 可能引起或者增加不安全的情况， 这样的软件被认为是安全关键的［２］．近年来， 基于模型驱动开发方法Ｍ开发和设计安全关键软件越来越得到重视． 随着功能和非功能的需求的不断提高， 安全关键软件变得越来越复杂，安全关键软件的模型形式化验证面临着巨大的状态空间爆炸问题． 现在， 基于契约的组合验证方法［４ ６］成为安全关键软件领域解决验证状态空间爆炸问题的国际前沿热点． 其核心思想是利用软件系统的组合结构对验证问题进行分解， 先验证各个子组件的性质， 然后组合推理导出整个系统的性质， 通过分而治之解决状态空间爆炸问题， 这些性质用契约来形式化规约． 该方法的三个关键要素包括软件架构、 契约以及组合推理规则．基于契约的组合验证方法在程序语言、模型检测、模型驱动工程、嵌入式系统等领域都得到广泛的研究． 我们的研究是将组合验证引人到安全关键软件领域． 体系结构设计与分析语言ＡＡＤＬ［７ ８］（Ａｒｃｈｉ ｔｅｃｔｕｒｅＡｎａｌｙｓｉｓａｎｄＤｅｓｉｇｎＬａｎｇｕａｇｅ） 是由美国汽车工程师协会提出的面向安全关键系统的一种建模语言标准， 丰富的可表达方式使得ＡＡＤＬ成为安全关键软件设计与验证方法的一种重要选择，安全关键软件的ＡＡＤＬ体系结构模型组合验证方法已成为一个重要研究内容． 美国Ｒｏｃｋｗｅｌｌ Ｃｏｌ ｌｉ ｎｓ公司和Ｍｉ ｎｎｅｓｏｔａ大学在ＤＡＲＰＡＭＥＴＡＰｒｏｇｒａｍ项目的支持下， 提出了ＡＡＤＬ架构模型组合验证方法和环境ＡＧＲＥＥ？９－１１］ （ＡｓｓｕｍｅＧｕａｒａｎｔｅｅＲｅａｓｏｎｉｎｇＥｎｖｉｒｏｎｍｅｎｔ） ， 并给出了ＡＡＤＬ扩展附件ＡＧＲＥＥＡｎｎｅｘ． 使用ＡＡＤＬ构造系统的体系结构模型， 使用ＡＧＲＥＥａｎｎｅｘ构造各个组件的契约， 然后基于ＡＧＲＥＥ进行组合推理， 将基于契约的组合验证方法引人到安全关键软件领域．但是， 验证在体系结构中一层一层执行， 底层叶子组件契约被组合验证内部抽象其组件行为并默认是正确的， 所以这些组件的功能行为需要在组合验证环境外进行验证． 模型转换是ＡＡＤＬ模型形式化验证和分析的主要途径， 如转换到ＢＩＰ［１ ２］（ＢｅｈａｖｉｏｒＩｎｔｅｒａｃｔｉｏｎＰｒｉｏｒｉｔｙ）、ＦＩＡＣＲＳ１３］、ＴＬＡ＋［１４］、Ｓｉｇｎａｌ＾１ ５］、 ＳｔａｔｅｆｕｌＴｉ ｍｅｄＣＳＰ［１ ６］（ Ｃｙｂｅｒ－ＰｈｙｓｉｃａｌＳｙｓｔｅｍｓ）等， 模型转换后可以重用这些模型已有的验证和分析能力． 然而， ＵＰＰＡＡＬ［１ ７ １８］、 Ｓｉ ｍＵｌ ｉ ｎｋ［ｌ ９］等验证和分析工具在工业界已有较多使用， 这些工具常用于验证单组件的行为是否满足期望的性质即组件契约， 而组合验证环境则可以进一步基于组件契约进行整个系统的组合推理． 因此， 组合验证环境和工业界已经常用的验证和分析工具的集成是工业界的一个应用需求． 因此， 我们考虑组合验证方法ＡＧＲＥＥ和ＵＰＰＡＡＬ的结合， 并对工业界实际案例进行验证和分析．本文在已有研究工作的基础上提出了一种组合验证方法， 该方法包括ＡＡＤＬ体系结构模型的组合验证和基于ＵＰＰＡＡＬ的组件的功能行为验证． 首先， 根据需求分解构造系统的体系结构模型， 根据需求构造组件契约， 基于组件契约对系统的体系结构进行推理， 从而验证复杂系统的体系结构． 然后对组合验证中的叶子组件的功能行为模型进行模型转换， 完成了ＡＡＤＬ模型子集到ＵＰＰＡＡＬ模型的转换， 主要是针对ＡＡＤＬ子程序和行为附件的转换，然后重用ＵＰＰＡＡＬ的验证能力， 对模型的功能正确性、可达性、安全性等性质进行验证分析， 确保底层叶子组件的功能行为正确性． 通过这种组合验证与模型转换相结合的组合验证方法完成了对整个复杂ＡＡＤＬ模型的验证与分析．本文是ＭＡＣＡｅｒｏｓｐａｃｅ 项目［２。］关于ＡＡＤＬ模２１３６计 算机 学 报２０２０ 年型验证的一部分工作． ＭＡＣＡｅｒｏｓｐａｃｅ 项目是一个基于ＡＡＤＬ的建模、 验证和代码生成研究项目． 该项目提出了一种基于限定自然语言ＲＮＬＣＲｅｓｔｒｉｃｔｅｄＮａｔｕｒａｌＬａｎｇｕａｇｅ） 的需求建模方法， 从ＲＮＬ需求自动生成ＡＡＤＬ模型； 然后对ＡＡＤＬ模型精化补充其平台相关信息得到平台执行模型； 之后通过形式化验证方法完成对平台执行模型的验证与分析并将验证结果反馈给ＡＡＤＬ模型， 实现ＡＡＤＬ模型的迭代更新； 最后对验证后的模型进行目标Ｃ／Ａｄａ代码自动生成． ＭＡＣＡｅｒｏｓｐａｃｅ 项因的总体结构如图１ 所示， 本文的工作是形式化验证部分．图１ ＭＡＣＡｅｒｏｓｐａｃｅ项目总体结构２ 研究背景２． １ＡＡＤＬ语言基本概念在安全关键软件的应用中， 清晰地表达系统的各个组成部分的结构关系十分的重要． ＡＡＤＬ语言是可以描述软件体系结构、 硬件体系结构、 功能和非功能属性的建模语言． 在软件体系结构上通过线程、 线程组、 进程、 子程序、 子程序组等组件以及组件交互进行描述； 在硬件体系结构上通过处理器、虚拟处理器、 总线、 虚拟总线等组件以及组件交互进行描述； 功能和非功能属性通过分发协议、通信协议、 调度策略、 模式变换协议以及分区机制等属性进行描述； 最后， 通过系统构件的组合， 能够层次化地建立起系统的体系结构模型． 除此之外， ＡＡＤＬ还提供了行为附件（ ｂｅｈａｖｉｏｒａｎｎｅｘ） 增强了对组件的功能行为的描述， 通过行为附件的执行模型能够更加详细地描述线程和子程序的功能行为模型．为了方便后续内容中阐述ＡＡＤＬ组合验证原理， 这里我们给出一个简单的ＡＡＤＬ模型示例如表１ 所示， 即一个ＡＡＤＬ系统ｔｏｐｌ ｅｖｅｌ ， 它的子构件包括Ａ、 Ｂ和Ｃ， 子构件之间的链接为即时通信方式（ｉｍｍｅｄｉａｔｅ）．表１ＡＡＵＬ模型示例ｐａｃｋａｇｅＩｎｔｅｇｅｒ一ＴｏｙｐｕｂｌｉｃｗｉｔｈＢａｓｅ＿Ｔｙｐｅｓ；ｓｙｓｔｅｍＡｆｅａｔｕｒｅｓＩ ｎｐｕｔ＿Ａ：ｉ ｎｄａｔ ａｐｏｒｔＢａｓｅ＿ＴｙｐｅｓＩＩＩｎｔ ｅｇｅｒ；Ｏｕｔｐｕｔ一Ａ：ｏｕｔｄａｔａｐｏｒｔＢａｓｅ＿Ｔｙｐｅｓ： ；Ｉｎｔｅｇｅｒ；ｅｎｄＡ；ｓｙｓｔｅｍＢｆｅａｔ ｕｒｅｓＩ ｎｐｕｔ＿Ｂ：ｉｎｄａｔａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ：Ｉｎｔｅｇｅｒ；？ｕｔｐｕｔ＿Ｂ： ｏｕｔｄａｔ ａｐｏｒｔＢａｓｅ＿Ｔｙｐｅｓ： ：Ｉｎｔ ｅｇｅｒ；ｅｎｄＢ；ｓｙｓｔｅｍＣｆｅａｔ ｕｒｅｓＩｎｐｕｔｌ＿Ｃ：ｉｎｄａｔ ａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ ： ： Ｉｎｔｅｇｅｒ；Ｉ ｎｐｕｔ２＿Ｃ：ｉｎｄａｔ ａｐｏｒｔＢａｓｅ＿Ｔｙｐｅｓ： ：Ｉ ｎｔｅｇｅｒ；Ｏｕｔｐｕｔ：ｏｕｔｄａｔ ａｐｏｒｔ Ｂａｓｅ＿ＴｙｐｅｓＸＩ ｎｔｅｇｅｒ；ｅｎｄＣ？ｓｙｓｔｅｍｔ ｏｐ＿ｌｅｖｅｌｆｅａｔ ｕｒｅｓＩ ｎｐｕｔ一Ｓ： ｉｎｄａｔ ａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ： Ｉ ｎｔｅｇｅｒ；Ｏｕｔｐｕｔ一Ｓ：ｏｕｔｄａｔａｐｏｒｔＢａｓｅ＿Ｔｙｐｅｓ： ： Ｉ ｎｔ ｅｇｅｒ；ｅｎｄｔ ｏｐ一ｌｅｖｅｌ；ｓｙｓｔｅｍｉｍｐｌｅｍｅｎｔ ａｔｉｏｎｔ ｏｐ＿ｌｅｖｅｌ．  ＩｍｐｌｓｕｂｃｏｍｐｏｎｅｎｔｓＡ一ｓｕｂ：ｓｙｓｔ ｅｍＡ；Ｂ＿ｓｕｂ：ｓｙｓｔ ｅｍＢ；Ｃ＿ｓｕｂ： ｓｙｓｔ ｅｍＣ；ｃｏｎｎｅｃｔｉｏｎｓＩ Ｎ＿ＴＯ＿Ａ：ｐｏｒｔ Ｉ ｎｐｕｔ一Ｓ—〉Ａ一ｓｕｂ． Ｉ ｎｐｕｔ一Ａ｛ Ｃｏｍｍｕｎｉｃａｔｉ ｏｎ一Ｐｒｏｐｅｒｔｉ ｅｓ： ：Ｔｉ ｍｉｎｇ＝〉ｉｍｍｅｄｉａｔｅ； ｝ ；Ａ＿ＴＯ＿Ｂ：ｐｏｒｔＡ＿ｓｕｂ． Ｏｕｔｐｕｔ＿Ａ—〉Ｂ＿ｓｕｂ．Ｉｎｐｕｔ＿Ｂ｛ Ｃｏｍｍｕｎｉ ｃａｔ ｉ ｏｎ一Ｐｒｏｐｅｒｔ ｉ ｅｓ： ：Ｔｉ ｍｉ ｎｇ＝〉ｉｍｍｅｄｉａｔｅ； ｝ ；Ａ＿ＴＯ＿Ｃ： ｐｏｒｔＡ＿ｓｕｂ．（）ｕｔｐｕｔ＿Ａ—］ ＞Ｃ＿ｓｕｂ．Ｉｎｐｕｔｌ＿Ｃ｛ Ｃｏｍｍｕｎｉｃａｔｉｏｎ＿Ｐｒｏｐｅｒｔｉｅｓ： ：丁ｉ ｍｉｎｇ＝〉ｉｍｍｅｄｉａｔ ｅ； ｝ ；Ｂ一ＴＯ＿Ｃ：ｐｏｒｔＢ＿ｓｕ ｂ． 〇ｕｔｐｕｔ一Ｂ—〉Ｃ＿ｓｕｂ． Ｉ ｎｐｕｔ２＿Ｃ｛ Ｃｏｍｍｕｎｉｃａｔ ｉ ｏｎ＿Ｐｒｏｐｅｒｔ ｉｅｓ：： Ｔｉ ｍｉｎｇ＝〉ｉｍｍｅｄｉａｔｅ； ｝ ；Ｃ＿ＴＯ＿Ｏｕｔｐｕｔ：ｐｏｒｔＣ＿ｓｕｂ． Ｏｕｔｐｕｔ＿Ｃ—＞０ｕｔｐｕｔ＿Ｓ｛ Ｃｏｍｍｕｎｉｃａｔｉｏｎ＿Ｐｒｏｐｅｒｔｉ ｅｓ！ Ｔｉ ｍｉ ｎｇ＝＞ｉｍｍｅｄｉａｔｅ； ｝ ；ｅｎｄｔ ｏｐ＿ｌｅｖｅｌ．Ｉｍｐｌ ；ｅｎｄＩ ｎｔ ｅｇｅｒ＿Ｔｏｙ；２． ２ 组合验证概述为了验证一个系统满足其需求， Ｈａｍｍｏｎｄ 提出了满意度论证的概念［２ ２：， 即通过系统行为的规范和对系统的假设来建立系统需求． 为了形式化满意度参数， 基于契约的组合验证方法提供了一种机制，张博林等：一种面向安全关键软件的ＡＡＤＬ模型组合验证方法 ２１３７通过对其组件信息的抽象， 从而推导系统级需求是否被满足． 组合验证中组件契约描述如下：Ｃ〇ｎｔｒａＣｔ＝（ Ａｓｓｕｍｅ，Ｇｕａｒａｎｔｅｅ） ， 其中Ａｓｓｕｍｅ为组件契约的假设部分， 描述组件对其运行环境的需求， 可以是验证过程中的组件输人的断言或者是不变量； Ｇｕａｒａｎｔｅｅ为组件契约的保证部分， 描述当组件的假设部分被满足时， 组件必须保证的外部行为特征， 即是否满足需求． 契约精确地指定了组件与系统其它部分的交互所需要的信息， 还支持按照系统模型的层次结构对验证部分进行层次分解．在表１ 案例的基础上， 我们给出如下系统验证需求：ｔｏｐｌｅｖｅｌｓｙｓｔｅｍ输人小于１０ 时， 输出应小于５０； 子组件Ａ输人小于２０ 时， 输出应小于二倍的输人； 子组件Ｂ输入小于２０ 时． 输出应小于输人值与１５ 之和； 子组件Ｃ输出应小于子系统Ａ和子系统Ｂ输人数据之和． 根据需求建立组件契约及证明过程如图２ 所示． 表１ 只简单给出了两层结构， 但可以任意多个层次． 从而推广到更复杂的系统验证中．表２ＡＧＲＥＥａｎｎｅｘ 示例①ｃ°Ａａ： Ｉｎｐｕｔ ＜２０Ｇａ： （Ｘｉｔｐｕｔ ＜２＊Ｉｎｐｕｔ－？？Ｂ？—Ａｃ： ｎｏｎｅＧＡ：Ｏｕｔｐｕｔ＝Ｉｎｐｕｔ １ ＋ Ｉｎｐｕｔ２１Ａ？：Ｉ ｎｐｕｔ ＜２０Ｇａ：Ｏｕｔｐｕｔ＜Ｉｎｐｕｔ ＋１ ５Ａｓ：Ｉ ｎｐｕｔ ＜１０ＪＧｓ： （）ｕｔｐｕｔ ＜５〇！｜图２ 组合验证案例假设保证推理环境ＡＧＲＥＥ是集成在开源工具ｆｐｌａＯＳＡＴＥ（ＯｐｅｎＳｏｕｒｃｅＡＡＤＬＴｏｏｌＥｎｖｉ ｒｏｎｍｅｎｔ）上的ＡＡＤＬ模型的组合验证工具， 并发布了ＡＡＤＬ组合验证附件ＡＧＲＥＥａｎｎｅｘ用于构造组件契约．在ＡＧＲＥＥ框架下， ＡＡＤＬ模型使用ＡＧＲＥＥａｎｎｅｘ构造的契约表示组件的功能， 在对系统的分层设计过程中，当前层的需求在设计下一层组件的时候成为下一层各个组件的需求， 从而下一层组件必须满足当前层的需求， 然后由各个层次不同组件的需求构造相应的组件契约， 最后通过组合推理的方法证明这个系统体系结构的正确性． 表１ 的系统验证需求对应的ＡＡＤＬＡＧＲＥＥａｎｎｅｘ表示如表２ 所示？使用ＡＧＲＥＥ可以完成对该模型的验证分析， 确认其需求得到满足．ＡＧＲＥＥａｎｎｅｘ具体语法可参见手册①■ｐａｃｋａｇｅＩ ｎｔｅｇｅｒ＿Ｔｏｙｐｕｂｌｉ ｃｗｉｔ ｈＢａｓｅ一Ｔｙｐｅｓ；ｓｙｓｔｅｍ八ｆｅａｔ ｕｒｅｓＩｎｐｕｔ： ｉｎｄａｔａｐｏｒｔ Ｂａｓｅ一Ｔｙｐｅｓ； ！ Ｉ ｎｔ ｅｇｅｒ；Ｏｕ ｔｐｕｔ：ｏｕｔｄａｔ ａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ：Ｉ ｎｔｅｇｅｒ；ａｎｎｅｘａｇｒｅｅ｛＊＊ａｓｓｕｍｅ“Ａｉ ｎｐｕｔｒａｎｇｅ”：Ｉ ｎｐｕｔ ＜２０；ｇｕａｒａｎｔ ｅｅ“Ａｏｕｔｐｕｔｒａｎｇｅ”：Ｏｕｔｐｕｔ ＜Ｃ２＊ Ｉ ｎｐｕｔ；＊＊｝ ；ｅｎｄＡ；ｓｙｓｔｅｍＢｆｅａｔ ｕｒｅｓＩ ｎｐｕｔ： ｉｎｄａｔａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ：Ｉｎｔｅｇｅｒ；Ｏｕｔｐｕｔ： ｏｕｔｄａｔａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ：Ｉ ｎｔｅｇｅｒ；ａｎｎｅｘａｇｒｅｅ｛＊＊ａｓｓｕｍｅ“Ｂｉ ｎｐｕｔｒａｎｇｅ”： Ｉ ｎｐｕｔ ＜２０；ｇｕａｒａｎｔｅｅ＊ ＊Ｂｏｕｔｐｕｔｒａｎｇｅｗ ：Ｏｕｔｐｕｔ＜ＣＩｎｐｕｔ－ｆ１ ５；＊ ＊｝ ；ｅｎｄＢ；ｓｙｓｔｅｍＣｆｅａｔ ｕｒｅｓＩ ｎｐｕｔ  １： ｉｎｄａｔａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ： Ｉｎｔｅｇｅｒ；Ｉｎｐｕｔ２ ： ｉｎｄａｔ ａｐｏｒｔＢａｓｅ一Ｔｙｐｅｓ： ： Ｉｎｔ ｅｇｅｒ；Ｏｕｔｐｕｔ：ｏｕｔｄａｔａｐｏｒｔＢａｓｅ＿Ｔｙｐｅｓ＊ＩＩ ｎｔｅｇｅｒ；ａｎｎｅｘａｇｒｅｅ｛＊＊ｇｕａｒａｎｔｅｅ“Ｃｏｕｔｐｕｔｒａｎｇｅ”：Ｏｕｔｐｕｔ：Ｉ ｎｐｕｔｌ＋Ｉｎｐｕｔ２ ；＊＊；：ｅｎｄＣ；ｓｙｓｔｅｍｔ ｏｐ＿ｌｅｖｅｌｆｅａｔ ｕｒｅｓＩ ｎｐｕｔ：ｉｎｄａｔ ａｐｏｒｔＢａｓｅ＿Ｔｙｐｅｓ！ ；Ｉ ｎｔｅｇｅｒ；Ｏｕｔｐｕｔ：ｏｕｔｄａｔａｐｏｒｔＢａｓｅ＿ＴｙｐｅｓＩ；Ｉ ｎｔｅｇｅｒ；ａｎｎｅｘａｇｒｅｅ｛＊＊ａｓｓｕｍｅ“Ｓｙｓｔｅｍｉ ｎｐｕｔｒａｎｇｅ”： Ｉ ｎｐｕｔ ＜＝９ ；ｇｕａｒａｎｔｅｅ＇＇Ｓｙｓｔｅｍｏｕｔｐｕｔｒａｎｇｅ＊ ＊：Ｏｕｔｐｕｔ  ＜Ｃ５０；＊＊｝ ；ｅｎｄｔｏｐ＿ｌｅｖｅｌ ；ｓｙｓｔｅｍｉｍｐｌｅｍｅｎｔａｔｉｏｎｔｏｐ＿ｌ ｅｖｅｌ．Ｉ ｍｐｌｓｕｂｃｏｍｐｏｎｅｎｔｓＡ＿ｓｕｂ： ｓｙｓｔｅｍＡ；Ｂ＿ｓｕｈ： ｓｙｓｔ ｅｍＢ；Ｃ＿ｓｕｂ：ｓｙｓｔ ｅｍＣ；ｃｏｎｎｅｃｔｉｏｎｓＩ Ｎ＿ＴＯ＿Ａ：ｐｏｒｔ Ｉｎｐｕｔ—〉Ａ＿ｓｕｂ． Ｉ ｎｐｕｔ｛ Ｃｏｍｍｕ ｎｉ ｃａｔｉｏｎ＿Ｐｒｏｐｅｒｔｉｅｓ： ： Ｔｉ ｍｉ ｎｇ＝〉ｉｍｍｅｄｉａｔｅ ； ｝ ；Ａ＿ＴＯ一Ｂ：ｐｏｒｔＡ＿ｓｕｂ． Ｏｕｔｐｕｔ—〉Ｂ＿ｓｕｂ． Ｉ ｎｐｕｔ｛ Ｃｏｍｍｕｎｉ ｃａｔｉｏｎ一Ｐｒｏｐｅｒｔｉｅｓ： ：Ｔｉ ｍｉ ｎｇ＝〉ｉ ｍｍｅｄｉ ａｔｅ； ｝ ；Ａ＿ＴＯ＿Ｃ：ｐｏｒｔＡ＿ｓｕｂ． Ｏｕｔｐｕｔ—＞Ｃ＿ｓｕｂ． Ｉ ｎｐｕｔ ｌ｛ Ｃｏｍｍｕｎｉｃａｔｉｏｎ＿Ｐｒｏｐｅｒｔｉｅｓ： ：Ｔｉ ｍｉ ｎｇ＝〉ｉｍｍｅｄｉａｔｅ ；Ｂ一ＴＯ＿Ｃ：ｐｏｒｔＢ一ｓｕｂ． Ｏｕｔｐｕｔ—〉Ｃ＿ｓｕｂ． Ｉ ｎｐｕｔ ２｛ Ｃｏｍｍｕｎｉｃａｔｉｏｎ＿Ｐｒｏｐｅｒｔｉ ｅｓ： ： Ｔｉ ｍｉ ｎｇ＝〉ｉｍｍｅｄｉ ａｔｅ ；｝；Ｃ一丁Ｃ）＿Ｏｕｔｐｕｔ：ｐｏｒｔＣ一ｓｕｂ． Ｏｕｔｐｕｔ—＞Ｏｕｔｐｕｔ｛ Ｃｏｍｍｕ ｎｉ ｃａｔｉ ｏｎ一Ｐｒｏｐｅｒｔｉ ｅｓ：： Ｔｉ ｍｉ ｎｇ＝〉ｉ ｍｍｅｄｉａｔｅ：；ｅｎｄｔｏｐ＿ｌｅｖｅｌ．Ｉ ｍｐｌ；ｅｎｄＩ ｎｔｅｇｅｒ＿Ｔｏｙ；２． ３ＵＰＰＡＡＬ概述ＵＰＰＡＡＬ［ ？是一个依靠时间自动机进行验证分析的验证环境， 可以构造时间自动机网络模型对实时系统进行建模、 模拟和验证． 在ＵＰＰＡＡＬ中进行的模型验证的理论基础是自动机中的可达性验证理论， 依据该理论可以验证模型中所有状态在可达路径上的性质集合． 若用Ｍ来表示一个时间状态自动机， 用ｉ？表示验证过程中用到的时序逻辑， 在验①ＡｓｓｕｍｅＧｕａｒａｎｔｅｅＲｅａｓｏｎｉ ｎｇＥｎｖｉ ｒｏｎｍｅｎｔ（ ＡＧＲＥＥ）．ｈｔ ｔｐ： ／／ｌ ｏｏｎｗｅｒｋｓ．ｃｏｍ／ｔｏｏｌｓ／ａｇｒｅｅ．ｈｔ ｍｌ．２０１ ９， ０８，２４１１ 期＆－＊ＡｇｘＢｔ＜＜＼＼＼＼ＡＧＧＧ２１３８ 计 算 ２０２０年证过程中， 会搜索所有的Ｍ的状态， 而且会验证Ｒ在搜索过程中经过的每一条可达的路径． 验证需求的ｉ？ 必须使用特定的形式化描述， 在ＵＰＰＡＡＬ中使用了一个简化版的时序逻辑ＴＣＴＬ对表示的．一个ＴＣＴＬ公式可以验证模型中某个状态是否存在， 比如ｘ＝ ＝３在任何工等于３ 上的状态为真． 所有的状态公式和状态转移都不能更改状态机中的表达式， 状态公式可以析取． 表３ 给出了ＵＰＰＡＡＬ支持的ＴＣＴＬ公式及其能力， 使用这些公式可以完成对模型的可达性、 活性、 安全性等性质的验证．表３ 路径公式公式类型 公式表示 说明可达性公式 ＥＯ＜ｐ表示状态公式９ 是从初始位置可达的，比如“初始状态一定是可达的活性公式 Ａ＜）＜ｐ活性表示在某种情况下，一个事情最终一定发生，通常表述为“好事”会发生．Ａ〈 〉９？ 表示最终一定满足安全性公式Ａ［］炉Ｅ［２＜ｐ安全性是指在某种情况下，一件事永远都不会发生，一般用来表达不希望出现的事情， 因此安全性也可以表述为“坏事”不会发生． Ａ［］ｐ表示在所有可达的所有状态中都应该满足 而 表示有一条路径上的状态都满足＆２． ４ 面向安全关键软件的ＡＡＤＬ模型组合验证方法研究框架已有的验证方法往往是将扁平化的整个ＡＡＤＬ模型进行模型转换然后直接验证， 但是对工业界复机 学 报杂的ＡＡＤＬ模型直接验证往往存在状态空间爆炸的问题． 工业界的ＡＡＤＬ模型涉及到大量的函数调用行为， 在ＡＡＤＬ模型中可以使用子程序及行为附件来表达， 但是现有的验证手段很少涉及对子程序及其行为附件的验证分析． 因此， 为了更好的完成对复杂系统的验证分析， 本文提出了一种面向安全关键软件的ＡＡＤＬ模型组合验证方法． 该方法总体框架如图３ 所示， 包括三部分：（ １ ） 提出ＡＡＤＬ体系结构模型的组合验证方法， 根据需求及需求分解使用ＡＡＤＬ层次化的构建体系结构模型， 同时确定其组件划分， 使用需求及子需求构造组件的契约， 基于组件契约对系统的体系结构模型进行组合验证， 验证系统体系结构的正确性．（２） 提出基于ＵＰＰＡＡＬ的组件功能行为验证方法， 基于模型转换语言ＡＴＬ（Ａｔｌ ａｓＴｒａｎｓｆｏｒｍａｔｉ ｏｎ１＾吨１＾昭６）［２３］将单组件ＡＡＤＬ模型（ 主要是子程序）转换为ＵＰＰＡＡＬ模型． 根据ＡＡＤＬ２ＵＰＰＡＡＬ的模型转换方法， 将ＡＡＤＬ组件功能行为模型（ 主要是子程序和行为附件）转换为ＵＰＰＡＡＬ模型并进行验证分析， 从而验证叶子组件的功能行为的正确性．（３） 实现了ＡＡＤＬ模型验证原型工具， 用于支持ＡＧＲＥＥ组合验证和ＵＰＰＡＡＬ的组件功能行为验证， 并通过插件技术集成在ＡＡＤＬ 建模工具ＯＳＡＴＥ±，面向安全关键软件的ＡＡＤＬ模型组合验证方法图３ 面向安全关键软件的ＡＡＤＬ模型组合验证方法框架张博林等：一种面向安全关键软件的ＡＡＤＬ模型组合验证方法 ２１３９１ １ 期３ＡＡＤＬ的体系结构模型的组合验证方法一个复杂的系统需求需要对其进行分解并分配给不同的子系统， 体系结构的分解同时涉及到需求和体系结构， 体系结构的可能会影响需求分配给每一个子系统， 所以在分解的同时需要确定需求分配给子系统的架构能否满足系统级需求， 确定子系统架构的建立对系统环境是否有改变［３４］， ＡＡＤＬ建模语言可以完成复杂系统的体系结构建模需求．３．１ 基于ＡＡＤＬ的火箭发射控制子系统体系结构建模火箭发射系统是在用来控制火箭执行各项操作以及包含火箭自主执行的部分发射功能的系统， 控制从接收到发射的指令一直持续到火箭顺利离开发射装置． 经过简化的火箭发射系统的结构如图４ 所示， 主要包括发控单元计算机、 火箭供电机箱、 供电控制组合、点火控制组合等组成， 本文主要介绍的火箭发射控制子系统在发控单元计算机中运行． 火箭发射控制子系统的功能主要是根据主控任务的控制命令， 进行相应的命令的执行， 是处于发控单元计算机中过程层的控制系统．图４ 火箭发射系统结构图火箭发射控制系统的需求ＳＲ为： 首先打开排气盖和箭舱盖， 执行火箭发射准备命令， 同时进行火箭加电控制， 然后解锁箭舱和安全机构， 最后执行火箭点火命令． 如果执行过程中出现故障， 则进行断电控制． 经过对系统的功能行为详细分析之后， 对系统需求进行分解， 可以得到以下子系统需求：（ １） 排气盖控制ＳＲ１ ． 收到排气盖开／关盖控制命令， 执行排气盖开／关盖控制， 如果排气盖状态查询正常， 回告发控系统排气盖开／关盖控制执行成功； 如果排气盖状态查询异常， 则回告发控系统排气盖故障．（２） 箭舱盖控制ＳＲ２． 收到火箭舱盖开／关盖控制命令， 执行箭舱盖开／关控制， 如果箭舱盖状态查询正常， 回告发射控制系统箭舱盖控制执行成功； 如果箭舱盖状态查询异常． 则回告发控系统箭舱盖故障．（３） 火箭发射准备／取消控制ＳＲ３． 收到火箭发射准备／取消控制命令， 进行火箭发射准备／取消控制， 如果闭合级电路状态查洵正常， 回告发射控制系统火箭发射准备／取消控制执行成功； 如果闭合级电路状态查询异常， 则回告发控系统火箭发射准备／取消异常．（４） 火箭加电控制ＳＲ４． 收到火箭加电命令， 如果加电自检正常则进行火箭加电控制， 回告发控系统火箭加电行成功； 如果加电自检异常， 则进行断电控制， 回告发射控制系统异常．其余子需求为： 箭舱解锁／锁定控制ＳＲ５ 、 热电池激活控制ＳＲ６、 安全机构解锁／恢复控制ＳＲ７、 火箭点火控制ＳＲ８、 火箭断电控制ＳＲ９， 这里就不再赘述． 构造火箭发射控制系统的ＡＡＤＬ模型如图５所示．图５ 火箭发射控制子系统体系结构为了说明与火箭发射控制子系统的需求分解与体系结构分解的关系， 本文以火箭加电控制ＳＲ４ 为例说明对需求的进一步细化分解． 火箭加电控制由火箭加电１ 控制ＳＲ４Ｃ１、火箭加电２ 控制ＳＲ４Ｃ２ 和火箭加电３ 控制ＳＲ４Ｃ３ 三个子组件组成， 每一个加电控制是针对不同的电池组件进行控制， 火箭在进行加电控制时， 正常情况下是按照严格的加电顺序进行加电， 否则会回告加电错误． 下一层以火箭加电１ 控制为例可以分解为火箭加电１函数ＳＲ４Ｃ１Ｈ１、火箭自检结果查询函数ＳＲＣ１ Ｈ３ 和火箭类型识别码查询函数ＳＲＣ１Ｈ４； 这一层还能够进一步划分，以火箭自检结果查询函数为例可以划分为单步自检看门狗函数ＷＤＳＥ、 单步自检函数ＳＳＥ、 连续自检看门狗函数ＷＤＳＩ 以及连续自检函数ＳＳＩ． 此时对模型已经细化到了子程序层面， 其体系结构如图６ 所示．２１４０ 计 算机 学 报２０２０年丨 冬丨 ６ 火箭发射控制子系统体系结构模型３． ２ 基于契约的需求形式化复杂安全关键软件的层次分解涉及到需求分解和体系结构模型， 在３．１ 节中层次的构造其体系结构模型后， 如果对体系结构模型进行组合验证， 需要把系统各个层次的组件需求形式化为组件契约．即抽象的外部可见行为， 本节主要介绍基于契约的需求形式化．由于自然语言需求描述不精确的问题． 把一个需求抽象为一个契约， 首先要明确其输入输出， 然后忽略其内部行为， 将组件抽象为黑盒， 最后明确组件的输入输出关系， 然后构造组件契约． 本节以火箭加电控制子系统的需求及其需求分解为例构造其契约．首先需要说明一个控制命令应该由火箭模式（ 单步或连续） 、火箭状态（ 正常态或训练态） 、 操作命令、 火箭码等数据组成，一个控制命令会由获取控制命令子程序进行分解． 然后返回具体命令到调用该子程序的组件中． 本文为了表达的简洁， 在叙述需求时不再对控制命令进行详细介绍．根据上节的介绍可以知道， 火箭加电控制的需求为ＳＲ４， 其需求和体系结构分解为： 加电１ 控制ＳＲ４Ｃ１、加电２ 控制ＳＲ４Ｃ２ 和加电３ 控制ＳＲ４Ｃ３，每个子系统应完成相应的加电控制． 而此需求描述实际上涵盖了子系统中组件的功能， 根据需求ＳＲ４其输入为： 火箭发射控制系统的加电命令． 输出为：加电命令的执行结果、 是否发出断电令以及断电码．输人输出关系为： 输人正确的加电令且子系统反馈正常， 回告加电命令