第４ ３ 卷第１ １ 期２ ０ ２ ０ 年１ １ 月计算机学报ＣＨ ＩＮＥＳＥＪ Ｏ ＵＲＮＡＬＯ ＦＣＯＭＰ ＵＴ ＥＲ ＳＶｏｌ ．４ ３Ｎｏ．１ １Ｎｏ ｖ． ２０ ２ ０一种面向安全关键软件的ＡＡＤＬ 模型组合验证方法张博林ｕ杨志斌ｕ ’ ２ ＞周勇ｕ马燕燕ｎ黄志球＾薛垄３＞南京航空航天大学计算机科学与技术学院南京２ １１ １０ ６ ）２＞（ 高安全系统软件开发与验证技术工信部重点实验室南京２ １ １ １ ０ ６ 〉３ ）（上海航天电子技术研究所上海２０ １ １０ ９ ）摘要安全关键软件变得越来越复杂， 这类软件的形式化验证是一个具有挑战性的问题． 本文针对火箭发射控制子系统实例， 提出一种组合验证方法， 该方法采用组合验证与模型转换相结合的方法完成对该系统的验证与分析． 首先， 使用体系结构分析与设计语言ＡＡＤＬ 对火箭发射控制子系统进行层次化构造系统的体系结构模型， 将系统各个层次的组件需求形式化为组件契约， 然后通过组合验证确保系统体系结构的正确性； 其次， 提出了ＡＡＤＬ２ ＵＰＰＡＡＬ 的模型转换方法， 然后基于ＵＰ ＰＡＡＬ 对该模型中组件的功能行为进行验证与分析， 确保组件的功能行为的正确性； 最后， 实现了ＡＡＤＬ 模型验证原型工具， 支持基于ＡＧＲＥＥ 的体系结构模型的组合验证和支持基于ＵＰＰＡＡＬ 的组件功能行为验证， 通过对火箭发射控制子系统案例的验证和分析表明本文所提方法的有效性与局限性．关键词安全关键软件； 火箭发射控制子系统； 组合验证； ＡＡＤＬ ；ＵＰＰＡＡＬ中图法分类号ＴＰ ３ １ １ＤＯＩ 号 １ ０．  １ １８ ９ ７ ／ ＳＰ． Ｊ ．  １ ０ １ ６ ． ２ ０ ２ ０．０ ２ １ ３ ４ＡＣｏｍｐ ｏｓｉ ｔ ｉｏｎａｌＶｅｒｉｆｉｃａｔｉｏｎ Ｍｅｔｈｏｄ ｆｏｒＡＡＤＬＭｏｄｅｌｓｏｆ Ｓａｆｅｔｙ－Ｃｒｉｔ ｉｃａｌ ＳｏｆｔｗａｒｅＺ ＨＡＮＧＢｏ－Ｌｉ ｎ１ １ＹＡＮＧ ＺＨ－Ｂｉｎ１ ， ２ ）ＺＨＯＵＹｏｎｇ１ ＊ＭＡＹａｎ－ＹａｎｕＨ ＵＡＮＧ Ｚｈｉ－Ｑｉｕ１ Ｋ２）ＸＵＥＬｅｉ３ ＞ｌ ）ｉ Ｃｏ ｌｌ ｅｇ ｅ ｏ ｆＣｏ ｍｐ ｕ ｔｅｒ Ｓｃｉ ｅｎ ｃｅ ａｎｄ Ｔｅｃ ｈｎ ｏｌ ｏｇｙ  ｔＮａ ｎｊ ｉ ｎｇＵｎ ｉ ｖｅｒｓ ｉ ｔｙ ｏ ｆ Ａｅｒｏ ｎａ ｕｔｉ ｃｓ ａ ｎｄＡｓ ｔ ｒｏ ｎａ ｕ ｔｉ ｃｓ ｔ Ｎａ ｎｊ ｉｎｇ２ １ １ １ ０ ６ ）（． Ｋｅｙ Ｌａ ｂｏ ｒａ ｔｏ ｒ ｙ ｏｆ Ｓｏ ｆｔｗａ ｒ ｅＤｅ ｖｅｌｏ ｐｍｅｎ ｔ ａｎｄＶｅ ｒｉｆｉ ｃａ ｔ ｉｏ ｎ Ｔｅｃｈ ｎｏ ｌ ｏｇｙ Ｍｉ ｎ ｉｓ ｔ ｒｙ ｏ ｆ Ｉｎｄｕ ｓ ｔｒｙ ａ ｎｄＩｎ ｆｏ ｒｍａｔ ｉｏ ｎ  Ｔｅｃｈｎ ｏ ｌｏ ｇ ｙ ｆｏ ｒ Ｈｉ ｇｈＳｅｃ ｕｒｉ ｔｙ Ｓｙｓ ｔ ｅｍｓ， Ｎａｎｊｉｎｇ２ １ ０ ０ ９ ３ ）｛ Ｓｈａｎｇｈａｉ Ａｅ ｒｏｓｐａｃｅ Ｅｌｅｃ ｔｒ ｏｎ ｉ ｃＴｅｃ ｈｎｏ ｌｏ ｇｙ Ｉｎｓｔ ｉｔ ｕｔ ｅ９Ｓｈａｎｇｈａｉ２０ １ １０ ９ ）Ａ ｂｓｔｒ ａｃ ｔＴ ｈｅ ｃｏｍｐ ｌ ｅｘｉ ｔｙｏｆ ｓａｆ ｅｔ ｙ－ ｃｒｉ ｔ ｉｃａｌ ｓｏｆｔｗａｒｅ ｈａ ｓｂｅｅ ｎ ｈｉｇ ｈｅｒ ａｎｄ ｈｉｇｈ ｅｒｗｉ ｔｈｔｈ ｅｄｅｖｅｌｏｐｍｅｎｔｏｆ ｒｅ ｑｕ ｉｒ ｅｍ ｅｎ ｔ ｓｐ ｅｃｉ ｆ ｉ ｃａｔ ｉ ｏｎ ．Ｔ ｈｅ ｒｅ ｆｏ ｒｅ ，ｉ ｔ ｉ ｓ ａ ｓｅ ｒ ｉ ｏ ｕｓ ｃｈ ａ ｌ ｌ ｅ ｎｇ ｅ ｔ ｏｖ ｅｒｉ ｆ ｙｗｈ ｅ ｔｈ ｅ ｒ ｔ ｈ ｅ ｓｅ ｃｏ ｍｐ ｌｅｘｓｙ ｓ ｔ ｅｍ ｓｓａ ｔ ｉ ｓｆ ｙｅ ｘｐｅ ｃ ｔｅ ｄｐｒ ｏｐｅ ｒ ｔ ｉ ｅ ｓｏｒ ｎｏ ｔ．Ａｃｃｏ ｒｄｉ ｎ ｇｔｏ ｔ ｈｅ ｅ ｘａｍｐ ｌ ｅ ｏｆ ｔ ｈｅ ｒｏｃ ｋｅ ｔ ｌａ ｕｎｃ ｈｃ ｏｎ ｔｒ ｏｌｓｕ ｂｓ ｙｓ ｔ ｅｍ ，ｔ ｈ ｉ ｓｐ ａｐ ｅ ｒ ｐ ｒｏｐｏ ｓｅ ｓａ ｃｏ ｍｂ ｉ ｎａ ｔ ｉ ｏｎ ｏｆ ｃｏｍ ｐｏ ｓｉ ｔｉｏｎ ａ ｌ ｖｅ ｒｉ ｆｉ ｃ ａ ｔｉ ｏ ｎａ ｎ ｄｍ ｏｄｅ ｌ ｃｈ ｅ ｃｋ ｉ ｎｇ ｔ ｏｃｏｍ ｐｌ ｅ ｔ ｅｔ ｈ ｅｖ ｅｒ ｉ ｆ ｉｃ ａ ｔｉ ｏ ｎａ ｎｄ ａ ｎａ ｌ ｙ ｓｉ ｓｏｆｔ ｈｅ ｓ ｙｓｔ ｅｍ．Ｆｉｒ ｓｔ ， Ａｒ ｃｈｉ ｔ ｅ ｃｔ ｕ ｒｅＡ ｎａ ｌｙ ｓｉ ｓａ ｎｄ Ｄ ｅ ｓｉ ｇｎＬａｎ ｇｕ ａ ｇｅ （ ＡＡＤＬ）ｉ ｓ ｕｓｅ ｄ ｔ ｏ ｈｉ ｅ ｒａ ｒ ｃ ｈｉ ｃａｌ ｌ ｙｃｏ ｎｓ ｔ ｒｕｃ ｔ ｔ ｈｅ  ａｒ ｃ ｈ ｉｔ ｅ ｃｔ ｕ ｒｅ ｍｏｄ ｅｌ  ｏｆ ｔ ｈ ｅｒ ｏｃｋｅ ｔ ｌ ａ ｕｎｃｈｃｏｎｔ ｒｏｌ ｓ ｕｂ ｓｙ ｓｔ ｅ ｍ ， ａ ｎｄ ｔ ｈｅ ｃ ｏｍｐ ｏｎ ｅｎｔ ｒｅ ｑｕ ｉｒｅｍ ｅｎ ｔ ｓｏ ｆ ｅａｃｈ ｌ ｅ ｖｅ ｌ ｏｆ ｔ ｈｅ ｓｙｓ ｔ ｅｍ ａ ｒｅｆ ｏｒｍ ａ ｌ ｉｚ ｅｄ ｂ ｙｃｏｎｔ ｒａｃｔｔ ｈｅ ｏｒｙ ， ａ ｎｄｔ ｈ ｅｎ ｔｈ ｅｃ ｏｒｒｅｃｔ ｎｅ ｓｓｏ ｆｔ ｈｅ ｓｙ ｓｔｅｍａｒ ｃｈ ｉｔ ｅｃｔ ｕ ｒｅ ｉ ｓ ｖｅ ｒ ｉｆｉ ｅ ｄｔ ｈｒｏｕ ｇｈ ｃｏｍｐｏｓ ｉｔ ｉｏｎ ａｌｖｅｒｉｆｉ ｃａｔｉｏｎ．Ｓｅｃ ｏｎｄｌ ｙ ，ｔ ｈｅ ｆｕｎｃｔ ｉｏｎａｌ ｂ ｅｈ ａ ｖｉｏｒｏｆ  ｔｈ ｅ ｃｏｍ ｐｏｎ ｅｎｔ ｓ ｉ ｎ ｔｈ ｅ ｍｏ ｄｅｌ ａｒｅ ｖｅｒｉ ｆｉ ｅｄｂａ ｓｅ ｄｏｎＵＰＰ ＡＡ Ｌ ｔｏ ｅｎ ｓｕ ｒ ｅｔ ｈ ｅ ｃｏｒｒ ｅｃｔ ｎ ｅｓ ｓｏｆ  Ｃｏｍｐ ｏｎｅ ｎｔ ｂｅ ｈａｖ ｉｏｒｓ ；Ｆｉ ｎａ ｌ ｌｙ ，ｔｈｅ ＡＡＤＬｍｏ ｄｅｌ  ｖｅｒ ｉ ｆｉ ｃａｔ ｉｏｎｐｒｏｔ ｏｔｙｐ ｅ ｔｏｏｌ  ｉｓ ｉｍｐ ｌ ｅｍｅ ｎｔ ｅｄ ｔｏ ｓｕ ｐｐｏｒｔ ｔ ｈｅ ｃｏｍ ｐｏｓ ｉ ｔｉ ｏｎａ ｌ ｖｅ ｒｉ ｆｉ ｃａ ｔ ｉｏｎ ｏｆ ＡＧＲＥＥ－ｂ ａ ｓ ｅｄ ａｒｃｈ ｉｔ ｅｃｔ ｕ ｒｅ收稿日期．．２０ １ ９－１ ２－ ２ ４ ； 在线发布日期： ２ ０２ ０￣０ ４－１ ６． 本课题得到国家自然科学基金（ ６ １ ５ ０ ２ ２ ３ １ ） 、国家重点研发计划（ ２０ １６ ＹＦＢ１ ０ ０ ０ ８ ０２ ） 、ＧＦ 基础科研重点项目（ ＪＣＫＹ２ ０ １ ６ ２ ０ ３ Ｂ０Ｕ ） 、航空科学基金（ ２０ １ ９ １ ９ ０ ５２ ０ ０ ２ ） 、南京航空航天大学研究生创新基地（ 实验室） 开放基金（ Ｋ ＦＪＪ ２ ０ １ ８ １ ６ ０ ３ ） 资助． 张傅林， 硕士研究生， 中国计算机学会（ ＣＣＦ ） 学生会员， 研究方向为形式化验证、软件工程等． Ｅ－ｍａ ｉ ｌ ：ｍｌ ８ ７ ５ ６ ８ ０ １ ９ ９ ６ ＠ １ ６ ３ ． ｃｏｍ． 杨志斌（ 通信作者）， 博士， 副教授， 中国计算机学会（ ＣＣＦ ） 会员， 研究方向为安全关键软件、形式化验钲等．Ｅ－ ｍａｉ ｌ ： ｙａ ｎｇｚｈｉ ｂ ｉ ｎｌ ６ ８＠ １ ６ ３ ． ｃ ｏｍ． 周勇， 博士， 副教授， 中国计算机学会（ ＣＣＦ＞ 会员， 研究方向为软件工程、形式化方法等？ 马燕蒸， 硕士研究生， 中国计算机学会（ ＣＣＦ） 学生会员， 研究方向为形式化验证、软件工程等． 黄志球， 博士， 教授， 中国计箅机学会（ ＣＣＦ ） 理事， 研究领域为软件工程、形式化方法． 薛垒， 硕士， 髙级工程师， 研究方向为嵌人式软件验证、嵌人式软件系统设计．１ １ 期张博林等：一种面向安全关键软件的ＡＡＤＬ 模型组合验证方法 ２ １ ３ ５ｍ ｏｄｅ ｌ ｓａ ｎ ｄＵＰ ＰＡＡ Ｌ－ ｂａ ｓｅ ｄｃ ｏｍｐ ｏｎ ｅｎ ｔ ｆｕ ｎｃ ｔｉ ｏ ｎａ ｌ ｂ ｅｈ ａ ｖｉ ｏｒｖｅ ｒｉ ｆ ｉｃ ａ ｔ ｉｏ ｎ ， ｔ ｈ ｅ ｒｏ ｃｋ ｅ ｔ  ｌ ａ ｕｎ ｃｈ ｃ ｏｎｔ ｒ ｏ ｌｓｕ ｂｓｙｓｔ ｅ ｍｃａ ｓｅ ｉ ｓ ｕｓ ｅｄｔ ｏｓｈ ｏｗ ｔ ｈ ｅ ｅｆ ｆｅ ｃｔ ｉ ｖｅ ｎｅ ｓ ｓａ ｎｄｌｉ ｍｉ ｔ ａ ｔｉ ｏｎ ｓ ｏｆ ｔｈ ｅｐｒｏ ｐｏ ｓ ｅ ｄｍ ｅ ｔ ｈｏｄ ａ ｒｅｄ ｅｍ ｏｎｓ ｔ ｒａｔ ｅｄ．Ｋ ｅｙｗｏｒｄｓｓ ａ ｆｅ ｔ ｙ－ ｃｒｉ ｔ ｉｃ ａ ｌ ｓｏｆ ｔ ｗａ ｒ ｅ ；ｒ ｏｃｋ ｅｔ ｌ ａ ｕ ｎｃ ｈ ｃｏｎ ｔ ｒｏｌ ｓ ｙｓ ｔｅ ｍ ；ｃｏｍ ｐｏ ｓ ｉｔ ｉ ｏ ｎａ ｌｖｅ ｒ ｉ ｆ ｉ ｃａ ｔ ｉｏ ｎ ；Ａ ＡＤＬ； ＵＰＰＡＡＬｉ 引言安全关键软件（ Ｓａｆ ｅ ｔ ｙ－Ｃｒｉ ｔ ｉ ｃａ ｌＳｏ ｆｔ ｗａ ｒ ｅ ）［ １ ］ 在航天、航空、交通等领域的安全软件系统中有广泛应用，且Ｊｒ 有高安全性的、高可靠性的、交互频繁的、资源受限的、实时响应的特征的软件． 安全关键软件一般为安全关键系统的关键部分， 可能引起或者增加不安全的情况， 这样的软件被认为是安全关键的［ ２ ］．近年来， 基于模型驱动开发方法Ｍ 开发和设计安全关键软件越来越得到重视． 随着功能和非功能的需求的不断提高， 安全关键软件变得越来越复杂，安全关键软件的模型形式化验证面临着巨大的状态空间爆炸问题． 现在， 基于契约的组合验证方法［ ４ ６ ］成为安全关键软件领域解决验证状态空间爆炸问题的国际前沿热点． 其核心思想是利用软件系统的组合结构对验证问题进行分解， 先验证各个子组件的性质， 然后组合推理导出整个系统的性质， 通过分而治之解决状态空间爆炸问题， 这些性质用契约来形式化规约． 该方法的三个关键要素包括软件架构、契约以及组合推理规则．基于契约的组合验证方法在程序语言、模型检测、模型驱动工程、嵌入式系统等领域都得到广泛的研究． 我们的研究是将组合验证引人到安全关键软件领域． 体系结构设计与分析语言Ａ ＡＤＬ［ ７ ８ ］（ Ａｒ ｃｈｉ ｔ ｅ ｃｔ ｕｒ ｅＡｎａｌ ｙ ｓｉ ｓａ ｎｄＤｅ ｓ ｉ ｇｎＬａ ｎｇ ｕａ ｇ ｅ ） 是由美国汽车工程师协会提出的面向安全关键系统的一种建模语言标准， 丰富的可表达方式使得ＡＡ ＤＬ 成为安全关键软件设计与验证方法的一种重要选择，安全关键软件的ＡＡＤ Ｌ 体系结构模型组合验证方法已成为一个重要研究内容． 美国Ｒｏ ｃｋｗｅｌ ｌ Ｃｏ ｌ ｌ ｉ ｎｓ公司和Ｍ ｉ ｎｎ ｅｓ ｏｔ ａ大学在ＤＡ Ｒ ＰＡＭ ＥＴＡＰ ｒｏｇｒ ａｍ项目的支持下， 提出了ＡＡＤＬ 架构模型组合验证方法和环境ＡＧＲＥＥ？９－１１］ （ Ａｓ ｓ ｕｍｅＧ ｕａ ｒａ ｎｔ ｅｅ Ｒｅａ ｓｏｎ ｉｎｇＥｎｖｉ ｒ ｏｎｍ ｅｎ ｔ ） ， 并给出了ＡＡ ＤＬ扩展附件ＡＧＲ ＥＥＡｎ ｎｅ ｘ ． 使用Ａ Ａ ＤＬ 构造系统的体系结构模型， 使用ＡＧ ＲＥ Ｅａ ｎ ｎｅ ｘ 构造各个组件的契约， 然后基于ＡＧＲ ＥＥ 进行组合推理， 将基于契约的组合验证方法引人到安全关键软件领域．但是， 验证在体系结构中一层一层执行， 底层叶子组件契约被组合验证内部抽象其组件行为并默认是正确的， 所以这些组件的功能行为需要在组合验证环境外进行验证． 模型转换是ＡＡ Ｄ Ｌ 模型形式化验证和分析的主要途径， 如转换到ＢＩ Ｐ［ １ ２ ］（ Ｂｅｈａ ｖｉ ｏｒＩｎ ｔｅｒａｃ ｔｉｏｎ Ｐｒｉｏｒ ｉ ｔｙ） 、Ｆ ＩＡＣＲＳ１ ３］、ＴＬＡ＋ ［１ ４ ］、Ｓ ｉ ｇｎ ａｌ＾ １ ５］、Ｓ ｔａ ｔ ｅ ｆ ｕｌＴ ｉ ｍｅ ｄＣＳＰ ［ １ ６ ］（ Ｃｙ ｂ ｅｒ － Ｐｈ ｙ ｓ ｉ ｃａ ｌＳ ｙ ｓｔ ｅｍ ｓ ） 等， 模型转换后可以重用这些模型已有的验证和分析能力． 然而， ＵＰＰ ＡＡＬ［ １ ７ １ ８ ］、Ｓｉ ｍＵ ｌ ｉ ｎ ｋ ［ ｌ ９ ］等验证和分析工具在工业界已有较多使用， 这些工具常用于验证单组件的行为是否满足期望的性质即组件契约， 而组合验证环境则可以进一步基于组件契约进行整个系统的组合推理． 因此， 组合验证环境和工业界已经常用的验证和分析工具的集成是工业界的一个应用需求． 因此， 我们考虑组合验证方法ＡＧＲＥＥ 和ＵＰＰ ＡＡＬ 的结合， 并对工业界实际案例进行验证和分析．本文在已有研究工作的基础上提出了一种组合验证方法， 该方法包括ＡＡＤＬ 体系结构模型的组合验证和基于ＵＰ Ｐ ＡＡ Ｌ 的组件的功能行为验证． 首先， 根据需求分解构造系统的体系结构模型， 根据需求构造组件契约， 基于组件契约对系统的体系结构进行推理， 从而验证复杂系统的体系结构． 然后对组合验证中的叶子组件的功能行为模型进行模型转换， 完成了ＡＡＤ Ｌ 模型子集到ＵＰ Ｐ Ａ Ａ Ｌ 模型的转换， 主要是针对ＡＡＤ Ｌ 子程序和行为附件的转换，然后重用ＵＰ ＰＡＡＬ 的验证能力， 对模型的功能正确性、可达性、安全性等性质进行验证分析， 确保底层叶子组件的功能行为正确性． 通过这种组合验证与模型转换相结合的组合验证方法完成了对整个复杂ＡＡＤＬ 模型的验证与分析．本文是ＭＡＣＡｅ ｒｏｓ ｐａ ｃ ｅ 项目［ ２ 。］ 关于ＡＡ ＤＬ 模２ １ ３ ６计算机学报２ ０２ ０ 年型验证的一部分工作． ＭＡＣ Ａ ｅ ｒ ｏｓ ｐａ ｃ ｅ 项目是一个基于Ａ Ａ Ｄ Ｌ 的建模、验证和代码生成研究项目． 该项目提出了一种基于限定自然语言ＲＮ Ｌ ＣＲ ｅ ｓ ｔ ｒ ｉ ｃ ｔ ｅ ｄＮ ａ ｔ ｕ ｒ ａ ｌＬ ａ ｎｇ ｕ ａｇ ｅ ） 的需求建模方法， 从ＲＮ Ｌ 需求自动生成Ａ Ａ Ｄ Ｌ 模型； 然后对Ａ Ａ ＤＬ 模型精化补充其平台相关信息得到平台执行模型； 之后通过形式化验证方法完成对平台执行模型的验证与分析并将验证结果反馈给Ａ Ａ Ｄ Ｌ 模型， 实现Ａ Ａ Ｄ Ｌ 模型的迭代更新； 最后对验证后的模型进行目标Ｃ ／ Ａ ｄ ａ代码自动生成． Ｍ Ａ Ｃ Ａ ｅ ｒ ｏｓ ｐａ ｃ ｅ 项因的总体结构如图１ 所示， 本文的工作是形式化验证部分．图１Ｍ Ａ Ｃ Ａｅ ｒｏｓ ｐａ ｃｅ 项目总体结构２ 研究背景２ ． １ＡＡＤＬ 语言基本概念在安全关键软件的应用中， 清晰地表达系统的各个组成部分的结构关系十分的重要． Ａ Ａ Ｄ Ｌ 语言是可以描述软件体系结构、硬件体系结构、功能和非功能属性的建模语言． 在软件体系结构上通过线程、线程组、进程、子程序、子程序组等组件以及组件交互进行描述； 在硬件体系结构上通过处理器、虚拟处理器、总线、虚拟总线等组件以及组件交互进行描述； 功能和非功能属性通过分发协议、通信协议、调度策略、模式变换协议以及分区机制等属性进行描述； 最后， 通过系统构件的组合， 能够层次化地建立起系统的体系结构模型． 除此之外， Ａ Ａ ＤＬ 还提供了行为附件（ ｂｅ ｈａ ｖｉ ｏ ｒａ ｎｎ ｅ ｘ ） 增强了对组件的功能行为的描述， 通过行为附件的执行模型能够更加详细地描述线程和子程序的功能行为模型．为了方便后续内容中阐述Ａ ＡＤ Ｌ 组合验证原理， 这里我们给出一个简单的Ａ Ａ ＤＬ 模型示例如表１ 所示， 即一个Ａ Ａ ＤＬ 系统ｔ ｏｐｌ ｅ ｖｅ ｌ ， 它的子构件包括Ａ 、Ｂ 和Ｃ ， 子构件之间的链接为即时通信方式（ ｉｍ ｍｅ ｄ ｉ ａ ｔ ｅ ） ．表１Ａ Ａ Ｕ Ｌ 模型示例ｐ ａ ｃｋ ａ ｇ ｅＩ ｎ ｔ ｅ ｇ ｅｒ 一Ｔ ｏｙｐｕ ｂｌｉ ｃｗ ｉ ｔ ｈＢ ａｓ ｅ＿Ｔ ｙ ｐ ｅ ｓ；ｓ ｙｓ ｔｅ ｍＡｆ ｅａ ｔ ｕｒ ｅｓＩ ｎ ｐ ｕ ｔ＿Ａ ：ｉ ｎｄ ａ ｔ ａｐ ｏ ｒ ｔＢ ａ ｓ ｅ＿Ｔ ｙ ｐ ｅ ｓ Ｉ  Ｉ  Ｉ ｎ ｔ ｅｇ ｅ ｒ；Ｏ ｕ ｔ ｐ ｕ ｔ一Ａ ：ｏ ｕ ｔ ｄ ａ ｔａｐ ｏ ｒ ｔ Ｂａ ｓ ｅ＿Ｔ ｙ ｐｅ ｓ ： ； Ｉ ｎ ｔ ｅｇ ｅ ｒ；ｅ ｎ ｄ Ａ ；ｓ ｙ ｓ ｔｅ ｍＢｆ ｅａ ｔ ｕｒ ｅｓＩ ｎ ｐ ｕ ｔ＿ Ｂ ：ｉ ｎ ｄ ａ ｔａ ｐ ｏ ｒ ｔＢ ａｓ ｅ 一Ｔ ｙ ｐ ｅｓ ： ：  Ｉｎ ｔｅｇ ｅｒ ；？ ｕ ｔ ｐ ｕ ｔ＿ Ｂ： ｏ ｕ ｔ ｄ ａｔ ａ ｐ ｏ ｒ ｔ  Ｂａ ｓ ｅ＿Ｔｙ ｐ ｅ ｓ ： ： Ｉ ｎ ｔ ｅｇｅ ｒ；ｅ ｎ ｄ Ｂ ；ｓ ｙ ｓ ｔｅ ｍＣｆｅａ ｔ ｕｒ ｅｓＩ ｎ ｐ ｕ ｔ ｌ ＿Ｃ： ｉ ｎ ｄ ａ ｔ ａ ｐ ｏ ｒｔＢ ａ ｓ ｅ一Ｔ ｙ ｐ ｅｓ ： ：  Ｉｎ ｔｅ ｇ ｅ ｒ；Ｉ ｎ ｐ ｕ ｔ ２＿Ｃ ： ｉ ｎｄ ａ ｔ ａ ｐ ｏ ｒ ｔＢ ａ ｓ ｅ＿Ｔ ｙｐ ｅ ｓ ： ： Ｉ ｎ ｔｅ ｇ ｅ ｒ；Ｏ ｕ ｔ ｐ ｕ ｔ： ｏ ｕ ｔ ｄ ａｔ ａ ｐｏ ｒｔ Ｂａ ｓ ｅ＿ Ｔｙ ｐ ｅｓ Ｘ Ｉ ｎ ｔ ｅｇ ｅ ｒ ；ｅ ｎ ｄＣ？ｓ ｙ ｓ ｔｅ ｍｔ ｏ ｐ＿ｌ ｅ ｖ ｅｌｆ ｅａ ｔ ｕｒ ｅ ｓＩ ｎ ｐ ｕ ｔ一Ｓ： ｉ ｎ  ｄ ａｔ ａｐ ｏ ｒ ｔ Ｂａ ｓｅ一Ｔ ｙ ｐ ｅ ｓ ： ： Ｉ ｎ ｔ ｅｇ ｅ ｒ ；Ｏ ｕ ｔ ｐ ｕ ｔ一Ｓ ： ｏ ｕ ｔ ｄ ａ ｔａ ｐ ｏ ｒ ｔＢ ａｓ ｅ＿Ｔ ｙ ｐｅ ｓ ： ： Ｉ ｎ ｔ ｅｇ ｅｒ；ｅｎ ｄ ｔ ｏ ｐ一ｌ ｅ ｖ ｅｌ；ｓ ｙ ｓｔ ｅ ｍｉ ｍｐ ｌ ｅｍｅ ｎｔ ａ ｔｉ ｏ ｎ ｔ ｏ ｐ＿ｌ ｅ ｖｅ ｌ ． Ｉｍ ｐ ｌｓ ｕ ｂ ｃ ｏ ｍｐ ｏ ｎ ｅｎｔｓＡ一ｓｕ ｂ：ｓ ｙｓ ｔ ｅｍＡ ；Ｂ＿ ｓｕ ｂ ： ｓ ｙｓｔ ｅｍＢ ；Ｃ＿ ｓｕ ｂ ： ｓ ｙｓ ｔ ｅｍＣ ；ｃｏ ｎ ｎ ｅｃ ｔｉ ｏ ｎ ｓＩ Ｎ＿ＴＯ＿Ａ ： ｐｏ ｒ ｔ Ｉ ｎ ｐ ｕ ｔ一Ｓ —〉Ａ一ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ一Ａ｛ Ｃｏｍ ｍｕ ｎ ｉ ｃａ ｔｉ ｏ ｎ 一Ｐ ｒ ｏ ｐ ｅｒ ｔｉ ｅ ｓ ： ： Ｔ ｉ ｍｉ ｎ ｇ＝〉ｉ ｍｍｅ ｄ ｉ ａｔ ｅ ； ｝ ；Ａ＿ＴＯ＿Ｂ ： ｐ ｏｒ ｔ Ａ＿ｓｕ ｂ ． Ｏ ｕ ｔ ｐ ｕ ｔ＿ Ａ —〉Ｂ＿ｓ ｕ ｂ ． Ｉｎ ｐ ｕ ｔ＿Ｂ｛ Ｃｏｍ ｍｕ ｎ ｉ ｃａ ｔ ｉ ｏ ｎ一Ｐ ｒ ｏ ｐ ｅ ｒｔ ｉ ｅ ｓ ： ： Ｔ ｉ ｍｉ ｎ ｇ＝〉ｉ ｍｍｅ ｄ ｉ ａｔ ｅ； ｝ ；Ａ＿ ＴＯ ＿Ｃ ： ｐ ｏ ｒ ｔ Ａ＿ｓ ｕ ｂ ． （ ） ｕ ｔ ｐ ｕ ｔ＿Ａ —］＞ Ｃ＿ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ ｌ ＿Ｃ｛ Ｃｏｍ ｍｕ ｎ ｉ ｃａ ｔｉｏ ｎ ＿Ｐ ｒ ｏ ｐ ｅ ｒｔｉｅ ｓ ： ： 丁ｉｍｉｎ ｇ＝〉ｉｍｍｅ ｄ ｉａｔ ｅ； ｝ ；Ｂ一ＴＯ＿Ｃ ： ｐ ｏ ｒ ｔＢ＿ ｓｕ ｂ． 〇ｕ ｔ ｐ ｕ ｔ一Ｂ—〉Ｃ＿ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ ２ ＿Ｃ｛ Ｃｏｍ ｍｕ ｎｉ ｃａ ｔ ｉ ｏ ｎ＿Ｐ ｒ ｏ ｐ ｅｒ ｔ ｉ ｅ ｓ ：  ： Ｔ ｉ ｍｉ ｎ ｇ＝〉ｉ ｍｍｅ ｄ ｉ ａｔ ｅ； ｝ ；Ｃ＿ ＴＯ ＿Ｏｕ ｔ ｐ ｕ ｔ： ｐ ｏｒ ｔＣ＿ｓｕ ｂ ． Ｏ ｕ ｔ ｐ ｕ ｔ＿Ｃ —＞ ０ ｕｔ ｐ ｕ ｔ＿Ｓ｛ Ｃｏｍｍ ｕ ｎ ｉ ｃａ ｔｉｏ ｎ ＿Ｐ ｒ ｏ ｐ ｅ ｒｔｉ ｅ ｓ ！ Ｔ ｉ ｍｉ ｎ ｇ＝ ＞ ｉ ｍｍｅ ｄ ｉ ａｔ ｅ ； ｝ ；ｅｎ ｄ ｔ ｏ ｐ＿ ｌ ｅ ｖ ｅｌ． Ｉ ｍｐ ｌ ；ｅｎ ｄＩ ｎｔ ｅｇ ｅｒ＿Ｔ ｏ ｙ ；２ ． ２ 组合验证概述为了验证一个系统满足其需求， Ｈ ａ ｍｍ ｏｎ ｄ 提出了满意度论证的概念［２ ２：， 即通过系统行为的规范和对系统的假设来建立系统需求． 为了形式化满意度参数， 基于契约的组合验证方法提供了一种机制，张博林等：一种面向安全关键软件的Ａ Ａ ＤＬ 模型组合验证方法 ２ １ ３ ７通过对其组件信息的抽象， 从而推导系统级需求是否被满足． 组合验证中组件契约描述如下：Ｃ〇ｎ ｔ ｒ ａＣ ｔ ＝（ Ａ ｓ ｓ ｕ ｍ ｅ ，Ｇ ｕ ａ ｒ ａ ｎ ｔ ｅ ｅ ） ， 其中 Ａ ｓ ｓ ｕｍ ｅ 为组件契约的假设部分， 描述组件对其运行环境的需求， 可以是验证过程中的组件输人的断言或者是不变量； Ｇｕａｒａ ｎｔ ｅ ｅ为组件契约的保证部分， 描述当组件的假设部分被满足时， 组件必须保证的外部行为特征， 即是否满足需求． 契约精确地指定了组件与系统其它部分的交互所需要的信息， 还支持按照系统模型的层次结构对验证部分进行层次分解．在表１ 案例的基础上， 我们给出如下系统验证需求：ｔ ｏ ｐｌ ｅ ｖｅ ｌ ｓｙｓ ｔ ｅｍ 输人小于１ ０ 时， 输出应小于５ ０ ； 子组件Ａ 输人小于２ ０ 时， 输出应小于二倍的输人； 子组件Ｂ 输入小于２ ０ 时． 输出应小于输人值与１ ５ 之和； 子组件Ｃ 输出应小于子系统Ａ 和子系统Ｂ输人数据之和． 根据需求建立组件契约及证明过程如图２ 所示． 表１ 只简单给出了两层结构， 但可以任意多个层次． 从而推广到更复杂的系统验证中．表２Ａ ＧＲ Ｅ Ｅａ ｎ ｎ ｅｘ 示例①ｃ°Ａａ ： Ｉｎｐ ｕｔ ＜２ ０Ｇａ： （ Ｘｉｔ ｐｕ ｔ ＜２＊Ｉ ｎ ｐｕ ｔ－？？Ｂ ？—Ａｃ：ｎ ｏ ｎ ｅＧＡ： Ｏｕ ｔｐｕ ｔ＝Ｉｎ ｐ ｕ ｔ  １＋  Ｉｎ ｐ ｕ ｔ２１Ａ？ ：Ｉ ｎ ｐ ｕｔ ＜２ ０Ｇａ ： Ｏｕ ｔｐ ｕ ｔ＜ Ｉｎｐ ｕ ｔ ＋ １ ５Ａ ｓ ：Ｉ ｎ ｐｕ ｔ ＜１ ０ＪＧｓ：  （） ｕｔ ｐｕ ｔ ＜５ 〇！｜图２ 组合验证案例假设保证推理环境ＡＧ ＲＥ Ｅ 是集成在开源工具ｆｐｌａＯ ＳＡＴＥ（ Ｏｐ ｅｎＳ ｏｕｒ ｃ ｅＡＡＤＬ Ｔｏｏ ｌ Ｅｎ ｖｉ ｒ ｏｎｍ ｅｎｔ ）上的Ａ Ａ ＤＬ 模型的组合验证工具， 并发布了Ａ Ａ Ｄ Ｌ组合验证附件Ａ Ｇ ＲＥ Ｅａ ｎ ｎｅ ｘ 用于构造组件契约．在Ａ ＧＲＥＥ 框架下， Ａ ＡＤＬ 模型使用ＡＧ ＲＥＥ ａｎｎ ｅｘ构造的契约表示组件的功能， 在对系统的分层设计过程中， 当前层的需求在设计下一层组件的时候成为下一层各个组件的需求， 从而下一层组件必须满足当前层的需求， 然后由各个层次不同组件的需求构造相应的组件契约， 最后通过组合推理的方法证明这个系统体系结构的正确性． 表１ 的系统验证需求对应的Ａ Ａ ＤＬ Ａ Ｇ ＲＥ Ｅａ ｎ ｎ ｅ ｘ 表示如表２ 所示？使用Ａ Ｇ ＲＥ Ｅ 可以完成对该模型的验证分析， 确认其需求得到满足．Ａ Ｇ ＲＥ Ｅａ ｎ ｎｅ ｘ 具体语法可参见手册①■ｐ ａｃ ｋ ａｇ ｅＩ ｎ ｔ ｅｇ ｅ ｒ＿ Ｔｏ ｙｐ ｕ ｂ ｌ ｉ ｃｗｉ ｔ ｈ Ｂａ ｓ ｅ一Ｔｙ ｐ ｅ ｓ；ｓｙ ｓ ｔｅ ｍ 八ｆｅ ａｔ ｕ ｒ ｅｓＩｎ ｐ ｕ ｔ： ｉ ｎ  ｄ ａ ｔａ ｐｏ ｒ ｔ Ｂａ ｓ ｅ一Ｔ ｙ ｐ ｅｓ ； ！ Ｉ ｎ ｔ ｅｇ ｅ ｒ；Ｏ ｕ ｔｐ ｕ ｔ：  ｏ ｕｔｄ ａｔ ａ ｐ ｏ ｒｔＢａ ｓ ｅ一Ｔ ｙ ｐ ｅ ｓ ： ： Ｉ ｎ ｔ ｅｇ ｅｒ；ａ ｎ ｎｅｘ  ａｇｒｅ ｅ ｛＊ ＊ａ ｓ ｓ ｕ ｍｅ“Ａｉ ｎ ｐ ｕ ｔ ｒ ａ ｎ ｇｅ” ：Ｉ ｎ ｐ ｕ ｔ ＜ ２ ０；ｇ ｕ ａ ｒａ ｎ ｔ ｅ ｅ“Ａ  ｏ ｕ ｔ ｐ ｕ ｔｒ ａ ｎｇ ｅ”：Ｏ ｕ ｔ ｐ ｕ ｔ ＜Ｃ ２＊ Ｉ ｎ ｐ ｕ ｔ；＊ ＊｝ ；ｅｎ ｄ Ａ ；ｓｙｓ ｔｅ ｍＢｆｅａ ｔ ｕ ｒｅ ｓＩ ｎ ｐ ｕ ｔ： ｉ ｎ  ｄ ａ ｔａｐ ｏ ｒｔ Ｂａ ｓｅ一Ｔ ｙ ｐ ｅｓ ： ：  Ｉ ｎ ｔｅ ｇ ｅ ｒ ；Ｏｕ ｔ ｐ ｕ ｔ： ｏ ｕ ｔ ｄ ａ ｔａ ｐ ｏ ｒｔ Ｂ ａ ｓ ｅ一Ｔ ｙ ｐ ｅ ｓ ： ： Ｉ ｎ ｔ ｅｇ ｅ ｒ ；ａ ｎ ｎ ｅｘ  ａｇｒ ｅ ｅ ｛＊ ＊ａ ｓ ｓ ｕ ｍｅ“ Ｂ ｉ ｎ ｐ ｕ ｔｒ ａ ｎ ｇ ｅ”： Ｉ ｎ ｐ ｕ ｔ ＜ ２ ０；ｇ ｕａｒａ ｎ ｔｅｅ＊＊Ｂ ｏ ｕ ｔ ｐ ｕ ｔ ｒ ａｎｇｅｗ ：Ｏ ｕ ｔｐ ｕ ｔ ＜ Ｃ Ｉ ｎ ｐ ｕ ｔ － ｆ１ ５； ＊ ＊｝ ；ｅ ｎｄ Ｂ ；ｓ ｙ ｓ ｔｅ ｍＣｆ ｅａ ｔ ｕ ｒ ｅｓＩ ｎ ｐ ｕｔ  １： ｉ ｎ  ｄ ａｔ ａｐ ｏ ｒｔ Ｂａ ｓ ｅ一Ｔｙ ｐ ｅｓ ： ： Ｉｎ ｔ ｅｇ ｅｒ ；Ｉ ｎ ｐ ｕ ｔ ２ ： ｉ ｎ ｄ ａｔ ａｐ ｏ ｒｔ Ｂａ ｓ ｅ一Ｔｙ ｐｅ ｓ ： ： Ｉｎ ｔ ｅｇ ｅｒ ；Ｏｕ ｔ ｐ ｕ ｔ： ｏ ｕ ｔ ｄ ａ ｔ ａ ｐｏ ｒ ｔＢ ａ ｓ ｅ＿Ｔ ｙ ｐ ｅ ｓ＊ Ｉ  Ｉ ｎ ｔ ｅｇ ｅ ｒ ；ａ ｎ ｎ ｅｘ ａ ｇｒ ｅ ｅ｛ ＊ ＊ｇｕ ａｒａ ｎ ｔｅｅ“Ｃｏ ｕ ｔ ｐ ｕｔ ｒ ａ ｎｇ ｅ”： Ｏ ｕ ｔ ｐｕ ｔ： Ｉ ｎｐ ｕ ｔ ｌ ＋ Ｉｎ ｐｕ ｔ２ ； ＊ ＊；：ｅｎ ｄ Ｃ ；ｓ ｙｓ ｔｅｍｔ ｏ ｐ＿ｌ ｅ ｖｅ ｌｆ ｅａ ｔ ｕｒ ｅｓＩ ｎ ｐ ｕ ｔ ： ｉ ｎ ｄ ａ ｔ ａｐ ｏ ｒ ｔ Ｂ ａ ｓ ｅ＿Ｔ ｙ ｐ ｅ ｓ！ ； Ｉ ｎ ｔ ｅｇ ｅ ｒ；Ｏｕ ｔ ｐ ｕ ｔ：ｏ ｕ ｔ ｄ ａ ｔａ ｐ ｏ ｒ ｔＢａｓ ｅ＿Ｔ ｙ ｐ ｅｓ Ｉ  ；  Ｉ ｎ ｔｅ ｇ ｅ ｒ；ａ ｎ ｎ ｅｘ ａ ｇ ｒ ｅ ｅ｛ ＊  ＊ａｓ ｓ ｕｍｅ“Ｓｙ ｓ ｔｅ ｍｉ ｎ ｐ ｕ ｔｒ ａ ｎ ｇ ｅ”： Ｉ ｎ ｐ ｕ ｔ ＜＝９ ；ｇ ｕａ ｒａ ｎ ｔｅ ｅ＇＇Ｓ ｙ ｓ ｔ ｅｍｏ ｕ ｔ ｐ ｕ ｔｒａ ｎ ｇ ｅ＊＊：Ｏ ｕ ｔ ｐ ｕ ｔ ＜Ｃ  ５ ０；＊ ＊｝ ；ｅｎ ｄ ｔ ｏ ｐ＿ｌ ｅ ｖｅ ｌ ；ｓ ｙｓ ｔｅｍ ｉ ｍｐ ｌｅ ｍｅ ｎ ｔａ ｔ ｉ ｏ ｎ ｔ ｏ ｐ ＿ｌ ｅｖ ｅ ｌ． Ｉ ｍｐ ｌｓ ｕ ｂ ｃｏ ｍ ｐ ｏｎ ｅ ｎ ｔｓＡ ＿ｓ ｕ ｂ ： ｓ ｙ ｓ ｔｅｍ Ａ ；Ｂ＿ｓ ｕ ｈ： ｓｙ ｓ ｔ ｅｍＢ ；Ｃ＿ ｓ ｕ ｂ ： ｓｙｓｔ ｅｍ Ｃ ；ｃｏ ｎ ｎ ｅｃｔｉｏ ｎ ｓＩ Ｎ＿Ｔ Ｏ＿Ａ ：ｐ ｏ ｒ ｔ Ｉｎ ｐ ｕ ｔ—〉Ａ＿ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ｛ Ｃｏｍｍｕ ｎ ｉ ｃａ ｔｉ ｏ ｎ ＿ Ｐｒ ｏ ｐ ｅ ｒ ｔｉ ｅ ｓ ： ： Ｔ ｉｍ ｉ ｎ ｇ＝〉ｉ ｍｍ ｅｄｉ ａ ｔｅ ； ｝ ；Ａ＿Ｔ Ｏ一Ｂ ： ｐ ｏｒ ｔＡ＿ｓｕ ｂ ． Ｏ ｕ ｔ ｐ ｕ ｔ—〉Ｂ＿ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ｛ Ｃｏ ｍｍｕ ｎ ｉ ｃ ａ ｔｉ ｏ ｎ 一Ｐ ｒ ｏ ｐ ｅ ｒ ｔｉ ｅ ｓ ： ： Ｔ ｉｍ ｉ ｎ ｇ＝〉ｉ ｍｍ ｅｄ ｉ ａ ｔ ｅ ； ｝ ；Ａ＿Ｔ Ｏ＿Ｃ ： ｐ ｏ ｒ ｔＡ＿ｓ ｕ ｂ ． Ｏ ｕ ｔ ｐ ｕ ｔ—＞Ｃ＿ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ ｌ｛ Ｃｏｍｍｕ ｎ ｉ ｃａ ｔ ｉｏ ｎ ＿ Ｐ ｒｏ ｐ ｅｒ ｔｉ ｅ ｓ ： ： Ｔ ｉｍ ｉ ｎ ｇ＝〉ｉ ｍｍ ｅｄｉ ａ ｔｅ ；Ｂ一ＴＯ＿Ｃ ： ｐ ｏｒ ｔＢ一ｓｕ ｂ ． Ｏ ｕ ｔ ｐ ｕ ｔ—〉Ｃ＿ ｓ ｕ ｂ ． Ｉ ｎ ｐ ｕ ｔ ２｛ Ｃｏ ｍｍ ｕ ｎｉｃａ ｔｉｏ ｎ＿ Ｐ ｒｏ ｐ ｅ ｒ ｔｉ ｅ ｓ ： ： Ｔ ｉｍｉ ｎ ｇ＝〉ｉｍｍ ｅｄ ｉ ａ ｔｅ ；｝；Ｃ一丁Ｃ）＿Ｏ ｕ ｔ ｐ ｕ ｔ： ｐ ｏｒ ｔＣ一ｓ ｕ ｂ ． Ｏ ｕ ｔ ｐ ｕ ｔ—＞ Ｏｕ ｔ ｐ ｕ ｔ｛ Ｃｏ ｍｍｕ ｎ ｉ ｃａ ｔｉ ｏ ｎ一Ｐｒ ｏ ｐ ｅ ｒ ｔｉ ｅ ｓ ： ： Ｔ ｉｍ ｉ ｎ ｇ＝〉ｉ ｍｍ ｅｄ ｉ ａ ｔｅ ：；ｅｎ ｄ ｔ ｏ ｐ＿ｌ ｅ ｖｅ ｌ ． Ｉ ｍｐ ｌ；ｅｎ ｄ Ｉ ｎ ｔ ｅｇ ｅ ｒ＿ Ｔｏ ｙ ；２ ． ３Ｕ ＰＰＡＡ Ｌ概述ＵＰ Ｐ ＡＡ Ｌ［ ？ 是一个依靠时间自动机进行验证分析的验证环境， 可以构造时间自动机网络模型对实时系统进行建模、模拟和验证． 在Ｕ ＰＰＡ Ａ Ｌ 中进行的模型验证的理论基础是自动机中的可达性验证理论， 依据该理论可以验证模型中所有状态在可达路径上的性质集合． 若用Ｍ 来表示一个时间状态自动机， 用ｉ？ 表示验证过程中用到的时序逻辑， 在验①Ａｓ ｓ ｕ ｍｅ Ｇ ｕ ａ ｒａ ｎ ｔ ｅｅ Ｒ ｅａ ｓ ｏ ｎ ｉ ｎ ｇ  Ｅｎ ｖｉ ｒ ｏ ｎ ｍｅ ｎ ｔ（ Ａ Ｇ Ｒ ＥＥ ） ．ｈ ｔ ｔ ｐ ： ／ ／ ｌ ｏ ｏ ｎ ｗ ｅｒ ｋ ｓ ． ｃｏ ｍ ／ ｔｏ ｏ ｌ ｓ ／ ａｇ ｒｅ ｅ ． ｈ ｔ ｍ ｌ． ２ ０ １ ９ ， ０ ８ ， ２ ４１ １ 期＆－ ＊ＡｇｘＢｔ＜＜＼＼＼＼ＡＧＧＧ２ １ ３ ８ 计 算 ２ ０ ２ ０ 年证过程中， 会搜索所有的Ｍ 的状态， 而且会验证Ｒ在搜索过程中经过的每一条可达的路径． 验证需求的ｉ？ 必须使用特定的形式化描述， 在ＵＰ ＰＡ Ａ Ｌ 中使用了一个简化版的时序逻辑ＴＣ Ｔ Ｌ 对表示的．一个ＴＣ Ｔ Ｌ 公式可以验证模型中某个状态是否存在， 比如ｘ＝ ＝３ 在任何工等于３ 上的状态为真． 所有的状态公式和状态转移都不能更改状态机中的表达式， 状态公式可以析取． 表３ 给出了ＵＰ ＰＡ Ａ Ｌ 支持的ＴＣ Ｔ Ｌ 公式及其能力， 使用这些公式可以完成对模型的可达性、活性、安全性等性质的验证．表３ 路径公式公式类型 公式表示 说明可达性公式 ＥＯ＜ｐ表示状态公式９ 是从初始位置可达的， 比如“初始状态一定是可达的活性公式 Ａ ＜  ） ＜ｐ活性表示在某种情况下，一个事情最终一定发生， 通常表述为“ 好事” 会发生．Ａ〈〉９？ 表示最终一定满足安全性公式Ａ ［］ 炉Ｅ ［２ ＜ｐ安全性是指在某种情况下，一件事永远都不会发生，一般用来表达不希望出现的事情， 因此安全性也可以表述为“ 坏事”不会发生． Ａ ［ ］ ｐ 表示在所有可达的所有状态中都应该满足而表示有一条路径上的状态都满足＆２ ． ４ 面向安全关键软件的ＡＡＤ Ｌ 模型组合验证方法研究框架已有的验证方法往往是将扁平化的整个ＡＡＤＬ模型进行模型转换然后直接验证， 但是对工业界复机学报杂的Ａ Ａ Ｄ Ｌ 模型直接验证往往存在状态空间爆炸的问题． 工业界的Ａ Ａ Ｄ Ｌ 模型涉及到大量的函数调用行为， 在Ａ Ａ Ｄ Ｌ 模型中可以使用子程序及行为附件来表达， 但是现有的验证手段很少涉及对子程序及其行为附件的验证分析． 因此， 为了更好的完成对复杂系统的验证分析， 本文提出了一种面向安全关键软件的Ａ Ａ ＤＬ 模型组合验证方法． 该方法总体框架如图３ 所示， 包括三部分：（ １ ） 提出ＡＡ Ｄ Ｌ 体系结构模型的组合验证方法， 根据需求及需求分解使用Ａ Ａ ＤＬ 层次化的构建体系结构模型， 同时确定其组件划分， 使用需求及子需求构造组件的契约， 基于组件契约对系统的体系结构模型进行组合验证， 验证系统体系结构的正确性．（ ２ ） 提出基于ＵＰＰＡＡＬ 的组件功能行为验证方法， 基于模型转换语言ＡＴ Ｌ （Ａ ｔ ｌ ａ ｓＴ ｒ ａｎ ｓ ｆｏ ｒｍ ａｔ ｉ ｏ ｎ１＾ 吨１＾昭６ ）［２ ３］ 将单组件ＡＡＤ Ｌ 模型（ 主要是子程序）转换为Ｕ Ｐ Ｐ ＡＡ Ｌ 模型． 根据Ａ Ａ Ｄ Ｌ２ ＵＰ Ｐ ＡＡ Ｌ 的模型转换方法， 将Ａ ＡＤ Ｌ 组件功能行为模型（ 主要是子程序和行为附件） 转换为Ｕ ＰＰ Ａ Ａ Ｌ 模型并进行验证分析， 从而验证叶子组件的功能行为的正确性．（ ３ ） 实现了Ａ Ａ Ｄ Ｌ 模型验证原型工具， 用于支持Ａ Ｇ ＲＥ Ｅ 组合验证和Ｕ ＰＰ ＡＡ Ｌ 的组件功能行为验证， 并通过插件技术集成在ＡＡ ＤＬ 建模工具Ｏ ＳＡ ＴＥ± ，面向安全关键软件的ＡＡＤ Ｌ模型组合验证方法图３ 面向安全关键软件的Ａ Ａ Ｄ Ｌ 模型组合验证方法框架张博林等：一种面向安全关键软件的１ １ 期 ＡＡＤＬ 模型 组合验证方法 ２ １ ３９３Ａ ＡＤＬ 的体系结构模型的组合验证方法一个复杂的系统需求需要对其进行分解并分配给不同的子系统， 体系结构的分解同时涉及到需求和体系结构， 体系结构的可能会影响需求分配给每一个子系统， 所以在分解的同时需要确定需求分配给子系统的架构能否满足系统级需求， 确定子系统架构的建立对系统环境是否有改变［ ３ ４ ］， Ａ ＡＤ Ｌ 建模语言可以完成复杂系统的体系结构建模需求．３ ． １ 基于ＡＡＤＬ 的火箭发射控制子系统体系结构建模火箭发射系统是在用来控制火箭执行各项操作以及包含火箭自主执行的部分发射功能的系统， 控制从接收到发射的指令一直持续到火箭顺利离开发射装置． 经过简化的火箭发射系统的结构如图４ 所示， 主要包括发控单元计算机、火箭供电机箱、供电控制组合、点火控制组合等组成， 本文主要介绍的火箭发射控制子系统在发控单元计算机中运行． 火箭发射控制子系统的功能主要是根据主控任务的控制命令， 进行相应的命令的执行， 是处于发控单元计算机中过程层的控制系统．图４ 火箭发射系统结构图火箭发射控制系统的需求Ｓ Ｒ 为： 首先打开排气盖和箭舱盖， 执行火箭发射准备命令， 同时进行火箭加电控制， 然后解锁箭舱和安全机构， 最后执行火箭点火命令． 如果执行过程中出现故障， 则进行断电控制． 经过对系统的功能行为详细分析之后， 对系统需求进行分解， 可以得到以下子系统需求：（ １ ） 排气盖控制ＳＲ １ ． 收到排气盖开／关盖控制命令， 执行排气盖开／ 关盖控制， 如果排气盖状态查询正常， 回告发控系统排气盖开／ 关盖控制执行成功； 如果排气盖状态查询异常， 则回告发控系统排气盖故障．（ ２ ） 箭舱盖控制ＳＲ２ ． 收到火箭舱盖开／关盖控制命令， 执行箭舱盖开／关控制， 如果箭舱盖状态查询正常， 回告发射控制系统箭舱盖控制执行成功； 如果箭舱盖状态查询异常． 则回告发控系统箭舱盖故障．（ ３ ） 火箭发射准备／ 取消控制Ｓ Ｒ ３ ． 收到火箭发射准备／ 取消控制命令， 进行火箭发射准备／ 取消控制， 如果闭合级电路状态查洵正常， 回告发射控制系统火箭发射准备／ 取消控制执行成功； 如果闭合级电路状态查询异常， 则回告发控系统火箭发射准备／ 取消异常．（ ４ ） 火箭加电控制ＳＲ ４ ． 收到火箭加电命令， 如果加电自检正常则进行火箭加电控制， 回告发控系统火箭加电行成功； 如果加电自检异常， 则进行断电控制， 回告发射控制系统异常．其余子需求为： 箭舱解锁／ 锁定控制Ｓ Ｒ５ 、热电池激活控制ＳＲ６ 、安全机构解锁／恢复控制Ｓ Ｒ ７ 、火箭点火控制ＳＲ８ 、火箭断电控制Ｓ Ｒ ９ ， 这里就不再赘述． 构造火箭发射控制系统的Ａ Ａ Ｄ Ｌ 模型如图５所示．图５ 火箭发射控制子系统体系结构为了说明与火箭发射控制子系统的需求分解与体系结构分解的关系， 本文以火箭加电控制Ｓ Ｒ ４ 为例说明对需求的进一步细化分解． 火箭加电控制由火箭加电１ 控制ＳＲ ４ Ｃ １ 、火箭加电２ 控制ＳＲ ４ Ｃ２ 和火箭加电３ 控制Ｓ Ｒ ４ Ｃ ３ 三个子组件组成， 每一个加电控制是针对不同的电池组件进行控制， 火箭在进行加电控制时， 正常情况下是按照严格的加电顺序进行加电， 否则会回告加电错误． 下一层以火箭加电１ 控制为例可以分解为火箭加电１ 函数Ｓ Ｒ４Ｃ １ Ｈ １ 、火箭自检结果查询函数ＳＲＣ １ Ｈ ３ 和火箭类型识别码查询函数ＳＲ Ｃ １ Ｈ ４ ； 这一层还能够进一步划分，以火箭自检结果查询函数为例可以划分为单步自检看门狗函数ＷＤＳ Ｅ 、单步自检函数ＳＳ Ｅ 、连续自检看门狗函数ＷＤ ＳＩ 以及连续自检函数Ｓ ＳＩ． 此时对模型已经细化到了子程序层面， 其体系结构如图６ 所示．２ １ ４ ０ 计算机学报 ２ ０ ２ ０ 年丨冬丨６ 火箭发射控制子系统体系结构模型３ ． ２ 基于契约的需求形式化复杂安全关键软件的层次分解涉及到需求分解和体系结构模型， 在３ ． １ 节中层次的构造其体系结构模型后， 如果对体系结构模型进行组合验证， 需要把系统各个层次的组件需求形式化为组件契约． 即抽象的外部可见行为， 本节主要介绍基于契约的需求形式化．由于自然语言需求描述不精确的问题． 把一个需求抽象为一个契约， 首先要明确其输入输出， 然后忽略其内部行为， 将组件抽象为黑盒， 最后明确组件的输入输出关系， 然后构造组件契约． 本节以火箭加电控制子系统的需求及其需求分解为例构造其契约．首先需要说明一个控制命令应该由火箭模式（ 单步或连续） 、火箭状态（ 正常态或训练态） 、操作命令、火箭码等数据组成，一个控制命令会由获取控制命令子程序进行分解． 然后返回具体命令到调用该子程序的组件中． 本文为了表达的简洁， 在叙述需求时不再对控制命令进行详细介绍．根据上节的介绍可以知道， 火箭加电控制的需求为Ｓ Ｒ４ ， 其需求和体系结构分解为： 加电１ 控制ＳＲ４ Ｃ１ 、加电２ 控制ＳＲ４Ｃ２ 和加电３ 控制ＳＲ ４Ｃ３ ，每个子系统应完成相应的加电控制． 而此需求描述实际上涵盖了子系统中组件的功能， 根据需求ＳＲ４其输入为： 火箭发射控制系统的加电命令． 输出为：加电命令的执行结果、是否发出断电令以及断电码．输人输出关系为： 输人正确的加电令且子系统反馈正常， 回告加电命令执行成功， 不发出断电令及断电码； 如果输人错误加电令或子系统反馈故障， 回告加电命令执行错误， 发出断电令以及断电码． 形式化为契约Ｓ Ｒ４ Ｇ 如图７ 所示．ｇ ｉｍｒａ ｎ ｔ ｅｅ“ 根据火箭发射控制系统的命令． 进行相应的命令执行， 否则输出断电令以及断电码”：（ ｃｈｅ ｃｋ＿ ｐ ｏ ｗ ｅｒ ｕ ｐ ＝ ＞ｏ ｕ ｔｐ ｕ ｔ＿ｉ ｓ＿ｓ ｕ ｃｃ ｅｓｓ ＝ ｔ ｒ ｕｅ ａ ｎｄｏ ｕ ｔ ｐ ｕ ｔ＿ ｐｏ ｗ ｅ ｒ＝ ｆａ ｌ ｓｅ ａ ｎ ｄ ｏ ｕ ｔ ｐ ｕ ｔ＿ｐ ｏｗｅｒ＿ｏｆ ｆ＝ｐ ｏｗ ｅｒ ｄ ｏ ｗ ｎ）ｏ ｒ（ ｎ ｏ ｔｃ ｈ ｅｃ ｋ一 ｐ ｏ ｗｅ ｒ ｕ ｐ ＝ 〉ｏ ｕ ｔ ｐ ｕ ｔ＿ｉ ｓ 一ｓｕ ｃ ｃ ｅｓ ｓ＝ ｆａ ｌ ｓ ｅ ａ ｎ ｄｏ ｕ ｔｐ ｕ ｔ＿ ｐｏ ｗ ｅ ｒ＝ ｔｒｕ ｅ ａ ｎ ｄ ｏ ｕ ｔ ｐ ｕ ｔ一ｐｏ ｗｅ ｒ＿ ｏ ｆ ｆ＝ ｐ ｏ ｗｅ ｒｄ ｏ ｗｎ ） ；图７ 火箭加电控制组件契约ＳＲ４ Ｇ火箭加电１ 控制的需求为Ｓ Ｒ４ Ｃ １ ， 同样的， 其耑求分解为： 火箭加电１ 函数Ｓ Ｒ４ Ｃ １ Ｈ １ 、火箭自检结果查询阐数ＳＲ ４  Ｃ １ Ｈ ２ 和火箭类型识别码杳询函数ＳＲ４Ｃ １ Ｈ３ 来具体完成， 其需求描述包含了子组件的行为． 根据需求ＳＲ４ Ｃ１ 可以得到输人为： 火箭加电１ 令（ 单步） 或火箭准备令（ 连续）． 输出为： 加电１指令执行结果、已加电码、是否发出断电令以及断电码． 输人输出关系为： 输人火箭加电１ （ 单步） 或者火箭准备令（ 连续） 且子系统反馈正常， 回告火箭加电１执行成功， 断电令及断电码不发出； 如果输入命令错误或子系统反馈故障， 则回告火箭加电１ 执行层故障， 断电令发出且断电码为断电１． 形式化其需求ＳＲ４ Ｃ１ Ｇ 如图８ 所示．ｇ ｕ ａｒａ ｎ ｔ ｅｅ“ 输人火箭加电１ 令或者火箭准备令， 返回加电１ 指令执行结果”：（ ｃ ｈｅｃｋ ＿ ｏｕ ｔ ｐｕ ｔ＿ ｓｕ ｃ ｃｅｓ ｓ ＝ ＞ ｏ ｕ ｔｐ ｕ ｔ＿ ｉ ｓ＿ ｓｕ ｃｃ ｅｓｓ ＝ｔ ｒｕ ｅ ） ｏｒ（ ｎ ｏ ｔｃ ｈ ｅｃ ｋ＿ｏ ｕ ｔ ｐ ｕ ｔ＿ｓ ｕ ｃ ｃｅｓ ｓ＝＞ ｏ ｕ ｔ ｐｕ ｔ＿ｉｓ＿ｓｕ ｃｃ ｅｓ ｓ＝ｆａ ｌ ｓｅ ）；ｇ ｕａ ｒａ ｎ ｔｅ ｅ“ 执行完成后反馈加电１ 已加电”：（ ｏ ｕ ｔ ｐ ｕ ｔ＿ ｉｓ＿ ｓ ｕ ｃ ｃ ｅｓ ｓ＝〉ｏ ｕ ｔ ｐ ｕ ｔ ４＿ ｐ ｏ ｗ ｅｒ ｕ ｐ＝ｅ ｎ ｕｍ （ Ｄ ａ ｔａ＿Ｔ ｙ ｐ ｅｓ ：  ？？ｐ ｏ ｗｅ ｒ ｕ ｐ＿ｏ ｎ ， ｐ ｏ ｗ ｅ ｒ ｕ ｐ ｌ ） ） ｏ ｒ（ ｏ ｕｔｐ ｕ ｔ＿ｉ ｓ ＿ｓｕ ｃｃｅｓｓ＝〉ｏ ｕ ｔ ｐ ｕｔ ４＿ ｐｏｗｅ ｒ ｕ ｐ＝ｅｎ ｕｍ （ Ｄａｔ ａ一Ｔｙ ｐｅｓ ： ：ｐ ｏｗ ｅ ｒ ｕ ｐ＿ ｏ ｎ，ｎ ｕｌ ｌ ） ）；ｇ ｕａ ｒａ ｎ ｔ ｅ ｅ？ ？ 断电令是否发出”：（ ｏ ｕ ｔ ｐ ｕ ｔ＿ ｉ ｓ＿ｓ ｕ ｃｃ ｅｓｓ ＝ ＞ｏ ｕ ｔ ｐ ｕ ｔ＿ ｐｏｗ ｅ ｒ ＝ ｔ ｒ ｕｅ ）ｏ ｒ （  ｎ ｏｔｏ ｕ ｔ ｐ ｕ ｔ 」ｓ ＿ｓ ｕ ｃ ｃｅｓ ｓ＝＞ ｏ ｕ ｔ ｐ ｕ ｔ＿ ｐ ｏｗｅ ｒ＝ｆ ａ ｌｓ ｅ ）；ｇ ｕａ ｒ ａ ｎ ｔｅ ｅ“ 断电令发出则为断电１ 否则为断电令为ｎ ｕ ｌ ｌ”：ｉ ｆ ｏ ｕ ｔ ｐ ｕ ｔ＿ ｐｏ ｗ ｅ ｒｔ ｈ ｅ ｎｏ ｕ ｔ ｐ ｕ ｔ＿ ｐｏ ｗｅ ｒ＿ｏ ｆｆ＝ｅ ｎ ｕｍ（Ｄ ａｔａ 一Ｔｙ ｐ ｅ ｓ ： ：ｐ ｏｗｅ ｒｕ ｐ＿ ｄｏ ｗ ｎ ，ｐ ｏｗ ｅ ｒ ｄｏｗ ｎ ｌ ）ｅ ｌ ｓ ｅｏ ｕ ｔ ｐ ｕ ｔ＿ ｐｏ ｗｅ ｒ＿ ｏ ｆｆ＝ｅ ｎ ｕｍ （ Ｄａｔ ａ＿Ｔｙ ｐ ｅｓ ： ： ｐ ｏｗｅｒ ｕ ｐ一ｄ ｏ ｗｎ ， ｎｕ ｌ ｌ ）；图８ 火箭加电１ 控制组件契约Ｓ Ｒ ４Ｃ １ Ｇ根据耑求火箭加电１ 函数的需求Ｓ Ｒ４Ｃ １ Ｈ １ 得到其输人为： 加电１ 指令（ 单步） 或火箭准备令（ 连续） ；输出为： 加电１ 函数控制结果、回告系统的加电１ 函数控制结果、训练态的加电１ 控制结果． 输入输出关系为： 如果指令正确且满足发控表， 正常态下向自检函数发送加电１ 控制成功， 回告发控系统加电１ 控制已执行， 训练态下直接回告发控系统加电１ 控制执行结果； 如果指令正确或者不满足发控表， 则向自检函数发送加电１ 控制失败， 回告发控系统加电１控制故障． 形式化其需求Ｓ Ｒ ４ Ｃ １ Ｈ １ Ｇ 如图９ 所示．张博林等：一种面向安全关键软件的１ １ 期 ＡＡＤＬ 模型 组合验证 方法 ２ １ ４ １ｇｕ ａ ｒ ａ ｎ ｔ ｅｅ“ 指令是否是供电１ 指令（ 单步） 或加电命令（ 连续） ， 满足发控表则反馈执行成功”：（ ｃｈ ｅｃ ｋ＿ ｐ ｏｗ ｅｒ ｕ ｐ ｌ＝＞ ｏ ｕ ｔ ｐ ｕ ｔ＿ｉ ｓ＿ｓ ｕ ｃｃｅ ｓｓ＝ ｔｒ ｕｅ ）  ｏ ｒ  （ ｎ ｏｔｃｈ ｅ ｃ ｋ＿ ｐ ｏ ｗｅｒ ｕ ｐ ｌ ＝〉ｏ ｕ ｔ ｐ ｕ ｔ＿ ｉｓ＿ｓ ｕ ｃｃｅ ｓ ｓ＝ ｆ ａｌ ｓ ｅ ）；ｇｕ ａ ｒａ ｎ ｔｅ ｅ“回告系统加电１ 函数结果”：ｏ ｕ ｔ ｐ ｕ ｔ一ｉ ｓ＿ ｓ ｕ ｃ ｃｅ ｓ ｓ—〉ｏ ｕ ｔ ｐ ｕ ｔ＿ ｉ ｓ— ｓ ｕｃ ｃｅ ｓ ｓ一ｓｙ ｓｔ ｅｍ ；ｇｕ ａ ｒａ ｎ ｔｅ ｅ“如果是训练态， 模拟返回加电１ 结果”：ｃｈｅ ｃ ｋ＿ｔ ｒ ａｉ ｎ —〉ｏ ｕ ｔ ｐ ｕ ｔ＿ｉ ｓ一ｔ ｒ ａ ｉ ｎ；图９ 火箭加电１ 函数组件契约Ｓ Ｒ４Ｃ １ Ｈ １ Ｇ吴似的将火箭加电控制１ 控制的体系结构模型中各个组件的需求形式化为组件契约， 增加组件与组件之间的约束， 可以使用组合推理的方式完成对火箭加电１ 控制子系统的体系结构进行验证， 证明其系统需求在该体系结构下得到满足．３ ． ３ 基于ＡＧＲ ＥＥ 的体系结构模型验证根据上述方法， 构造火箭加电控制子系统的体系结构如图１ ０ 所示， 在火箭加电控制子系统中． 包含火箭加电１ 控制、火箭加电２ 控制、火箭加电３ 控制三个子系统， 三个子系统结构相似， 针对不同的三个硬件供电模块而做出不同的加电控制， 同时回告火箭发射控制系统控制命令执行结果．模式状态加电令火箭码图１ ０ 火箭加电控制子系统的体系结构图火箭力卩电控制子系统Ａ ＧＲＥ Ｅｃ ｏ ｕｎ ｔ ｒａｃ ｔ火箭加电３ 控制火箭加电２控制１火箭加电１ 控制ＡＧ ＲＥＥ ｃ ｏｕｎ ｔｒａｃ ｔＳＲ ４Ｃ １ Ｈ１ ＳＲ４ Ｃ１Ｈ２ ＳＲ４ Ｃ１ Ｈ３ＡＧ Ｋ Ｋ Ｋ ｃｏ ｕ ｎ ｔ ｒ ａｃ ｔ？？ 执行结果＞断电信号？ 断电令使用假设保证推理环境ａ ｇ ｒｅｅ 对火箭加电控制子系统进行组合推理， 其结果图１ １ 所示； 根据其组合验证结果， 可以得知， 火箭加电控制子系统的组合验证共涉及６ ４ 个组合推理， 其中系统级契约ＳＲ４ Ｇ 得到满足， 其子组件契约Ｓ Ｒ４ Ｃ １ Ｇ、ＳＲ ４ Ｃ２ Ｇ 、ＳＲ４ Ｃ３Ｇ 以及其子组件契约等经过组合推理之后证明其正确性． 由此可知火箭加电控制子系统在该体系结构模型下的系统需求及其子需求都得到了满足．Ｐｒ ｏ ｂｌｅ ｍｓ二 Ｐ ｒ ｏｐｅ ｒ ｔ ｉｅｓＡ Ａ Ｄ Ｌ Ｐ ｒ ｏｐ ｅ ｒ ｔｙ Ｖ ａｌ ｕ ｅ ｓ．．Ｐ ｒ ｏｇｒ ｅｓ ｓ＾Ａ ＧＲ Ｅ Ｅ Ｒｅ ｓ ｕ ｌ ｔ ｓ ：ＳＣ ｏｎ ｓ ｏｌ ｅＰ ｒ ｏｐｅｒ ｔｙＲｅｓｕ ｌ ｔｖＶ ｅ ｒ ｉ ｆ ｉ ｃ ａ ｔ ｉｏ ｎ ｆ ｏｒ  ＴｏｐＬｅｖｅｌ Ｓｙｓ ． ｉ ｍｐ Ｉ ６４Ｖａ ｌ ｉｄｖ ｖ Ｃｏ ｎｔ ｒａ ｃｔ Ｇ ｕ ａｒａ ｎ ｔｅ ｅｓ ２ Ｖａ ｌ ｉｄｖＳ ｕ ｂｃ ｏｍ ｐｏ ｎｅｎ ｔ Ａｓｓ ｕｍｐｔ ｉ ｏｎ ｓ Ｖ ａｌ ｉｄ（Ｏｓ）福据火箭发射控制系统的命今， 进行招应的命令执行， 否則输出断电令以及断电码 Ｖ ａｌ ｉｄ（Ｏｓ）ｖ Ｔｈｉ ｓ ｃ ｏｍｐｏｎ ｅ ｎ ｔ  ｃｏ ｎｓｉ ｓ ｔ ｅｎ ｔ １ Ｖａ ｌ ｉｄＲｏ ｃｋ ｅｔ＿ ｐｏｗｅ ｒｕｐ１ ｃｏ ｎ ｓｉｓｔｅ ｎｔ１  Ｖａ ｌｉｄＲｏ ｃ ｋｅｔ＿ｐｏｗ ｅ ｒｕ ｐ２ ｃｏ ｎ ｓ ｉｓ ｔ ｅ ｎ ｔ １  Ｖａ ｌ ｉｄ－  Ｒｏｃ ｋ ｅｔ＿ ｐｏｗ ｅｒｕｐ３  ｃｏ ｎ ｓｉｓ ｔ ｅｎ ｔ１ Ｖａ ｌ ｉｄＣｏ ｍｐｏｎ ｅｎｔ ｃ ｏｍｐｏ ｓ ｉ ｔ ｉ ｏｎ ｃ ｏｎ ｓ ｉ ｓｔｅｎｔ１  Ｖａｌ ｉｄ▽ Ｖｅｒｉ ｆｉｃａｔ ｉｏｎｆ ｏ ｒ Ｒ ｏｃ ｋｅｔ＿ ｐｏｗｅｒ ｕｐ１ １ ９Ｖａｌ ｉｄｖｖ Ｃ ｏｎ ｔｒａ ｃ ｔ Ｇ ｕａ ｒａ ｎｔｅ ｅｓ ５ Ｖａ ｌ ｉｄＳ ｕ ｂｃ ｏ ｍｐｏｎ ｅ ｎ ｔ Ａｓｓ ｕｍｐｔ ｉｏ ｎｓ Ｖ ａ ｌ ｉｄ（Ｏｓ）＿入火窮加电１ 令或者火箭准备令． 返回加电１ 指令执行＾果 Ｖ ａ ｌ ｉｄ（Ｏｓ）抗行完成后反懐加电１ 已加电 Ｖａｌ ｉｄ（Ｏｓ）ｖ 抗行宙误断电令发出 Ｖ ａｌ ｉｄ（Ｏｓ）新电令发出则为断电１ 否则为断电令为ｎｕ ｌ ｌ Ｖ ａ ｌ ｉ ｄ（Ｏｓ）ｖ Ｔｈ ｉ ｓ ｃ ｏｍｐｏ ｎ ｅｎ ｔｃ ｏｎ ｓ ｉｓ ｔ ｅ ｎ ｔ １  Ｖａ ｌ ｉｄ．  Ｒｏｄｃ ｅ ｔ＿ ｐｏｗｅ ｒｕｐ １＿ｉ ｎｐｕ ｔ  ｃｏ ｎ ｓ ｉ ｓ ｔｅｎ ｔ １  Ｖａ ｌｉｄｖＳ ｅ ｌＣｅ ｎｔｅ ｒ ｃ ｏｎ ｓｉｓｔｅ ｎｔ１  Ｖａ ｌ ｉｄｃ ｈ ｅｃ ｋ Ｒ ｏｃ ｋ ｅｔ ｃ ｏｎｓ ｉ ｓｔｅ ｎｔ１ Ｖａ ｌ ｉｄｖ Ｃ ｏ ｍｐｏ ｎ ｅ ｎ ｔｃｏ ｍｐｏｓｉ ｔｉｏｎ ｃ ｏ ｎ ｓｉｓｔｅ ｎｔ１  Ｖａ ｌｉｄ？ｙ  Ｖ ｅｒｉｆ ｉｃ ａｔ ｉ ｏ ｎｆｏｒ Ｓ ｅｌ ｆＣｅ ｎｔｅｒ ９ Ｖａｌｉ ｄ▽Ｖｅ ｒｉ ｆｉｃａ ｔｉｏｎ ｆｏ ｒ  Ｒｏｃ ｋｅ ｔ＿ ｐｏｗｅ ｒｕｐ２ １ ９Ｖａ ｌ ｉｄｖｖ Ｃ ｏｎ ｔｒ ａｃ ｔ Ｇ ｕａ ｒａ ｎｔ ｅｅ ｓ ５ Ｖａ ｌｉｄｖ  Ｓ ｕ ｂｃ ｏ ｍｐｏ ｎｅｎ ｔ Ａｓｓ ｕｍｐｔ ｉｏ ｎ ｓ Ｖ ａ ｌ ｉｄ（Ｏｓ）？翻较令或哲火雜龄， 返回Ｓ昵２ 指括果 Ｖａ ｌｉｄ（Ｏｓ）抗行反勵啦ＢＯＴ电 Ｖ ａ ｌ ｉｄ （Ｏｓ）Ｖ 拱行衝＾ 电令发出 Ｖ ａ ｌｉｄ（Ｏｓ）￣断电今发出则为断电１ 否则为断电令为ｎ ｕ ｌ ｌ Ｖ ａ ｌ ｉｄ（Ｏｓ）Ｔ ｈ ｉ ｓ ｃｏ ｍｐｏ ｎ ｅ ｎ ｔｃ ｏｎ ｓ ｉｓ ｔ ｅｎ ｔ１  Ｖａ ｌｉｄ－■ Ｒ ｏｃ ｋ ｅ ｔ ｐｏ ｗｅ ｒｕｐ ｌ Ｊ ｎ ｐｕ ｔ  ｃｏ ｎ ｓｉｓ ｔｅｎｔ１  Ｖａ ｌ ｉｄＳ ｅ ｌ ｆＣｅ ｎｔｅｒ ｃ ｏｎ ｓｉ ｓｔｅ ｎｔ１ Ｖａｌｉ ｄｃ ｈｅｃ ｋ＿Ｒ ｏｃ ｋ ｅ ｔ ｃ ｏｎ ｓｉｓｔｅ ｎｔ １  Ｖａ ｌ ｉ ｄ■ Ｃ ｏｍｐｏ ｎ ｅ ｎ ｔｃ ｏｍｐｏｓ ｉ ｔｉ ｏｎｃ ｏ ｎ ｓ ｉ ｓ ｔｅ ｎｔ１  Ｖａ ｌ ｉ ｄＶ ｅ ｒｉｆｉｃ ａ ｔｉｏ ｎｆｏｒ ＳｅｌｆＣｅｎｔ ｅｒ ９ Ｖａ ｌ ｉ ｄ图１ １ 火箭加电控制子系统体系结构模型组合验证结果类似的排气盖控制子系统的系统级需求为ＳＲ １ ， 可以分解为排气盖开关盖处理ＳＲ １ Ｈ １ 和排气盖开关盖控制ＳＲ １ Ｈ ２ ， 其中Ｓ Ｒ １ Ｈ １ 为： 判断是否是训练态， 如果为训练态则模拟回告排气盖控制系统排气盖控制结果； 如果为正常态， 则判断是否满足发射控制表， 满足则提取控制命令、火箭码然后执行排气盖控制命令， 回告火箭控制系统排气盖控制命令已执行． ＳＲ １ Ｈ ２ 为： 判断排气盖控制命令是否已执脊果执阁１ ２ 排气盖控制子系统的体系结构图证明其正确性． 由此可知排气盖控制子系统在该体系结构模咽下的系统级需求及其子需求都得到了满足． 通过这种方式可以完成对整个系统的体系结构模型的验证分析？ 确保体系结构模型的正确性．行， 已执行则在ｌ 〇ｓ 内每隔１ ０ ０ ｍｓ 进行自检， 判断自检结果， 如果ｌ 〇ｓ 内自检回告正常， 则回告排气盖控制系统排气盖控制命令执行成功， 否则回告自检故障， 排气盖控制命令执行失败． 排气盖开关盖控制ＳＲ １ Ｈ ２ 可以划分为子组件排气盖自检看门狗和排气盖自检函数． 这里就不再赘述． 如图〗２ 所示构造排气盖控制子系统的体系结构模型， 同时形式化其需求为契约．对其进行组合推理， 其组合推理结果如图１ ３ 所示． 根据其组合验证结果， 可以得知． 排气盖控制子系统的组合验证共涉及１ ３ 个组合推理， 其中系统级契约ＳＲ １ Ｇ 得到满足， 其子组件契约ＳＲ １ Ｈ １ Ｇ 、Ｓ Ｒ４ Ｈ ２ Ｇ 以及其子组件契约等经过组合推理之后〇 Ｐｒ ｏｂ ｌｅｍｓ； Ｐ ｒ ｏｐｅ ｒｔ ｉ ｅ ｓＡ Ａ ＤＬ Ｐｒｏ ｐ ｅ ｒｔｙ Ｖａ ｌｕ ｅ ｓ． Ｐ ｒｏ ｇｒ ｅ ｓｓ ＾Ａ Ｇ ＲＥ Ｅ Ｒｅ ｓｕ ｌ ｔｓ ＇Ｑ Ｄ Ｃ ｏｎｓｏ ｌ ｅＰ ｒ ｏｐｅｒ ｔ ｙｖＶｅｒｉ ｆｉｃａ ｔ ｉ ｏｎ ｆ ｏｒ  Ｒｏｃ ｋ ｅ ｔ Ｅｘｈ ａ ｕ ｓ ｔ Ｃ ｏｖ ｅｒ Ｔ ｏｐ Ｌｅ ｖ ｅ ｌＳ ｙｓｖ？Ｃ ｏｎ ｔ ｒ ａ ｃ ｔ Ｇ ｕ ａｒ ａ ｎ ｔｅｅ ｓ？ｖ  Ｓ ｕ ｂｃ ｏｍ ｐｏ ｎｅ ｎ ｔ Ａｓｓ ｕ ｍｐ ｔｉ ｏｎ ｓ， 输入火窮播气盖开关盖令， 返回排气盖幵关盖指令执行结果执行反離雜已开／缝＾Ｔｈ ｉ ｓｃ ｏ ｍｐｏｎ ｅ ｎｔ ｃ ｏｎｓ ｉ ｓｔｅ ｎｔＲ ｏｃ ｋ ｅｔ＿Ｅｘｈ ａ ｕ ｓｔＣｏ ｖ ｅｒ＿ｉ ｎｐｕｔ ｃ ｏｎ ｓ ｉ ｓｔｅ ｎｔ－ Ｓ ｅ ｌｆＣ ｅ ｎ ｔ ｅ ｒ ｃ ｏｎ ｓｉ ｓ ｔ ｅ ｎｔＣｏ ｍ ｐｏ ｎｅ ｎｔ ｃｏ ｍ ｐｏｓ ｉ ｔ ｉｏ ｎ ｃ ｏｎｓｉ ｓｔ ｅ ｎｔｖ， Ｖｅ ｒｉｆｉｃａ ｔｉ ｏｎ ｆｏ ｒ Ｓ ｅ ｌ ｆ Ｃｅｎ ｔｅ ｒｖ 、Ｃｏｎ ｔ ｒａ ｃ ｔＧ ｕａｒａ ｎ ｔ ｅｅｓＳ ｕ ｂｃ ｏ ｍｐｏ ｎ ｅ ｎｔ Ａｓｓ ｕ ｍｐ ｔｉｏｎ ｓ自錄正常， 正常则回告自碰雜織行５ｇｌ力，？ 否则酷播脱行姚Ｔ ｈｉ ｓ ｃｏ ｍ ｐｏｎ ｅｎ ｔ ｃ ｏ ｎ ｓ ｉ ｓ ｔｅｎ ｔｗａｔ ｃ ｈ ｄｏｇｓ ｅｑｕ ｅ ｎｃ ｅ ｃ ｏｎ ｓｉｓ ｔｅ ｎｔＳ ｅｌｆ Ｃｅｎｔｅｒ ｌ ｓ ｅ ｑｕｅ ｎ ｃ ｅ ｃ ｏｎ ｓｉｓｔｅ ｎｔ？ Ｃ ｏｍ ｐｏ ｎ ｅ ｎ ｔ ｃ ｏｍ ｐｏ ｓｉ ｔｉｏｎ ｃ ｏｎ ｓ ｉ ｓｔ ｅ ｎｔＲｅ ｓ ｕｌ ｔ１ ３ Ｖａ ｌ ｉ ｄ３ Ｖａ ｌ ｉ ｄＶ ａ ｌ ｉｄ（Ｏ ｓ）Ｖ ａｌ ｉｄ（Ｏ ｓ）Ｖ ａ ｌ ｉｄ （Ｏ ｓ）１  Ｖａ ｌ ｉ ｄ１  Ｖａ ｌｉ ｄ１  Ｖａｌｉ ｄ１  Ｖａ ｌ ｉ ｄ６  Ｖａｌ ｉｄ２  Ｖａ ｌ ｉｄＶ ａｌｉｄ（Ｏ ｓ）Ｖ ａｌ ｉｄ（Ｏｓ）１  Ｖａ ｌ ｉｄ１  Ｖａｌ ｉｄ１ Ｖａｌ ｉｄ１  Ｖａ ｌ ｉｄ图１ ３ 排气盖控制子系统体系结构模型组合验证结果４基于Ｕ Ｐ ＰＡ Ａ Ｌ 的单组件验证底层叶子组件被Ａ Ｇ ＲＥ Ｅ 内部抽象其组件功能行为并默认如果其保证成立． 则其功能就是正确的， 所以这些组件的功能行为需要在Ａ Ｇ Ｒ ＥＥ 验证环境外进行验证． 叶子组件的功能和行为由ＡＡ Ｄ Ｌ 模型中子程序及行为附件表达． 本节提出了Ａ Ａ Ｄ Ｌ２ Ｕ Ｐ ＰＡ Ａ Ｌ 的模型转换的方法， 将叶子组件的模型转换到ＵＰ ＰＡ Ａ Ｌ 模型， 然后使用叶子组件的需求构造其性质逻辑公式Ｔ Ｃ Ｔ Ｌ ． 最后使用ＵＰ Ｐ Ａ Ａ Ｌ 进行验证分析， 证明叶子组件的功能行为的正确性．４． １ 形式化定义火箭发射控制子系统中大量使用子程序调用，因此， 这里给出行为附件和子程序形式化定义．定义１ ． 行为附件ＢＡ ＝ 〈Ｓ ， Ｓ〇， Ｖ ， Ｇ ， Ａ ， Ｔ ＞，其中：（ １ ） Ｓ 为状态集合， 状态主要有ｉ ｎｉ ｔ ｉ ａＫ ｃｏｍｐ ｌ ｅ ｔ ｅ 、ｃｏ ｍｐｏ ｓ ｉ ｔ ｅ 等类型， 其中． ｉｎｉ ｔｉ ａｌ 表示行为附件的初始状态； ｃｏｍｐｌ ｅ ｔ ｅ 为行为附件的完成状态； ｃｏ ｍｐｏ ｓ ｉ ｔ ｅ表示该状态可以是一个组合状态．（ ２ ） Ｓ０ Ｇ Ｓ ， 为初始状态．（ ３ ） Ｖ 为局部变量，一般为行为附件使用的辅助变量．（ ４ ） Ｇ （ Ｇ ｕ ａｒ ｄ ｓ ） 为状态转换条件， 针对状态变量的逻辑判断， 是否进行状态变迁．（ ５ ） Ａ （ Ａ ｃ ｔ ｉ ｏ ｎｓ ） 为状态转换需要执行的动作，包括子程序调用（ Ｓ ｕ ｂ Ｃ ａ ｌ ｌ ） 赋值、发送数据、计算、等待等．（ ６ ） ７＇＝ Ｓ Ｘ｛ Ｇ ， Ａ｝Ｘ Ｓ ， 为状态变迁．定义２ ．子程序组件Ｓ Ｕ ＝〈Ｐａ ｒｍ ， Ｓ ＯＰｒＤ ａ ｔａＡ ｃ ｃｅｗ ， ＳＭ ６／＞ ｒｏ ｇ＇ｒａｍ Ａｃ ｃｅｓ ｓ ， ＜ＢＡ＞ ， 其中：（ １ ）Ｐａ ｒ ｖｗ＝ Ｕ ＰＡ ｉ？Ｍ ， Ｏ ＰＡ ＲＭ｝， Ｊ ＰＡｉ ？Ｍ为输人参数， 为输出参数， 参数只能够通过子程序调用进行输人， 并由子程序调用输出．（ ２ ）Ｓ ＯＰ ｒ＝｛ ＯＥ Ｄ Ｐ ， 〇￡Ｐ｝ ， 子程序特征用参数来进行数据传递． 输出端口只包括输出事件端口和输出事件数据端口．（ ３ ）Ａ ｃ ｔ■如指定了子程序可以访问的数据２ １ ４ ２ 计算 机 学报 ２ ０ ２ ０ 年式态制令码模状控命箭盖火排张博林等：一种面向安全关键软件的１ １ 期 ＡＡＤＬ 模型组合验证方法 ２ １ ４ ３组件集合． 子程序的特征中用ｒ ｅ ｑｕｉ ｒ ｅ ｓ 声明子程序能够访问的数据组件． 子程序的行为附件中可以描述何时对数据组件进行访问．（ ４ ） ＳＭ６ｐ ｒｏ ｇ ｒａ ｗＡ ｃｃ ｅｓ ｓ 指定了当前子程序能够访问的子程序组件的集合． 子程序在特征中用ｒ ｅｑｕ ｉ ｒ ｅｓ 声明子程序能够访问的子程序组件． 子程序的行为附件中可以描述何时对子程序组件进行访问．（ ５ ）是具体的子程序功能行为描述．ＵＰ ＰＡＡＬ 是基于时间自动机网络的模型检查环境， 下面给出时间自动机与时间自动机网络的形式化定义．定义３． 时间自动机．一个时间自动机ＴＡ 由可以定义为一个六元组ＴＡ＝〈Ｌ ， ｋ ， ２ ， Ｘ ， ｆ：， Ｊ ＞ ，其中：（ １ ） Ｌ 是时间自动机ＴＡ 中所有状态（ 节点） 的非空集合．（ ２ ） １＾ ６ １ ， 是ＴＡ 中初始状态（ 节点） 的集合．（ ３ ） ２ 是变量集合．（ ４ ） Ｘ 是一个有穷的时钟集合， 而且默认从０开始， 每次自增１ ，且可以被置〇．（ ５ ） １ 是一个状态集合Ｌ 到时钟集合的映射（ 触发条件） ， 记作少（ Ｘ ） 表示Ｌ 中的每个状态Ｓ 都有一个属于步（ Ｘ ） 的时钟约束．（ ６ ） Ｅ ＧＬ Ｘ Ｇ Ｘ Ａ ｃ？ Ｘ ［／ Ｘ Ｌ 是自动机中所有状态变迁（ 有向边） 的集合． Ｇ 表示一个约束条件（ ｇｕａ ｒｄ ） 的集合可以为空， 只有满足了约束条件才会发生状态变迁分别表示输入（ 记为？ ）和输出（记为！ ） 的同步信号， 构成了状态变迁的条件．１／ 是对时钟变量或者整型变量的更新（ ｕｐ ｄａ ｔ ｅ ）操作， 在状态变迁进行的同时进行的赋值操作．定义４ ． 时间自动机网络定义为一个四元组Ｎ ＴＡ＝〈７Ｔ ＸＹ ， Ｖａｒ （ ；， Ｃｃ ， Ｃ／ ｉ ＞ ， 其中：（ １ ） ＴＷ＝〈ＴＡ。， ７７＾ ，…， ＴＡ？ ＞ 是一组相互平行并且相互关联的时间自动机．（ ２ ） Ｖａｒ ｃ 是全局（ 共享） 变量的集合．（ ３ ） Ｃｃ是全局时钟的集合．（ ４） ＣＡ 是同步信道的集合．４． ２ＡＡ ＤＬ２ ＵＰ ＰＡＡＬ 模型转换规则整个转换包括子程序、行为附件、数据类型四个方面． 针对子程序及行为附件定义转换规则ｎ （ Ａ ）＝＜ＴＴＳｙ ， ￡＞ｅｄ ＞ ， 其中表示对应Ａ ＡＤＬ 模型中子程序的转换后在时间自动机网络中时间自动机集合， Ｄｅｄ 表示声明的全局变量．（ １ ） 子程序组件到时间自动机的映射ｒ ．ｓ ［； （ ｓ ｍ６，． ）＝〈（ ７７１．吃） ， Ｄ ｅｃ Ｚ ＞ ， ０ ＜ ／ ＜ ｜Ｓ ｔ／｜， 子程序组件单独映射到一个时间自动机， 该时间自动机主要表示的是子程序的执行状态变换． 通过转换规则ｒｓ［； ： Ｓ Ｕ —〈 ７ＶＵ ， ＞ 将子程序映射为时间自动机． ｒ ｓｕ ） 的转换对应的是Ｓ Ｕ— （ Ｐａｒｍ ， ＳＯＰｔ ， Ｄａ ｔａＡ ｃｃ ｅ ｓｓ ， Ｓｕｂｐ ｒｏｇｒ ａｍＡｃｃ ｅｓｓ ，ＢＡ ）＾（ ＜Ｌ ， Ｌ〇ｒ Ｓ ， Ｘ ， Ｅ ， Ｉ＞ ， Ｄｅｃ ｌ ＞ ．以下对转换到ＴＡ 集合和对应的转换规则做具体的说明．Ｌ＝｛，ｔｔ ｒａ ｉ ｆ ｉ ｎｇ＂， ａ ｃ ｉ ｉ ｖａ ｔｉ ｏ ” ｝ ， 子程序在ＡＡ Ｄ Ｌ 模型中的执行语义是可以顺序执行的可调度单元， 所以其基本状态为等待（ ｗａ ｉ ｔ ｉ ｎｇ ） 状态， 如果子程序被调用，之后会进入激活状态（ ａ ｃｔ ｉ ｖａｔ ｉ ｏｎ ） ， 执行完成后则会进人初始状态（ ｐｉ ｖｏ ｔ ） ．初始状态为子程序初始化尚未调用的状态．２ ＝ ｛ ■ ＳＭＡ Ｓ ｆａ ｈ ａｃ ｆ ｉ ｔｉａ ｆ ｅ ｝ ， 用于记录子程序执行状态的监控变量和是否被激活的监控变量．用于记录子程序的执行时间．Ｅ ＝ ｛ ｐｉ ｖｏ ｔ＾－ ｗａ ｉ ｔ ｉｎｇ ，ｗａ ｉ ｔ ｉｎ ｇ－＾－ ｐ ｉ ｖｏ ｔ ， ｐ ｉｖ ｏｔ＾－ａ ｃ ｆ ｉ ｖ ａｔ ｉ ｏ ｎ ， ａｃ ｆ ｉ ｕａ ｆ ， Ｇ ， Ａ ， Ｌ〇， 表７Ｋ 不同状态之间的变迁， 其中， Ｇ 表示状态变迁的守卫条件的集合， Ａ 表示状态变迁同步通道的集合， １７ 表示状态变迁更新操作的集合．｝ ， 这里给出的不变量为调用该子程序的最大执行时间．Ｄ ｅｃ／ ＝｛ ｆａ ｒｍ ， ， ｄａｆ ａ ， Ｖａｒ ， ？ ｝ ， 将子程序在运行过程中使用的端口或数据声明为全局变量．子程序存在■Ｓｔ ＾ｐｒ ｏｇ ｒａ ｍＡ ｃ ｃｅ ｓ ｓ 表疋子程序在执行过程中会调用另一个子程序， 所以需要初始化调用的子程序， 则有：Ｓ ｕｂｐ ｒｏｇｒ ａｍ Ａｃｃｅｓ ｓ （ ｖＳ ｕ ｈ： Ｓ ｕｂＡ－？ ＊＜ ＴＡ Ｓ？ Ｍ ， Ｄｅｃｌ ） ） ，子程序的行为附件会调用ＢＡ 的转换规则映射到时间自动机中．（ ２ ） 行为附件到时间自动机的映射行为附件的整体结构是一个非确定的层次状态机． 子程序在执行时， 会从输入端口读人数据或事件， 该子程序的行为附件在运行的过程中可以使用这些数据或事件执行计算或逻辑判断， 然后将执行结果返回给子程序的输出数据或事件端口．一个行为附件是对子程序的细化， 因此， 行为附件的转换是对子程序时间自动机的扩展． 通过转换规则： ｒ Ｂ Ａ： ＢＡ—〈ＴＡ ＿？ ｄ， Ｄｅｄ ＞ 将行为附件映射到２ １ ４ ４ 计算机学报 ２ ０ ２ ０年时间自动机． ：Ｔ？ Ａ 的转换对应的是〈Ｓ ， ＳＯ ， Ｖ ， Ｇ ， Ａ ， Ｔ 〉—〈ＴＡ ，ｘ ，ｅ ？ ｄ ，＞，其中， 由于行为组件的状态中的一个状态可以变迁到多个状态＆ｅＳ ， 所以在状态转换的时候并不能直接映射到时间自动机中， 但是Ｔ ＝ Ｓ Ｘ ｛Ｇ ， Ａ｝ Ｘ Ｓ中包含的是一个完整的状态变迁， 所以可以不直接使用Ｓ 完成行为附件的状态变迁到时间自动机中的状态变迁的转换． 下面对具体的转换过程做说明：Ｌ＿ｄ＝｛Ｈ＾ Ｕ Ｌ ， 将每一个状态变迁＾： 映射成自动机变换的中间状态．附加后的自动机的初始状态不发生变换， 依旧为／＾ｏ ｒ２？ ，ｅ ｎｄ ＝ ｛ ＢＡ伽化｝Ｕ２ ， 增加了用于记录行为状态变换的监控变量．用于记录子程序的执行时间， 不发生变换．＾ｅ ｘ ｔ ｅ ｎ ｄ｛ ｐ ｌ Ｘ ＪＯ ｔ￣Ｔｊ ＊ Ｔ．￣ｐ ｉＤＯ ｔ ｉ Ｇｅ ｘ ｌｅ ｍＪ  ？ ＾ｅ ｘ ｔ ｅｎ ｄ ＞ ＾ｅ ｘ ｔ ｅｎ ｄ  ｝（ ０ ＜〇＿＜｜Ｔ｜） ， 首先对状态变迁进行扩展， ＢＡ 中每一个状态变迁Ｔ 都会转换为状态变迁ｒ，— 同时将ＢＡ 的了中的Ｇ 和Ａ 映射到〇？ ，＾ 和． 如果Ａ 中含有子程序调用则将调用子程序状态机改为激活状态．） ＝｛ ｃ Ｚ ＜ ｃｏ？ｊ ／） ＭＺ ｅ＿ ｃ？ ａｚ ＜＾ｉ ”ｅ ｝ ， 这里给出的不变量为子程序最大执行时间．｛ Ｖ ｝ ， 将行为附件的变量映射为全局变量．上述映射规则通过图１ ４ 进行说明， 子程序的起始状态为状态， 根据状态监控变量进行状态变迁， 其中激活状态的下？ ？ 个状态应为行为附件的初始状态， 之后每一个行为附件的状态变迁ＴＭ？ ？． 都会生成一个新的自动机中间状态节点， 行为附件的最终状态回到子程序自动机的激活状态， 完成整个子程序状态机的状态变迁．ｕ ｓ Ｏｒ ｄｅ ｒｌ：？ ｒ Ｂａ ｓ ｅ＿Ｔｙ ｐｅ３ ： ：！．＂ｎｓ ｉ ｇａｅ ａ＿ｓｐｅｃｉ ｆｉ ｃａｔ ｉｏ ｎ ；： Ｈ ａ ｓ ？ Ｔｙ ｐｅ ｓ ： ：Ｂａ ｓ ｅ Ｔ ｙｐ ｅ ｓ ： ： ：图１ ４ 子程序模型转换（ ３ ） 基本数据类型的映射Ａ Ａ Ｄ Ｌ 定义了三种基本数据类型： 整型、布尔类型、用户自定义数据类型． Ｕ Ｐ ＰＡ Ａ Ｌ 中定义了基本数据类型整型、布尔型、数组类型、结构休数据类型等， 因此建立映射规则时对于整型和布尔型可以做直接映射， 对于用户自定义数据类型则分别映射为数组类型和结构体数据类型， 对应的映射关系如表４ 所不．表４ 数据类型映射关系ＡＡＤ Ｌ 数据类型 ＵＰＰ ＡＡＬ 数据类型 描述Ｉ ｎｔ ｅ ｇ ｅｒ Ｉｎ ｔ 将ｉ ｎ ｔ ｅ ｇ ｅ ｒ 映射为ｉｎ ｔｂ ｏ ｏ ｌ ｅａ ｎ ｂ ｏ ｏ ｌ 将ｂ ｏｏ ｌ ｅａ ｎ 映射为ｂ ｏｏ ｌ自定义数组 数组类型ａ ｒ ｒａ ｙ将自定义数组映射为数组类型ａ ｒ ｒ ａ ｙ自定义结构体 结构体数据ｓ ｔ ｒ ｕ ｃ ｔ将自定义结构体映射为结构体类型ｓ ｔｒ ｕ ｃ ｔ使用上述的模型转换方法， 可以将Ａ Ａ Ｄ Ｌ 子程序以及行为附件转换为Ｕ Ｐ ＰＡ Ａ Ｌ 模型， 对组件的功能行为进行验证分析． 下面使用火箭加电１ 函数组件为例说明Ｕ Ｐ ＰＡ Ａ Ｌ 模型验证．４ ． ３ 基于ＵＰＰＡＡＬ 的ＡＡＤＭ莫型组件功能行为验证根据３．２ 节中火箭加电１ 函数的需求Ｓ Ｒ４ Ｃ１ Ｈ １ ，其功能行为由子程序、子程序调用以及行为附件具体实现． 构造其功能行为模型如图１ ５ 所示． 其中， ｓ。为初始状态， 状态变迁力主要是判断其是否是加电１ 命令或火箭准备令． 之后会调用获取发控参数表子程序， 如果不满足发控表进行状态变迁如果满足发控表则进行状态变迁， 在状态＆ 下判断是正常态还是训练态， 如果是正常态则是进行状态变迁ｓ２ ＿ ＆ ＿１ ， 执行加电１ 控制子程序， 执行提取控制命令和火箭码子程序， 并回告发射控制系统张博林等：一种面向安全关键软件的１ １ 期 ＡＡＤＬ 模型组合验证方法 ２ １ ４５加电１ 控制已执行； 如果为训练态， 则执行状态变迁ｓ２ ＿ ＆ ＿２ ， 但是变迁后调用训练态子程序， 模拟返回加电１ 控制结果．ｉ ｎ ｐ ａｒ ａｍｅｔ ｅｒｉ ｎ ｐａ ｒａｍ ｅｔｅｒｉｎ  ｐａ ｒａｍｅｔｅｒｉ ｎｐ ａｒ ａ ｍｅｔｅｒ ｉｎｉ ｔ ｉａｌｒｅｑｕ ｉｒｅ ｓｄ ａｔ ａ ａｃ ｃｅｓｓｒｅｑ ｕ ｉ ｒｅｓ ｄ ａｔ ａ ａｃｃｅｓ ｓ 匸Ｓｌ －Ｓ２５〇＿ＳｌｓｙｖｌｌＳ＼—Ｓ３＾ｆ ｉ ｎ ａｌｙ ｏ ｕｔｐ ａｒ ａｍｅｔ ｅｒ ｐｏ ｒ ｔｔｆｏｕ ｔ ｐａ ｒａ ｍｅｔｅｒｐ ｏｒ ｔｙｏｕ ｔ ｐａ ｒａ ｍｅｔ ｅｒｐ ｏｒ ｔ￥ ｒｅｑ ｕ ｉｒｅｓ ｓｕ ｂ ｐ ｒｏ ｇｒ ａｍ ａｃｃｅｓ ｓ） ｒ ｅｑ ｕｉ ｒｅｓ ｓｕ ｂｐ ｒ ｏｇｒａ ｍ ａｃ ｃｅｓｓ） ｒ ｅｑ ｕｉ ｒｅｓ ｓ ｕ ｂｐｒ ｏｇ ｒ ａｍ ａｃ ｃｅｓｓ析组件的功能行为．例如验证性质：（ １ ） 无死锁性：Ａ ［ ］  ［ｄ ｅａｄ ｌ ｏｃ ｋ ．（ ２ ） 可达性：Ｅ Ｏ （． ＢＡ Ｓ ｔａ ｔｅ＿Ｒ ｏ ｃ ｋ ｅ ｔ＿Ｐｏｗｅ ｒＯｎ ｌ＿ｉｎ ｉｔ＝＝ ３ ） ．（ ３ ） 功能正确性：Ｅ （ ＞ ｛ ＢＡ Ｓｔａ ｔ ｅ＿Ｒ ｏｃ ｋ ｅｔ＿Ｐｏ ｖｕｅｒ Ｏｎ ＼＿ｉ ｎ ｉ ｔ＝＝ ２ ｉｍ ｐｌ ｙＢ Ａ Ｓｔａ ｔ ｅ＿Ｒｏ ｃｋ ｅｔ＿Ｐｏ ｖｕ ｅｒＯ ｎ ＼＿ ｉ ｎ ｉｔ— ＝ ３ ） ａ ｎｄ图１ ５ 火箭加电１ 函数的功能行为模型示例 （ ａｃ ｔ ｉ ｖｅ＿Ｔ ｉ ｃｋＧｅ ｔ＿ｉ ｎ ｉ ｔ—＝１ ） ．通过４ ． ２ 节的转换规则， 将其ＡＡＤＬ 模型转换为ＵＰＰＡＡ Ｌ 模型如图１ ６ 所示． 转换得到的ＵＰＰＡ ＡＬ模型包含了火箭加电１ 函数自动机、获取发控表子程序自动机、匹配发控表子程序自动机、加电１ 控制子程序自动机、提取信息子程序、信息回告子程序自动机等自动机构成的时间自动机网． 根据其行为附件以及子程序调用的组成的时间自动机网络， 可以对自动机的状态、自动机的行为以及变量进行验证， 从而分（ ４ ） 安全性：Ａ ｛＾＼（ ＢＡ Ｓｔａ ｔｅ＿Ｒ ｏ ｃｋ ｅ ｔ＿ Ｐｏ ｗｅ ｒＯｎ ｌ＿ｉ ｎ ｉ ｔ＝＝ ２ ｉｍ ｐｌ ｙＢＡＳｔ ａｔ ｅ＿Ｒ ｏ ｃｋ ｅｔ ＿Ｐ ｏｖｕｅｒＯｎ ＼＿ｍ ｉ ｔ！ ＝ ３ ） ｏｒ（， ａ ｃｔ ｉｖｅ＿ Ｔｉ ｃｋ Ｇｅｔ＿ｉ ｎｉ ｔ ＼ ＝１ ）．使用ＴＣＴ Ｌ 公式表达性质， 然后通过ＵＰＰ ＡＡＬ模型检测工具验证模型是否满足性质， 可以验证火箭发射控制子系统底层叶子组件的功能行为正确性， 系统其余的叶子组件的验证这里就不再赘述．－ 公， 丨Ｈｍｓ ｆｌ ＣＴ＊Ｓ ＥＬＳＥＲＤ ＬＥ Ｒｏｃｋ ｅｔＰｏ？ｅ ｒＯ ｎｌ＿ ｉｎｉ ｔ ＿ｍａ ｃｈｉ ｎｅ ｗａ ｉ ｔ ｉｎ ｇ？ Ｓ Ｆ ＲＡ ？Ｅ＿ＰＣ＿Ｉｉ ｓ Ｒ£ ａ ｄｉ－ｌ＿ｉ ｎ ｉ ｔｅ ａ ｃ ｈ ｉ ｎｇ？Ｓ ＥＬ Ｓ ＨＲＤ ＬＥ＿ＦＲＡ ＭＥ＿Ｐ Ｃ＿Ｈｉ ｓＲｅａｄ＞－ｌ＿ ｉ ｎｉ ｔ＿？ ａｃｈｉ ｎ ｅ＿Ｔａ ｉ ｔ ｉ ｎｇ？ Ｓ  ＬＧＪ ＿ＴＯ＿Ｐｌ ａｉＩｎ ｆ ｏ ｉ ｎ ｉｔ ？ ａ ｃｈｉ ｎ ｅ－ ａ ＥＬ ＳＥＲＯ ＬＥ＿ＬＣＵ＿ＴＤ＿Ｐｌ ａ ｔＩｎｆｏ＿ｉｎｉ ｔ．ｉ Ｓ？ ｄＳｔａｒ ｔ ＿ｉ ｎｉ ｔ＿？ａｃｌ＊ ＾  ＥＬ ＳＥＲＯＬＥ＿？ｄＳ ｔ ａｒ ｔ．－一．－— ｃｈｉ ｎ ｅ ＾ｊｔ ａ ｉｔｉ ｎｇ？ Ｓ  ＬＣＯ＿ＴＤ＿Ｐ〇Ｔｅ ｒＯ ｎｌＣ ｈｋ＿ｉ ｎ ｉ ｔ＿？ ａ ｃｈ ｉｎｅ＋ Ｓ ＥＬ Ｓ ＥＲＯＬＥ＿Ｌ ＣＤ＿ＴＤ＿Ｐｏ ？ｅｒＯ ｎｌ Ｃ ｈｋ＿ ｉ ｎｉｔ＿ｉ ａｃｈｉ ｎ ｅ＿＊ａ ｉ ｔ ｉ ｎｇ士？￥ Ｔ ｉ ｃ ｋＧｓ ｔ＿ｉ ｎ ｉ ｔ＿？ａ ｃ ｈｉ ｎｅ？ ＾ ＥＬＳ ＥＲＵＬ Ｅ＿Ｔｉｃｋ Ｇｅ ｔ ＿ｉ ｎｉ ｔ ＿？ ａｃｈｉ ｎ ｅ＿Ｔ ａｉ ｔ ｉｎ？ｔ＾  Ｔｒ ｉ ｔ ｓ＿ ｉｎｉ ｔ＿＊ ａ ｃｈｉ ｎｅ＊ＳＬＣ０＿２８ ９ＡＣｈ ｅｃｋ Ｓ ｕ？＿ｉ ｎ ｉ ｔ ＿ ？ ？ｉ ＾ ＥＬ ＳＥＲＵＬ ￡＿ＬＣｌｆ＿ ２８ ９ＡＣｈｅ ｃｋ Ｓｕｉ ＿ ｉ ｎ ｉ ｔ＿ ？ ＊ ｃ ｈ ｉ ｎｅ ＿Ｔａ ｉ ｔ ｉ ｎｇ？ Ｓ  ｌ ｏｇ Ｈｓ ｇ＿ｓｒ ａｐｐ ？ｒ＿ｉ ｎｉ ｔ＿＊ ａ ｃｈ ｉｎｅｆＥＬ Ｓ ＥＲＵＬ Ｅ＿ ｌｏｇＫ ｓ ｇ＿Ｔｒ ａｐ ｐ？ ｒ＿ ｉ ｎｉ ｔ＿？ ａ ｃｈｉｎｅ＿ｖａｉ ｔ ｉ ｎｇ＊ ＾ Ｆ ＲＡ ＭＥ＿Ｐ Ｃ＿ｌ ｌｉ ｓ Ｃ ？ｐＣ ｈｋ ｉ ｎ ｉ ｔ ａ ａ ｃｈｉ ｎｅｔ Ｓ Ｅ Ｌ ＳＥＲＵ ＬＥ＿ ＦＲＡ Ｋ Ｅ＿Ｐ Ｃ＿Ｍｉ ｓＣ＊ ｐＣ ｈｋ＿ ｉ ｎｉ ｔ ＿？ ａ ｃｈｉ ｎ？ ＿Ｔａ ｉ ｔ ｉ ｎ ｇ＊ Ｓ ｌ ｏ ｇ Ｍ ｓ ｇ＿ ｉｎｉ ｔ ＿ｓ ａｃｈ ｉ ｎ ？＊ Ｓ Ｅ Ｌ ＳＥ ＲＵ Ｌ Ｅ＿ｌ ｏｇ＞ ｓ ｇ＿ｉ ｎ ｉ ｔ＿？ ａ ｃｈ ｉ ｎｅ＿＊ａ ｉ ｔ ｉ ｎ ｇ＊ 供型芦明： ｈ ｍｅ＿ｔ： 名字： ｉ ｔ＿？ｃｈ ｉ ｎｅ  爱舒：－ｆ，＊ － Ｔ＾ｈ ｉ ｎ ， ＇ｔ： ０々，ＢＡＳｒａ ｉ ｅＲ ｏｃ Ｋ ｅ ！＿ Ｐｏ ｗｅ ｒｐｒｆｉ＿ｍ ：ｔ ＝  ＼ ／＿ ＿＿＿＾ Ｒ ｘ ｆｃ ｉ—ｏｅｒｓ ｕ ｔ３ ｓｔａｉ ｅ＿Ｒｏ ｃ ｔ？ｔ＿Ｐｏｗ ｅｒ 〇ｎ ＾＿ｉ ｎ ｉ ｔ ＝ａ ｉｓ．＾Ｋｔｊ ｅａ＾８ 〇ｆｉＫ ｅｉ ．Ｐ ｏｗｅｒ〇ｎｉ＿ｉ ｎ ｉ ｆ＾Ｐ ｏｓｓ ｅｒＯ ｎ－ｉ＿ＩＴ ！ ？ ．ｌ ＢＪ ＜ｕｍ ＝Ｒ 〇ｃＫｅ ｔ＿Ｆ －： ＇ ｖｅ ｆＯｎ？！＿Ｐｏ ｖ？ ｅｆ〇ｎ ＇＿ｉｎ ｒｔ＿？ ｊｔｅ？ ｌｕｍ ＝Ｒｏｃ Ｊ？ ｌ＿Ｐｏ ？ （ｅ ｆＯｏ ｌ ｊｎ ｉ ｎ图１ ６ 火箭加电１ 函数转换得到的Ｕ ＰＰＡ ＡＬ 模型５ 工具实现及案例分析５ ．  １ 工具实现Ｏ ＳＡ Ｔ Ｅ 是开源的面向安全关键软件的Ａ Ａ ＤＬ模型建模工具环境， 在Ａ Ａ ＤＬ 模型驱动开发中广泛应用． 本文所开发的Ａ Ａ Ｄ Ｌ模型验证原型工具是以插件的形式集成到Ｏ ＳＡ Ｔ Ｅ 开发环境中， 以支持基于Ａ Ｇ ＲＥ Ｅ 的体系结构模型组合验证和基于Ｕ Ｐ ＰＡ Ａ Ｌ 的Ａ ＡＤ Ｌ 模型组件功能行为验证， Ａ Ａ Ｄ Ｌ模型验证原型工具的整体框架图如图１ ７ 所示． 其中工具实现主要是Ｕ ＰＰ Ａ Ａ Ｌ 模型验证模块， Ａ Ｇ Ｒ ＥＥ验证模块主耍是提供一个构造契约的窗口界面， 然后重用Ａ Ｇ Ｒ ＥＥ 现有的能力， 以方便验证人员使用．２ １ ４ ６ 计算 机 学报基于ＵＰＰＡＡＬ 的功能行为验证模块图１ ７Ａ ＡＤ Ｌ 模型验证原型工具的整体框架图基于Ａ Ｇ ＲＥ Ｅ 的组合验证工具架构如图１ ８ 所示， 工具提供了需求描述功能， 在建模的同时书写表５ 主要功能及其代码行数ＡＡ Ｄ Ｌ 模型验证原型工具功能执行功能 代码行数（ 行）自动将选定的ＡＡＤ Ｌ 模型转换到ＵＰ Ｐ ＡＡ Ｌ 模型Ｊ ＡＶ Ａ ： ５ ３ ０ ０＋ＡＴ Ｌ ： ７ ８ ０ ０＋ＵＰ Ｐ Ａ ＡＬ 验证界面 Ｊ ＡＶＡ ：９ ０ ０＋Ａ ＡＤＬ２ ＵＰＰ ＡＡＬ自动转换修改Ｕ Ｐ ＰＡ ＡＬ 初始声明变量值 ＪＡ ＶＡ ： ６ ０ ０＋将界面中的验证性质导人到Ｕ ＰＰ Ａ ＡＬ 中验证并返回验证结果到界面中Ｊ Ａ ＶＡ ： ８ ０ ０＋Ａ Ｇ Ｒ ＥＥ 验证ＡＧ ＲＥ Ｅ 验证界面 Ｊ Ａ ＶＡ ： １ ０ ０ ０＋添加契约到Ａ ＡＤ Ｌ 模型中 Ｊ Ａ ＶＡ ： ３ ０ ０＋２ ０ ２ ０年上该系统或组件的需求描述， 然后在工具中根据需求构造组件契约并导人到Ａ Ａ ＤＬ 模型中， 之后使用Ａ Ｇ ＲＥ Ｅ 验证分析．基于ＵＰ ＰＡ Ａ Ｌ 的Ａ ＡＤ Ｌ 模型组件功能行为验证模块的功能为启动工具时通过右击需要转换的Ａ Ａ ＤＬ 文件， 之后Ａ Ｔ Ｌ 转换引擎读人一个标准的Ａ Ａ ＤＬ 模型的ＸＭ Ｌ 文件（ ． ａ ａ ｘ ｌ ２ 文件） ， 该Ａ Ａ ＤＬ模型必须符合Ａ Ａ Ｄ Ｌ 元模型， Ａ Ｔ Ｌ 转换引擎参照Ａ Ａ Ｄ Ｌ 元模型和Ｕ ＰＰＡ Ａ Ｌ 元模型， 根据编写的Ａ Ａ ＤＬ ２ Ｕ ＰＰ Ａ Ａ Ｌ 转换规则， 生成对应Ａ Ｔ Ｌ 格式的Ｕ Ｐ ＰＡ Ａ Ｌ 模型的Ｘ Ｍ Ｌ 文件， 由于ＡＴ Ｌ 引擎识别的ＸＭ Ｌ 文件格式与Ｕ Ｐ ＰＡ Ａ Ｌ 运行的Ｘ Ｍ Ｌ 文件格式存在一些兼容性问题， 所以还需要对生成的ＸＭＬ 文件进行简单的后处理， 生成标准的ＵＰＰＡ Ａ Ｌ模型文件， 然后打开验证窗口， 通过窗口输人验证使用的Ｔ Ｃ ＴＬ 公式可以跳过Ｕ Ｐ ＰＡＡ Ｌ 工具直接将验证结果反馈到当前界面中． 该模块的架构如图１ ９ 所示． Ａ Ａ ＤＬ 模型验证原型工具的主要功能及其代码行数如表５ 所示．图１ ９ 基于ＡＧＲＥ Ｅ 的体系结构模型组合验证模块架构图工具的主要特点是：（ １ ） 在建模方面， 开源建模环境Ｏ ＳＡ ＴＥ 建立在Ａ ＡＤ Ｌ ＡＴＬ ＪＡＶＡ； ＵＰＰＡＡＬｉＯＳＡＴＥ图１ ８ 基于Ｕ ＰＰ ＡＡ Ｌ 的Ａ Ａ ＤＬ 模型组件功能行为验证模块架构ＷＸＶＳＯ张博林等：一种面向安全关键软件的Ａ ＡＤ Ｌ 模型组合验证方法 ２ １ ４ ７２ ５ ００２ ０ ００１ ５ ００巻１ ０ ００５ ００１ １１ ０１ ５１５４０萬／图２ ０ 火箭发射控制系统验证结果折线图根据以上数据和图表可以得知， 使用本文提出的组合验证方法， 可以完成对一个复杂系统的验证，整个验证运行时间粗略统计约３ ０ｍ ｉｎ ． 实际上， 本文最初是想通过ＵＰ ＰＡ Ａ Ｌ 对整个模型进行验证分析， 如折线图中的消耗时间增长最快的折线． 事实证明， 直接使用Ｕ Ｐ ＰＡ Ａ Ｌ 对整个模型进行验证分析，单个功能性质可能需要耗费大量时间， 而且随着组件复杂度增加， 验证时间无法估计， 因为对于每一个验证性质都需要遍历所有的状态空间， 不可避免的面临状态空间爆炸问题．５ ． ３ 讨论在体系结构构造及需求形式化、体系结构模型组合验证和组件功能行为模型验证的过程中发现了一些错误和目前工程上的不足之处．（ １ ） 在体系结构构造及需求形式化方面， 首先发现了直接根据需求分解成子需求的结构去构造体系结构模型， 很容易导致体系结构模型的层次划分１ １ 期Ｅ ｃ ｌ ｉ ｐｓ ｅ 平台上， 按照需求层次构建体系结构模型，支持以插件的形式实现Ａ Ａ Ｄ Ｌ 模型的验证和分析工具．（ ２ ） 在模型转换方面， 本文采用了模型转换语言Ａ Ｔ Ｌ 实现了Ａ Ａ ＤＬ 模型到Ｕ Ｐ ＰＡ Ａ Ｌ 模型的自动转换， 并以插件的方式集成在开源建模环境Ｏ ＳＡ ＴＥ 上， 方便用户使用．（ ３ ） 在性质验证和分析方面， ＵＰ ＰＡ Ａ Ｌ 支持对可达性、安全性、功能正确性等性质验证从而完成对组件级需求的验证， 使用Ａ Ｇ ＲＥ Ｅ 完成对系统级需求的验证．（ ４ ） 在系统的应用方面， 在工业界项目的支持下， 本文对火箭发射控制子系统进行了建模和实例性验证．５ ． ２ 案例分析火箭发射系统是在从发射指令到火箭顺利离开发射装置期间， 控制火箭执行各项操作和火箭自动执行的发射控制功能的系统． 火箭发射控制系统的功能主要是根据主控任务的控制命令， 进行相应的命令的执行， 处于过程层的系统． 火箭发射控制子系统包括排气盖控制、箭舱盖控制、火箭发射准备／ 取消控制、火箭加电控制、箭舱解锁／锁定控制、热电池激活控制、安全机构解锁／恢复控制、火箭点火控制、火箭断电控制等功能． 通过对火箭发射控制系统进行体系结构建模， 完整的火箭发射控制系统的Ａ Ａ Ｄ Ｌ 模型的数据统计如表６ 所示．表６ 火箭发射控制系统的Ａ Ａ Ｕ Ｌ 模型的数据统计ＡＡＤ Ｌ 模型（ 行） 线程数量 子程序数量ＳＲ １ １ ８ ０ ０ ＋ ４ １ ４Ｓ Ｒ２ １ ６ ０ ０ ＋ ３ １ ２Ｓ Ｒ３ １ ６ ０ ０ ＋ ４ １ １Ｓ Ｒ４ ４ ０ ０ ０ ＋ １ ８ ３ ２Ｓ Ｒ５ ２ ０ ０ ０ ＋ ６ １ ３Ｓ Ｒ６ １ ８ ０ ０ ＋ ６ １ ５Ｓ Ｒ７ １ ９ ０ ０ ＋ ６ １ ５Ｓ Ｒ８ １ ７ ０ ０ ＋ ４ １ ３ＳＲ ９ １ ２ ０ ０ ＋ ４ ９火箭发射控制系统 １ ７ ６ ０ ０ ＋ ５ ５ １ ３４为了确保复杂系统火箭发射控制系统的正确性， 不仅需要对其体系结构模型进行验证， 确保其体系结构的正确性， 还需要对其组件功能行为进行验证， 确保其组件功能行为的正确性． 本文根据上述的组合验证方法， 在与工业界合作研究经过多次的验证分析修改后， 对火箭发射控制系统进行验证， 火箭发射控制系统的验证结果统计如表７ 所示， 其折线图如图２ ０ 所示． 表中的体系结构模型验证时间， 是在Ａ ＧＲ Ｅ Ｅ 工具下对于系统及子系统单次验证得到的； 表中的Ｕ ＰＰＡ Ａ Ｌ 验证时间， 因为ＵＰ ＰＡ Ａ Ｌ 验证是在每个子系统下对多个叶子组件进行多次模型转换， 分别对多个叶子组件做验证， 所以是粗略的对多个验证时间统计得出， 有少许偏差但是并不影响结果．表７ 火箭发射控制系统的验证结果统计契约数量体系结构模型验证时间／ ｓＵ ＰＰ ＡＡＬ验证时间／ ｓＳＲ １ １ ３ １ １ １ １ ０ＳＲ ２ １ ０ １ ０ ８ ０ＳＲ３ １ ２ １ ２ ９０ＳＲ４ ６ ４ ４ ０ ７０ ０ＳＲ５ １ ５ １ ５ １ ４ ０ＳＲ６ １ ４ １ ５ １ ５ ０ＳＲ７ １ ４ １ ０ １ ４ ０Ｓ Ｒ８ １ ０ ８ ８ ０Ｓ Ｒ９ ７ ３ ３ ０火箭发射控制系统 １ ７ ０ １ ３ ７ １ ５ ２ ０７０３ ０ ００－ Ｘ － 契约数量＋ 仅仅使用…＆ ＵＰＰ ＡＡ Ｌ验证时间－■ ■ 体系结构模型验证时间２ １ ４ ８ 计 算 机 ２ ０ ２ ０年错误． 其次， 需求形式化过程中很明显地可以发现需求分解的过程中对各个子组件的输人输出描述不精确．（ ２ ） 在体系结构模型组合验证方面， 错误一般都是由于错误的连接导致的． 虽然在经过严格的体系结构建模以及需求形式化以及将大部分的错误排除在外， 但是组件与组件之间的交互关系， 在需求分解的时候很容易被忽视， 因此在进行需求分解的同时， 顶层需求要不断的根据需求的分解清晰的表达各个子需求之间的交互关系， 从而在构件体系结构模型的时候才能保证模型能够满足其需求．（ ３ ） 在组件功能行为模型验证方面， 错误一般出现在数据处理的问题上． 使用子程序和行为附件细化组件行为构造组件功能行为模型时， 涉及了大量的输出输人数据的处理， 当把输入的指令由子程序转换为相应的数据处理时， 往往会出现由数据处理导致的组件功能错误．（ ４ ） 在整个验证过程中， 大多数的错误都是发生在功能行为模型验证中， 但是体系结构模型的错误一旦出现很难修复． 这是因为体系结构错误涉及是系统的整个结构， 错误出现后需要对整个体系结构进行调整， 体系结构模型的调整包括模型的组件划分、输人端口、输出端口以及组件交互等． 虽然体系结构的错误修复代价高， 但是相对于传统的验证方法， 在系统体系结构建模时期验证其正确性， 能够在整个系统开发的早期识别体系结构错误， 而不是在系统集成和系统测试阶段， 能够降低成本． 此外，通过组合验证与模型转换相结合的方式， 能够有效减少状态空间爆炸问题， 可以完成对复杂系统的验证分析．本文的提出的组合验证方法目前有如下局限性：（ １ ） 基于契约的需求形式化的过程中， 主要是通过手工进行的， 这样就导致了人为因素的错误加人到组件的约束中， 会对体系结构的验证加人不确定因素．（ ２ ） 用于组合验证的Ａ ＧＲ ＥＥ 工具有很多的局限性， 并不能全面地验证功能／非功能需求是否满足， 目前Ａ ＧＲ Ｅ Ｅ 能够支持ＡＡ ＤＬ 同步子集模型，执行以确定的离散序列进行， 并不能支持对于Ａ Ａ ＤＬ 模型中的异步模型、事件数据端口和模型间的延时通信等． 在构建体系结构模型的时候， 很多情况是模拟组件的输人输出数据， Ａ Ｇ ＲＥＥ 很难去支持复杂数据处理， 例如位运算、三角函数或者是非线性函数．学报（ ３ ） 本文对叶子组件的需求进行了两次形式化， 第一次将组件需求形式化为契约为组件约束进行组合验证； 第二次是进行叶子组件的功能行为模型验证形式化为ＵＰ ＰＡＡ Ｌ 的ＴＣＴ Ｌ 公式． 两次的需求形式化工作实际上增加了很多的验证成本．但是上述局限性对火箭发射控制系统并没有很明显的影响， 因为数据处理由单独的子程序来完成，该系统很多情况下延时都由看门狗叶子组件实现，所以大多数需求都能得到验证． 现在也已经考虑从限定自然语言自动生成契约， 从而减少由人工导致的不确定因素．６ 相关工作本文的相关工作主要包括两个方面： Ａ Ａ ＤＬ 模型到模型转换和组合验证．６ ． １ 模型转换相关工作模型转换是对ＡＡＤＬ 模型的验证与分析的一种重要手段， 有很多针对ＡＡＤＬ 模型转换的研究， 例如转换到定时抽象状态机（ Ｔ Ａ ＳＭ ） 、Ｂ Ｉ Ｐ、ＦＩ Ａ ＣＲＥ、动作时序逻辑ＴＬ Ａ＋ 、同步语言Ｓ ｉ ｇｎ ａ ｌ 、Ｓ ｔ ａ ｔ ｅ ｆ ｕ ｌＴｉ ｍ ｅ ｄＣＳ Ｐ 等目标语言， 但是都缺少对子程序调用的转换验证．Ｃｈｋ ｏ ｕｒ ｉ 等人提出了一种将Ａ Ａ ＤＬ 模型转换到ＢＩＰ 模型的验证方法：１ ２］， 提出的转换规则主要是针对进程、线程、处理器等组件的执行模型， 但是在线程与线程间通信和Ａ Ａ Ｄ Ｌ 行为附件的转换不够全面．Ｔ ＯＰＣＡ ＳＥＤ 项目提出了一种将ＡＡ Ｄ Ｌ 模型转换到Ｆｉ ａ ｃ ｅ 模型的验证方法［ １ ３］， 该研究主要关注的是线程和线程间通信的Ａ Ａ ＤＬ 模型子集． Ｆ ｉ ａｃ ｅ 可以支持行为和时间描述的建模语言， 其建模的主要组件是进程和构件， 进程的一般描述是有输人输出端口的组件， 组件的行为使用的是状态和状态变迁表达， 在其模型中一个构件可以由多个进程组成． 主要的转换过程是将Ａ ＡＤ Ｌ 的线程和线程间通信分别映射为进程和进程行为， 然后基于Ｒ ａ ｃ ｅ 可以对Ａ Ａ Ｄ Ｌ 线程的分发和调度进行验证分析．Ｊ ｅａ ｎ－Ｆｒ ａ ｎｃｏｉ ｓ 提出将Ａ ＡＤＬ 模型转换到ＴＬＡ ＋的验证方法［１ １］， 提出的转换规则主要涉及到ＡＡＬＤ模型中执行模型的端口通信、共享变量和模式变换，但是ＴＬ Ａ ＋ 的所依赖的模型检测工具ＴＬＣ 验证能力不足？Ｍ ａ 等人提出了将ＡＡ ＤＬ 模型转换到同步语言张博林等：一种面向安全关键软件的ＡＡＤＬ 模型组合验证方法 ２ １ ４ ９ ｎ 期Ｓ ｉ ｎｇ ａｌ 的验证方法Ｍ， 提出的转换规则主要涉及线程执行、通信以及行为附件等， 还给出了系统组件和线程组件的形式语义， 其转换规则通过语义函数的方式给出．Ｎｕｚ ｚ ｏ 提出了ＡＡ Ｄ Ｌ 模型到有状态定时ＣＳＰ的转换规则［１ ６］． 然后， 在Ｐ Ａ Ｔ 中进行形式化验证，对ＡＡＤＬ 模型的并发行为特性进行验证分析， 如安全性、活动性， 其中考虑了时间容量、截止日期、Ａ Ａ ＤＬ 线程的周期和Ａ ＡＤ Ｌ 进程的持续时间．Ｙａ ｎ ｇ 等人提出了Ａ ＡＤ Ｌ 模型到Ｔ Ａ ＳＭ 模型的转换规则［２ ４］． 将Ａ ＡＤ Ｌ 模型中的周期线程、数据端口通信、模式变换和ＡＡ Ｄ Ｌ 的行为附件转换为ＴＡＳＭ 模型， 基于形式语义和元模型定义了转换规则， 实现了基于Ｏ ＳＡ ＴＥ 的Ａ ＡＤＬ ２ ＴＡ ＳＭ 的自动转换工具， 对模型的时间特性、可达性、活性等进行了验证分析．６． ２ 组合验证相关工作组合验证作为一种可扩展的推理技术， 在复杂系统的验证方面已经引起人们的广泛关注． 基于组件的设计和基于契约的设计等方法正在作为统一的形式化组合规范出现． 通过严格的形式化方式来对系统中的不同抽象层次进行推理， 从而支持需求工程， 配合基于契约的组合验证理论， 可以检测早期集成出现的错误， 还能够进行全局系统验证， 检测组件之间的兼容性等能力． 组合验证在程序验证、面向对象编程、模型驱动开发、系统设计与开发等领域都有广泛的应用．在面向对象编程方面， Ｂｅ ｒｇ ｍａｎ ｓ 等人［ ２ ５］ 提出了Ｃｏｍｐ ｏｓ ｉ ｔｉ ｏｎ － Ｆｉｌ ｔ ｅ ｒ ｓ 模型， 该模型将类似数据库的功能集成到面向对应的语言中， 对面向对象中的数据抽象、封装、消息传递和继承之类的对象功能统一集成， 然后将对象再分为接口对象和操作集两个部分， 接口对象负责根据外部消息， 判断需要执行的操作集． Ｎ ｉ ｅｒ ｓ ｔ ｒ ａ ｓ ｚ 等人［２ ６］ 提出一种基于组合理论的设计模式， 通过这种设计模式可以构造各个组件与组件之间的关系， 在这种模式下的组件组合过程能够完成面向对象应用程序的开发． Ｌｉ ａ ｎｇ 等人［２ ７］提出将Ｒ ＧＳｉ ｍ （ Ｒｅ ｌ ｙ－Ｇ ｕａ ｒａ ｎ ｔｅ ｅ － ｂ ａｓ ｅ ｄＳ ｉ ｍｕ ｌ ａｔ ｉｏ ｎ ）来验证并发程序的转换， 考虑了并行组合的线程间约束和线程运行环境约束下验证分析．在模型驱动开发方面， ＵＭ Ｌ 中采用的模型约束语言ＯＣ Ｌ［２ ８ ］ （ Ｏ ｂｊｅ ｃ ｔＣｏ ｎ ｓ ｔ ｒａ ｉ ｎｔ ｌ ａｎ ｇ ｕａ ｇｅ ） 可以为构件模型元素、行为建立各类功能／ 非功能约束，可以对ＵＭ Ｌ 模型进行验证分析． Ｐ ＥＣＯＳ 项目［２ ９］的研究工作中， 在使用Ｔ ｉｍｅ ｄＰ ｅ ｔ ｒ ｉＮ ｅ ｔ 描述组件的模型过程中， 通过对组件使用时间约束来表达组件对行为时间特性的描述， 然后在工具支持下进行时间特性的行为预测并且能够提供各种实时调度策略．组合验证在ＡＡＤＬ 模型的验证分析中也有广泛的应用． ＢＬＥＳ Ｓ 附件和工具［ ３ °］ 支持使用状态机和简单命令式语言定义的组件级行为的推理， 它支持组件的不变量和组件行为的模型．Ｍｕ ｒｕｇ ｅ ｓａ ｎ 等人［３ １］ 从需求分解的角度分层构造组件的契约， 然后使用Ｓｉ ｍ ｕｌｉ ｎ ｋ 描述组件级行为， 从而验证系统的体系结构设计和需求是否正确． Ｂａ ｃ ｋ ｅｓ 等人［５］ 使用ＡＧＲ ＥＥ 对飞行控制系统模型实例进行分析， 模型中每个组件都用契约进行注释， 然后基于组件契约对系统级行为进行推理， 将验证扩展到处理大型系统， 从而验证整个系统．相比已有的研究，一方面采用了ＡＧ Ｒ ＥＥ 和Ｕ ＰＰ Ａ ＡＬ 相结合的方式对工业界实际案例进行验证分析； 另一方面在和工业界合作研究过程中， 将工业界需要验证的实际需求和Ａ Ｇ ＲＥＥ 组合验证能力反复对比和分析， 从而洞察出一些真正需要扩展的理论点．７ 总结与展望首先， 本文提出了Ａ ＡＤＬ 体系结构模型的组合验证方法， 将系统各个层次的组件需求形式化为组件契约， 进一步验证系统体系结构的正确性． 其次，本文提出了Ａ Ａ ＤＬ ２ Ｕ ＰＰ ＡＡ Ｌ 的模型转换方法， 将ＡＡ Ｄ Ｌ 模型转换为Ｕ ＰＰ ＡＡ Ｌ 模型对体系结构模型的叶子组件的功能行为进行验证与分析． 最后， 基于开源建模环境ＯＳＡ Ｔ Ｅ ， 我们设计并实现了ＡＡＤＬ模型验证原型工具， 采用了ＡＧ ＲＥＥ 和Ｕ ＰＰ ＡＡＬ相结合的方式对工业界实际案例进行验证， 并通过对工业界实际案例分析了Ａ Ａ ＤＬ 组合验证工具的有效性和局限性．在未来工作中， 我们将进一步开展以下几个方面的研究工作：（ １ ） 在基于契约的需求形式化方面， 现在使用手工的方法将需求形式化为契约， 为验证工作增加了错误因素， 在以后的工作中， 考虑通过限定自然语言规范化需求， 然后将限定自然语言转换为契约约束组件， 从而保证契约构造的正确性， 减少人为因素．（ ２ ） 由于Ａ Ｇ ＲＥ Ｅ 只支持同步子集， 不支持异２ １ ５ ０ 计算机学报 ２ ０２ ０ 年步子集、事件数据端口、延时通信等Ａ ＡＤ Ｌ 模型子集， 所以考虑进一步扩展Ａ Ｇ ＲＥＥ 支持的模型子集，满足模型验证需求．（ ３ ） 考虑到叶子组件需求经过两次形式化，一次形式化为契约， 另一次形式化为ＴＣＴＬ 路径公式， 所以未来工作会尝试将契约映射到ＵＰＰ ＡＡ Ｌ验证中的ＴＣＴ Ｌ 公式， 从而进一步方便验证人员的工作．参考文献［ １ ］Ｍａ ｒ ｔｉ ｎｓＬ Ｅ Ｇ ， Ｇｏ ｒ ｓｃ ｈ ｅｋ Ｔ ．Ｒｅ ｑ ｕ ｉ ｒｅｍｅ ｎｔ ｓ ｅｎｇ ｉ ｎ ｅ ｅ ｒｉ ｎｇｆ ｏ ｒｓａｆ ｅｔ 广ｃｒ ｉｔｉ ｃａｌ ｓ ｙ ｓｔ ｅｍｓ ：Ｏ ｖｅ ｒｖ ｉ ｅｗａｎ ｄ ｃ ｈａｌ ｌ ｅｎｇ ｅｓ． ＩＥＥＥＳ ｏｆ ｔｗ ａｒｅ ，２ ０ １ ７，  ３ ４ （ ４ ） ： ４ ９ － ５ ７［ ２ ］Ｒｉ ｅｒｓｏ ｎＬ． Ｄｅ ｖ ｅｌｏ ｐｉ ｎｇ Ｓａｆ ｅ ｔｙ－Ｃｒｉｔｉ ｃａ ｌ Ｓｏｆ ｔ ｗａ ｒ ｅ ： ＡＰｒａ ｃｔｉｃ ａｌＧｕ ｉ ｄ ｅ ｆ ｏ ｒ Ａｖｉ ａ ｔｉｏｎ Ｓｏ ｆｔ ｗａｒ ｅ ａｎ ｄ ＤＯ－ １ ７ ８ Ｃ ｃｏｍｐ ｌｉ ａｎ ｃｅ． ＢｏｃａＲ ａｔ ｏ ｎ： Ｃ ＲＣ Ｐｒｅ ｓ ｓ， ２０ １ ３［ ３ ］Ｆｒ ａ ｎｚ ａｇ ｏＭ ， Ｒｕ ｓｃｉ ｏ Ｄ Ｄ ，Ｍａ ｌａ ｖ ｏ ｌｔ ａＩ ， ｅ ｔ ａｌ ．  Ｃｏ ｌ ｌ ａ ｂ ｏ ｒａ ｔｉｖ ｅｍｏ ｄ ｅ ｌ－ ｄ ｒｉ ｖｅ ｎ ｓｏ ｆ ｔ ｗａ ｒｅ ｅｎｇ ｉ ｎ ｅｅ ｒｉｎｇ； Ａ ｃｌ ａ ｓ ｓ ｉｆｉ ｃａ ｔｉ ｏ ｎｆｒ ａ ｍｅ？ｗｏｒｋ ａ ｎ ｄ ａ ｒｅｓ ｅａｒ ｃｈｍａ ｐ． Ｉ ＥＥＥＴｒａ ｎｓａ ｃｔｉｏ ｎｓ ｏ ｎ Ｓｏｆ ｔ ｗａ ｒｅＥｎｇｉ ｎ ｅｅ ｒｉ ｎｇ ， ２ ０ １ ８ ，  ４ ４ （ １ ２ ） ； １ １ ４ ６ － １ １ ７ ５［４ ］Ｃｏ ｂ ｌ ｅｉ ｇｈ  ＪＭ ，Ｇｉ ａｎｎ ａｋｏ ｐ ｏ ｕ ｌ ｏ ｕ Ｄ ， Ｐａ ｓａ ｒ ｅａ ｎｕＣ ，ｅｔ ａｌ ．Ｌｅ ａｒｎｉｎｇ ａ ｓ ｓ ｕｍｐ ｔｉｏ ｎ ｓｆ ｏ ｒ ｃｏｍ ｐ ｏ ｓｉｔｉｏ ｎａ ｌ ｖ ｅｒｉｆｉｃ ａ ｔｉ ｏ ｎ／ ／ Ｔｏ ｏ ｌ ｓａｎ ｄＡｌｇ ｏ ｒｉ ｔｈｍｓ  ｆ ｏｒ ｔ ｈ ｅ Ｃｏ ｎｓ ｔｒ ｕ ｃ ｔｉ ｏ ｎａｎ ｄ Ａｎａ ｌ ｙ ｓｉ ｓ ｏ ｆ Ｓｙｓｔ ｅｍｓ ．Ｂｅ ｒ ｌｉ ｎ ， Ｇｅ ｒｍａ ｎｙ ： Ｓｐｒｉ ｎｇｅ ｒ ， ２ ０ ０ ３［ ５ ］Ｃｏ ｆ ｅｒ  Ｄ，Ｇ ａ ｃｅ ｋＡ ，Ｂａ ｃｋｅ ｓＪ ，ｅ ｔ ａｌ ．Ａ  ｆｏ ｒｍａ ｌ  ａｐ ｐ ｒｏ ａ ｃｈ ｔ ｏｃｏ ｎｓ ｔｒ ｕ ｃ ｔ ｉ ｎｇ ｓ ｅｃｕ ｒｅ ａ ｉ ｒｖ ｅｈ ｉｃ ｌ ｅｓ ｏ ｆｔ ｗａｒｅ ．Ｃｏ ｍｐ ｕｔ ｅ ｒ？ ２ ０ １ ８，５ １ （ １ １ ） ： １ ４ － ２ ３［ ６ ］Ｃｈ ｅ ｎ Ｈ ， Ｗ ｕ Ｎ ， Ｓ ｈａｏ  Ｚ ， ｅ ｔ ａ ｌ ． Ｔ ｏ ｗａ ｒ ｄ ｃ ｏｍ ｐ ｏ ｓｉ ｔ ｉ ｏ ｎ ａ ｌ ｖ ｅ ｒｉ ｆｉ？ｃａ ｔｉ ｏｎ ｏ ｆｉ ｎ ｔ ｅｒ ｒ ｕ ｐ ｔｉｂ ｌ ｅ ＯＳ ｋｅ ｒｎｅ ｌ ｓ ａｎｄ  ｄ ｅｖ ｉ ｃ ｅｄ ｒ ｉ ｖ ｅｒｓ ． Ｊｏ ｕ ｒｎ ａｌｏｆ Ａｕ ｔ ｏｍａ ｔ ｅｄ Ｒ ｅ ａｓｏ ｎｉ ｎｇ ， ２ ０ １ ７ ，  ５ １ （ ６ ） ： １ －４ ９［ ７ ］Ｙａｎｇ ＺＢ ， Ｌｅｉ Ｐ Ｉ， Ｈ ｕ Ｋ ， ｅ ｔ ａｌ ．  ＡＡＤＬ ： Ａｎ ａ ｒｃ ｈｉｔ ｅ ｃｔ ｕ ｒｅｄ ｅｓ ｉ ｇ ｎ ａ ｎ ｄ  ａ ｎ ａｌ ｙ ｓ ｉ ｓ ｌ ａｎ ｇ ｕ ａｇｅ  ｆｏ ｒ  ｃｏｍｐ ｌ ｅ ｘ ｅｍｂ ｅ ｄｄ ｅｄ ｒ ｅａ ｌ－ ｔｉｍｅｓｙｓｔ ｅ ｍｓ． Ｊ ｏ ｕ ｒ ｎ ａ ｌ ｏ ｆ Ｓｏｆ ｔ ｗａ ｒ ｅ ，２ ０ １ ０， ２ １ （ ５ ） ： ８ ９ ９ － ９ １ ５［ ８ ］Ｂｅｒｔ ｈｏｍｉ ｅ ｕ Ｂ ，Ｂｏｄ ｅｖ ｅ ｉ ｘ ＪＰ ， Ｃｈａｕ ｄ ｅ ｔＣ ，ｅｔ ａ ｌ ． Ｆｏ ｒｍ ａｌｖｅｒｉｆｉ ｃａ ｔ ｉｏ ｎｏ ｆ ＡＡ ＤＬｓ ｐ ｅ ｃｉ ｆ ｉ ｃａ ｔｉ ｏ ｎ ｓｉ ｎｔ ｈ ｅＴＯＰＣ ＡＳ ＥＤｅｎｖｉｒｏｎｍ ｅｎ ｔ ／ ／ Ｐｒ ｏ ｃｅ ｅｄｉ ｎｇｓ ｏ ｆ ｔ ｈｅ Ｉ ｎ ｔ ｅｒ ｎａ ｔｉ ｏ ｎａ ｌ Ｃｏ ｎ ｆ ｅ ｒｅ ｎ ｃｅ ｏ ｎＲ ｅｌ ｉ ａ ｂｌ ｅ Ｓｏｆ ｔｗａ ｒ ｅ Ｔｅｃ ｈｎｏ ｌ ｏ ｇｉ ｅ ｓ ． Ｂｒ ｅ ｓｔ ， Ｆｒ ａ ｎｃｅ ＾  ２ ０ １ ８ ： ２ ０ ７－２ ２ １［９］Ｃｏｆｅｒ Ｄ， Ｇ ａｃｅ ｋ Ａ ，Ｍｉｌｌｅ ｒＳ ？ ｅ ｔ ａ ｌ ． Ｃｏｍｐ ｏｓ ｉｔｉ ｏ ｎａｌ ｖ ｅ ｒｉｆｉｃ ａｔｉｏ ｎｏ ｆ ａｒｃ ｈｉｔｅｃ ｔｕ ｒａ ｌ ｍｏ ｄｅｌｓ ．Ｌｅ ｃｔ ｕ ｒｅＮｏ ｔ ｅｓ ｉｎＣｏｍｐ ｕ ｔｅ ｒ Ｓｃｉｅｎ ｃｅ？２ ０ １ ２，７ ２ ２ ６ ： １ ２ ６－１ ４ ０［ １ ０ ］Ｂａｃ ｋｅｓ Ｊ ，Ｃｏ ｆ ｅｒ  Ｄ ，Ｍｉｌ ｌ ｅｒＳ ，ｅ ｔ ａ ｌ ． Ｒ ｅｑ ｕ ｉｒｅ ｍｅｎ ｔ ｓａ ｎ ａ ｌｙ ｓｉ ｓ  ｏ ｆａ ｑｕ ａｄ －ｒ ｅｄ ｕ ｎｄ ａ ｎｔ  ｆｌ ｉｇ ｈ ｔ ｃｏ ｎ ｔ ｒｏ ｌｓ ｙ ｓｔｅ ｍ． Ｃｏ ｍｐ ｕ ｔ ｅ ｒＳ ｃｉ ｅｎ ｃｅ，２ ０ １ ５，９ ０ ５ ８ ： ８ ２－ ９ ６［ １ １ ］Ｗｈ ａｌ ｅ ｎ ＭＷ ，Ｇ ａｃ ｅｋ Ａ ， Ｃｏ ｆ ｅｒ  Ｄ ， ｅｔ ａ ｌ ． Ｙｏ ｕ ｒ“Ｗｈ ａｔ”ｉ ｓｍ ｙ“Ｈｏ ｗ”：Ｉ ｔ ｅｒ ａ ｔｉ ｏｎ ａ ｎｄｈ ｉ ｅｒａ ｒｃ ｈｙｉ ｎ ｓｙ ｓｔ ｅ ｍｄｅ ｓｉｇｎ ．Ｉ ＥＥＥＳｏ ｆ ｔｗａ ｒｅ ， ２ ０ １ ３ ， ３ ０ （ ２ ） ： ５ ４ －６ ０［ １ ２ ］Ｃｈｋｏ ｕ ｒｉ ＭＹ ，ｅ ｔａ ｌ． Ｔｒａ ｎｓｌ ａｔ ｉ ｎｇ ＡＡＤＬ ｉ ｎｔ ｏ ＢＩ Ｐ－ ａｐ ｐ ｌ ｉ ｃａｔｉ ｏ ｎｔ ｏ ｔ ｈｅ ｖ ｅｒｉｆ ｉ ｃａ ｔｉ ｏ ｎｏ ｆ  ｒ ｅａ ｌ－ ｔｉｍｅ  ｓ ｙ ｓ ｔ ｅｍｓ ／ ／ Ｐｒ ｏ ｃｅｅ ｄ ｉ ｎｇ ｓ ｏ ｆ ｔ ｈｅＩ ｎｔ ｅｒｎａ ｔ ｉｏ ｎａｌＣｏｎｆ ｅｒｅ ｎｃｅ ｏ ｎＭｏ ｄ ｅ ｌＤ ｒｉ ｖ ｅｎ Ｅｎ ｇｉ ｎｅ ｅｒｉｎｇＬａ ｎｇ ｕ ａｇ ｅ ｓ  ａｎｄ  Ｓｙ ｓ ｔｅ ｍｓ． Ｂｅｒｌｉ ｎ ， Ｇｅｒｍ ａｎ ｙ ， ２ ０ ０ ８ ： ５－１ ９［ １ ３］Ｂｏ ｄｅ ｖ ｅｉ ｘ Ｊ－Ｐ ，ｅｔ ａ ｌ． Ｔ ｏｗａ ｒｄ ｓ ａ ｖ ｅｒｉ ｆｉ ｅｄ  ｔ ｒａ ｎ ｓ ｆｏ ｒｍａ ｔ ｉｏ ｎｆ ｒｏｍＡＡＤＬ ｔｏ ｔ ｈ ｅｆ ｏ ｒｍａｌ ｃｏｍｐ ｏ ｎｅ ｎｔ－ ｂ ａ ｓｅ ｄｌ ａ ｎｇ ｕ ａｇ ｅ ＦＩ ＡＣＲＥ．Ｓ ｃｉ ｅｎ ｃｅ ｏ ｆ Ｃｏｍｐ ｕ ｔ ｅｒ  Ｐｒ ｏ ｇ ｒａ ｍｍｉ ｎｇ ，  ２ ０ １ ５ ， １ ０ ６ ：  ３０－５ ３［ １ ４ ］Ｒ ｏｌ ｌ ａｎｄ Ｊ ＊ Ｂ ｏｄｅ ｖｅｉ ｘ Ｊ ， Ｆｉｌ ａｌｉＭ ， ｅｔ ａｌ． Ｍｏ ｄ ｅｓ ｉ ｎ ａｓｙｎ ｃｈｒｏ ｎｏ ｕｓｓ ｙｓ ｔｅｍ ｓ／ ／ Ｐｒ ｏｃｅ ｅｄ ｉｎ ｇｓ ｏ ｆ ｔ ｈｅ １ ３ ｔ ｈＩＥＥＥ Ｉ ｎｔｅ ｒｎａｔｉｏ ｎ ａｌ Ｃｏ ｎｆ ｅｒｅｎｃｅｏ ｎＥｎｇ ｉ ｎ ｅ ｅｒ ｉｎｇ ｏｆＣｏ ｍｐ ｌ ｅ ｘ Ｃｏｍｐｕ ｔ ｅ ｒＳｙ ｓ ｔ ｅ ｍｓ（ Ｉ ＣＥＣＣＳ２ ０ ０ ８ ） ． Ｂｅ ｌ ｆ ａ ｓｔ，ＵＫ ， ２ ０ ０ ８ ： ２ ８ ２ －２ ８ ７［ １ ５］Ｍａ Ｙ ，Ｔ ａｌ ｐ ｉ ｎＪ ，Ｇａ ｕ ｔ ｉ ｅｒＴ．Ｖｉ ｒｔ ｕａ ｌｐ ｒ ｏ ｔｏ ｔ ｙ ｐ ｉ ｎｇＡＡＤ Ｌａ ｒｃｈ ｉ ｔｅ ｃｔ ｕｒｅ ｓｉ ｎ ａｐｏ ｌ ｙ ｃ ｈｒｏ ｎｏ ｕ ｓｍｏ ｄｅ ｌｏ ｆｃ ｏ ｍｐ ｕ ｔ ａ ｔｉ ｏ ｎ／ ／Ｐ ｒｏｃｅ ｅｄ ｉ ｎｇｓ ｏｆｔ ｈｅ ２０ ０ ８６ ｔ ＫＡＣＭ／ ＩＥＥＥＩ ｎ ｔ ｅ ｒｎ ａ ｔｉ ｏ ｎ ａ ｌＣｏ ｎｆ ｅ ｒ ｅｎｃ ｅ ｏ ｎＦｏ ｒｍａ ｌＭｅｔ ｈｏ ｄ ｓ ａ ｎｄ Ｍｏ ｄ ｅｌ ｓ ｆ ｏ ｒ Ｃｏ －Ｄｅ ｓ ｉ ｇｎ ．Ａｎａ ｈｅ ｉｍ ， ＵＳＡ ， ２ ０ ０ ８ ：１ ３ ９－１ ４ ８［ １ ６］Ｆｅ ｎｇ Ｚ ？ Ｙｏ ｎｇｗａ ｎｇ Ｚ ？ Ｄ ｉ ａｎｆ ｕ Ｍ ？ ｅ ｔ ａｌ． Ｆｏ ｒｍａ ｌ ｖ ｅ ｒ ｉ ｆｉ ｃａｔ ｉ ｏ ｎｏ ｆ ｂ ｅ ｈ ａｖ ｉｏ ｒａ ｌ ＡＡ ＤＬｍｏ ｄ ｅ ｌ ｓｂｙ ｓｔ ａｔ ｅ ｆｕ ｌ ｔ ｉ ｍｅ ｄＣＳＰ ．ＩＥＥＥＡ ｃ ｃｅｓ ｓ，２ ０ １ ７，５ ： ２ ７ ４ ２ １－ ２ ７ ４ ３８［ １ ７ ］Ｂｅ Ｋｒｒａａ ｎｎ Ｇ ＞Ｄ ａｖ ｉ ｄ Ａ，  Ｌａｒ ｓｅｎ  ＫＧ．Ａｔｕ ｔ ｏ ｒｉ ａ ｌ ｏ ｎ ＵＰＰ ＡＡＬ／ ／ Ｆｏ ｒｍａ ｌ Ｍｅｔ ｈｏ ｄ ｓｆ ｏ ｒ ｔｈ ｅＤ ｅ ｓ ｉ ｇｎｏ ｆ Ｒ ｅａ ｌ－Ｔｉ ｍｅ Ｓｙ ｓ ｔｅｍ ｓ．Ｂｅｒｌｉ ｎ ， Ｇｅｒｍａ ｎｙ ：Ｓｐ ｒｉ ｎｇ ｅｒ ，２ ０ ０ ４［ １ ８ ］Ｚ ｈｕＸ ｕ ｅ－ Ｙａ ｎｇ ， Ｔ ａｎｇＺ ｈｉ－ Ｓｏ ｎｇ．Ａ ｔｅ ｍｐ ｏ ｒａｌ ｌ ｏ ｇｉｃ － ｂ ａｓ ｅｄｓ ｏ ｆ ｔ ｗａｒｅ ａｒｃ ｈｉ ｔ ｅｃｔ ｕ ｒ ｅｄ ｅｓ ｃｒｉｐ ｔｉ ｏ ｎｌ ａ ｎｇｕ ａ ｇ ｅＸＹＺ ／ ＡＤＬ．Ｊｏ ｕ ｒ ｎａｌ ｏ ｆ Ｓｏｆ ｔ ｗａｒｅ ， ２ ０ ０ ３ ， １ ４ （ ４ ）：７ １ ３－ ７ ２ ０ （ ｉ ｎＣｈ ｉ ｎｅｓ ｅ）（ 朱雪阳， 唐稚松． 基于时序逻辑的软件体系结构描述语言Ｘ ＹＺ ／ ＡＤＬ． 软件学报， ２ ０ ０ ３， １ ４ （ ４ ） ：７ １３ － ７ ２０ ）［ １ ９ ］Ｚ ｈａｎ Ｈａｏ ｌ ａｎ ＊ ｅ ｔ ａｌ ．Ｕ ｎｉｆｉｅ ｄ ｇ ｒ ａｐｈｉ ｃａｌ ｃ ｏ－ｍｏ ｄ ｅｌ ｌｉ ｎ ｇｏ ｆ ｃｙ ｂ ｅｒ？ｐ ｈｙ ｓ ｉ ｃａ ｌｓ ｙｓ ｔ ｅｍｓ ｕ ｓｉｎ ｇＡＡＤ Ｌａ ｎｄＳｉｍｕ ｌｉｎ ｋ／ Ｓｔ ａｔ ｅ ｆｌｏｗ／ ／Ｐｒｏ ｃｅ ｅｄ ｉｎｇ ｓ ｏ ｆｔ ｈｅ Ｉｎ ｔｅ ｒｎａ ｔ ｉ ｏｎａ ｌ Ｓｙｍｐ ｏ ｓ ｉ ｕｍ ｏ ｎＵｎｉｆ ｙ ｉｎｇＴ ｈｅｏ ｒ ｉ ｅｓ ｏｆ Ｐ ｒｏ ｇｒａ ｍｍ ｉ ｎｇ． Ｂｅ ｒ ｌ ｉ ｎ ， Ｇｅｒｍａ ｎｙ ， ２ ０ １ ９ ： １ ０ ９ － １２ ９［ ２ ０］Ｗ ａｎｇ  Ｆ ， Ｙａ ｎｇＺ ， Ｈｕａ ｎｇ Ｚ ， ｅ ｔａ ｌ． Ａｐｐｒｏ ａ ｃｈ ｆｏ ｒ ｇｅ ｎｅ ｒａｔ ｉ ｎｇＡＡＤＬ ｍｏ ｄ ｅｌ  ｂ ａｓ ｅｄ ｏｎ ｒｅｓｔｒｉｃｔｅ ｄ ｎ ａｔ ｕｒ ａｌ ｌ ａｎｇ ｕａｇｅ  ｒ ｅｑ ｕｉ ｒｅｍｅｎ ｔｔ ｅｍｐ ｌ ａ ｔｅ ． Ｊ ｏ ｕ ｒｎａ ｌ ｏ ｆ Ｓ ｏｆ ｔ ｗａ ｒｅ ，  ２ ０ １ ８ ＊  ２ ９ （ ８ ） ： ２ ３ ５ ０ － ２ ３ ７ ０［ ２ １ ］Ｄｉｍｏ ｖ ｓｋｉ ＡＳ ＊Ｗ＾ｓｏｗｓｋｉ Ａ．Ｆ ｒ ｏｍｔ ｒａ ｎｓｉｔｉｏ ｎｓｙ ｓ ｔｅ ｍｓｔ ｏｖ ａ ｒｉａｂ ｉ ｌ ｉｔｙ ｍｏ ｄ ｅ ｌ ｓ ａ ｎｄｆ ｒｏｍｌ ｉ ｆｔ ｅ ｄ ｍｏ ｄ ｅｌ ｃｈ ｅ ｃｋｉｎ ｇ ｂａ ｃｋｔ ｏＵＰＰＡＡＬ／ ／ Ｍｏ ｄｅｌｓ？Ａｌｇｏ ｒｉ ｔｈ ｍｓ， Ｌｏ ｇｉ ｃｓ ａｎ ｄＴｏ ｏ ｌ ｓ． Ｂｅ ｒｌ ｉｎ，Ｇｅｒｍａ ｎｙ ：  Ｓｐ ｒｉ ｎｇ ｅ ｒ ，  ２０ １ ７［ ２ ２ ］Ｈａｍｍｏｎｄ Ｊ ， Ｒ ａｗｌｉｎｇｓＲ ，Ｈ ａｌ ｌ Ａ．Ｗｉｌ ｌ Ｉ ｔ Ｗｏ ｒ ｋ？／ ／Ｐ ｒ ｃｘｅ ｅｄｉ ｎｇｓｏ ｆ ｔ ｈｅ  ５ ｔｈ Ｉ ＥＥＥ Ｉｎ ｔ ｅｒ ｎａ ｔ ｉｏ ｎａｌ Ｓ ｙｍｐ ｏ ｓｉ ｕｍ ｏ ｎＲ ｅｑ ｕ ｉ ｒ ｅｍｅ ｎｔ ｓＥｎｇｉ ｎ ｅｅｒｉ ｎ ｇ （ ＲＥ ２０ ０ １ ） ．Ｔｏ ｒ ｏ ｎｔ ｏ ，Ｃａ ｎ ａ ｄａ，２０ ０ １ － １ ０ ２－１ ０ ９［ ２ ３ ］Ｋ ｈａ ｎＹ ，Ｈａ ｓｓ ｉ ｎｅ Ｊ．Ｍｕ ｔ ａ ｔ ｉ ｏ ｎｏ ｐ ｅｒａ ｔ ｏ ｒ ｓｆｏ ｒｔ ｈｅａ ｔ ｌａ ｓｔ ｒ ａ ｎｓ ｆｏ ｒ ｍａｔ ｉ ｏ ｎ ｌ ａ ｎ ｇ ｕ ａ ｇ ｅ／ ／ Ｐｒ ｏ ｃｅ ｅｄ ｉ ｎｇｓｏ ｆ  ｔ ｈｅ ２ ０ １ ３ Ｉ ＥＥＥ６ ｔ ｈＩ ｎｔ ｅｒｎａ ｔ ｉ ｏｎ ａ ｌＣｏ ｎ ｆｅ ｒ ｅｎ ｃｅｏ ｎ Ｓｏ ｆｔ ｗａ ｒｅ Ｔ ｅｓｔｉ ｎ ｇ ， Ｖｅ ｒ ｉｆｉ ｃａ ｔｉ ｏ ｎａ ｎ ｄＶａ ｌｉｄ ａ ｔｉｏｎＷ ｏ ｒ ｋｓｈ ｏｐ ｓ ．Ｌ ｕ ｘｅｍ ｂｏ ｕ ｒ ｇ ＊ ２ ０ １ ３ ： ４ ３－５ ２［２ ４ ］Ｙ ａｎｇ Ｚ ？ Ｈｕ Ｋ ， Ｍａ Ｄ ？  ｅｔ ａ ｌ ． Ｆｒｏｍ ＡＡＤＬ ｔｏ  ｔｉｍｅ ｄ ａ ｂ ｓ ｔｒａ ｃｔｓ ｔ ａ ｔ ｅ ｍａｃ ｈ ｉ ｎ ｅ ｓ ： Ａ ｖｅ ｒｉ ｆ ｉ ｅｄ ｍｏ ｄ ｅ ｌ ｔ ｒａｎ ｓｆ ｏ ｒｍａｔ ｉ ｏｎ． Ｊｏ ｕ ｒｎ ａｌ ｏ ｆＳｙ ｓ ｔ ｅｍｓ ａ ｎｄ Ｓｏｆ ｔ ｗａ ｒ ｅ， ２ ０ １ ４，  ９ ３ Ｃ ２ ） ： ４ ２ － ６ ８［ ２ ５ ］Ａｋ§ ｉ ｔＭ ，Ｂｅ ｒ ｇｍａ ｎｓＬ ，Ｖｕ ｒ ａ ｌＳ．Ａｎｏ ｂｊ ｅｃ ｔ－ ｏｒｉ ｅｎ ｔｅ ｄｌ ａ ｎｇｕ ａ ｇｅ－ ｄａ ｔａ ｂ ａ ｓｅ ｉ ｎ ｔ ｅｇｒ ａ ｔｉ ｏ ｎｍｏ ｄｅ ｌ： Ｔ ｈｅ ｃｏｍｐｏ ｓｉｔｉ ｏ ｎ－ｆｉｌ ｔ ｅ ｒｓａ ｐ ｐｒｏ ａｃ ｈ／ ／ Ｐｒｏ ｃｅｅｄ ｉ ｎ ｇｓｏ ｆｔ ｈｅ Ｅｕ ｒｏ ｐ ｅ ａｎ Ｃｏ ｎｆ ｅｒｅ ｎｃ ｅｏ ｎＯｂｊ ｅ ｃｔ－Ｏｒｉｅ ｎｔ ｅｄ  Ｐｒ ｏ ｇ ｒａ ｍｍｉｎｇ ．Ｂｅ ｒｌ ｉ ｎ，Ｇｅ ｒｍａｎｙ ， １ ９ ９２  ｊ ３ ７２ －３ ９ ５［ ２ ６ ］Ｎ ｉ ｅｒ ｓｔ ｒａｓ ｚＯ ， Ｍｅｉｊｌ ｅ ｒ ＴＤ ． Ｒ ｅｓ ｅａ ｒｃｈ ｄｉ ｒ ｅｃ ｔｉｏ ｎｓ ｉ ｎ ｓｏ ｆｔ ｗ ａ ｒｅｃｏｍｐ ｏ ｓｉｔｉｏ ｎ ．ＡＣ Ｍ Ｃｏｍｐ ｕ ｔ ｉ ｎｇ Ｓｕ ｒｖ ｅｙｓ ， １ ９９ ５ ， ２ ７ （ ２ ） ：  ２ ６２－２ ６ ４［２ ７］Ｌｉ ａ ｎｇＨ ｏ ｎｇｊｉ ｎ ， Ｆｅｎ ｇＸ ｉ ｎｙ ｕ ， ＦｕＭｉ ｎ ｇ．Ｒｅ ｌｙ－ｇ ｕ ａｒ ａｎｔ ｅｅ －ｂ ａ ｓｅｄ ｓ ｉｍｕ ｌ ａｔ ｉ ｏ ｎ ｆ ｏｒ ｃｏｍｐ ｏ ｓｉ ｔ ｉ ｏ ｎａ ｌ ｖ ｅ ｒｉ ｆ ｉｃ ａｔ ｉ ｏ ｎｏ ｆ ｃｏ ｎｃｕ ｒ ｒ ｅｎ ｔ张博林等：一种面向安全关键软件的１ １ 期 ＡＡＤＬ 模型 组 合验证方法 ２ １ ５ １ｐ ｒ ｏｇ ｒ ａｍ ｔ ｒ ａｎ ｓ ｆｏ ｒｍａ ｔｉ ｏ ｎ ｓ ．ＡＣＭＴｒ ａ ｎｓａ ｃｔｉ ｏｎ ｓｏ ｎ Ｐ ｒ ｏｇ ｒ ａｍｍｉ ｎ ｇＬ ａｎ ｇ ｕ ａｇ ｅｓ ＾＊ Ｓ ｙｓ ｔ ｅｍｓ ， ３ ６ （ １ ） ： １－ ５ ５［ ２ ８ ］Ｂ ｕ ｒ ｇ ｕ ｅ ｎ ｏ Ｌ ， Ｇ ｏ ｇｏｌ ｌ ａＭ． Ｆｏ ｒｍａ ｌ ｌ ｙ ｍｏ ｄｅ ｌ ｉ ｎ ｇ ，  ｅｘｅ ｃｕ ｔｉ ｎ ｇ ，  ａｎｄｔ ｅ ｓ ｔ ｉ ｎｇ ｓｅ ｒ ｖ ｉ ｃｅ － ｏ ｒｉ ｅｎ ｔ ｅｄ ｓｙ ｓ ｔｅ ｍｓｗ ｉ ｔ ｈＵＭＬａ ｎ ｄ ＯＣ Ｌ／／Ｐ ｒｏ ｃｅｅｄｉ ｎ ｇ ｓｏ ｆ ｔ ｈｅ Ｉ ｎｔ ｅｒ ｎ ａ ｔ ｉ ｏｎ ａ ｌ Ｃｏ ｎ ｆ ｅｒ ｅｎｃ ｅｏ ｎ Ｓｅｒ ｖｉｃ ｅ－ Ｏｒｉ ｅｎ ｔ ｅｄＣｏｍｐ ｕ ｔ ｉ ｎｇ ． Ｂｅ ｒ ｌ ｉ ｎ ， Ｇ ｅ ｒｍａ ｎ ｙ ， ２ ０ １ ７ ： １ １ ３－１ ２ ２［ ２ ９ ］Ｎ ｉ ｅ ｒ ｓ ｔ ｒ ａ ｓｚ０ ， ｅｔ ａ ｌ．Ａ ｃ ｏｍｐ ｏ ｎ ｅｎ ｔｍｏｄ ｅ ｌ  ｆｏ ｒ  ｆｉ ｅ ｌ ｄ ｄ ｅ ｖｉｃ ｅｓ ／ ／Ｐ ｒ ｏ ｃｅ ｅｄ ｉ ｎ ｇｓｏ ｆ ｔ ｈ ｅＩ ｎ ｔ ｅ ｒ ｎ ａｔｉ ｏ ｎ ａ ｌＷ ｏｒ ｋ ｉ ｎ ｇＣｏ ｎ ｆ ｅｒ ｅｎ ｃ ｅｏ ｎＣｏｍ ｐｏ ｎｅ ｎ ｔ Ｄｅ ｐ ｌ ｏ ｙｍ ｅｎ ｔ ． Ｂｅ ｒｌｉ ｎ ，Ｇ ｅ ｒｍａ ｎ ｙ ， ２０ ０ ２ ：２ ０ ０ －２ ０ ９［３ ０ ］ Ｌａ ｒｓｏ ｎ Ｂ  Ｒ ？ Ｃｈａ ｌｉ ｎＰ ．Ｈ ａｔ ｃｌ ｉ ｆｆ Ｊ ． ＢＬ ＥＳＳ： Ｆｏ ｒｍａ ｌ ｓｐ ｅｃｉ ｆ ｉｃａ ｔ ｉ ｏ ｎａ ｎ ｄ ｖ ｅｒｉｆｉｃａ ｔｉｏ ｎ ｏ ｆｂ ｅ ｈ ａｖｉｏ ｒ ｓｆｏ ｒ ｅｍ ｂｅｄ ｄ ｅｄ ｓｙ ｓｔｅｍ ｓｗｉｔ ｈ ｓｏ ｆｔ ｗａ ｒ ｅ／ ／ Ｎ ＡＳ ＡＦｏ ｒ ｍａ ｌ Ｍｅ ｔ ｈ ｏ ｄ ｓＳ ｙ ｍｐ ｏ ｓ ｉ ｕｍ ． Ｂｅ ｒ ｌ ｉ ｎ ． Ｇ ｅｒ ｍａ ｎ ｙ ，２ ０ １ ３ ： ２ ７ ６－ ２ ９ ０［３ １ ］ Ｍｕ ｒ ｕ ｇ ｅｓ ａｎ Ａ ， Ｗｈ ａ ｌ ｅ ｎ ＭＷ ． Ｒａ ｙ ａ ｄ ｕ ｒ ｇ ａ ｍＳ ， ｅ ｔ ａ ｌ ．Ｃｏｍ ｐｏ？ｓｉｔｉｏ ｎ ａｌ ｖ ｅ ｒ ｉｆｉｃ ａ ｔｉｏ ｎ ｏ ｆ ａ ｍｅｄｉｃ ａｌ  ｄ ｅｖｉｃ ｅｓｙ ｓｔ ｅｍ． ＡＣＭＳＩ Ｇ Ａｄ ａＡｄ ａ Ｌ ｅｔ ｔ ｅｒ ｓ ，２ ０ １ ３ ，  ３３ （ ３ ） ： ５ １－６ ４ＺＨＡＮ ＧＢｏ －Ｌｉ ｎ，Ｍ． Ｓ． Ｈｉ ｓ ｒｅ ｓｅ ａｒｃ ｈｉ ｎ ｔ ｅ ｒｅ ｓ ｔ ｓｉ ｎ ｃ ｌ ｕ ｄｅｆｏ ｒｍａ ｌｖ ｅ ｒｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ？ｓｏ ｆ ｔ ｗａ ｒ ｅ ｅ ｎｇ ｉ ｎ ｅ ｅ ｒ ｉ ｎｇ ．Ｙ ＡＮ ＧＺｈ ｉ－ Ｂ ｉ ｎ ，Ｐｈ ． Ｄ． ，ａｓ ｓ ｏ ｃｉ ａ ｔ ｅｐ ｒｏ ｆ ｅ ｓｓ ｏ ｒ．Ｈ ｉ ｓｒ ｅｓ ｅ ａ ｒ ｃｈ ｉ ｎ ｔ ｅ ｒ ｅ ｓ ｔ ｓｉｎ ｃ ｌ ｕ ｄｅ ｓ ａ ｆ ｅ ｔ ｙ－ ｃ ｒｉ ｔ ｉ ｃ ａ ｌｓ ｏ ｆ ｔ ｗａ ｒ ｅ，ｆ ｏ ｒｍａ ｌｖｅ ｒ ｉ ｆ ｉ ｃ ａ ｔ ｉ ｏｎ．ＺＨＯ Ｕ Ｙｏ ｎｇ ．Ｐ ｈ． Ｄ． ， ａ ｓｓ ｏｃ ｉ ａ ｔ ｅ ｐ ｒｏｆ ｅ ｓ ｓ ｏｒ ．Ｈｉ ｓ  ｒｅ ｓ ｅ ａ ｒｃ ｈｉ ｎｔ ｅ ｒｅ ｓ ｔ ｓ ｉ ｎ ｃｌ ｕ ｄ ｅ ｓ ｏｆ ｔ ｗ ａ ｒ ｅ ｅ ｎ ｇｉ ｎｅ ｅ ｒ ｉ ｎｇ ， ｆｏ ｒ ｍａｌ ｍｅ ｔ ｈ ｏｄ ｓ．ＭＡ Ｙ ａ ｎ－ Ｙ ａ ｎ ．Ｍ ． Ｓ ．Ｈｅ ｒ ｒｅ ｓ ｅ ａ ｒ ｃ ｈ ｉ ｎ ｔ ｅ ｒ ｅｓ ｔ ｓ ｉ ｎ ｃｌ ｕ ｄ ｅｆｏ ｒｍａｌ ｖ ｅ ｒ ｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ，ｓ ｏｆ ｔ ｗ ａ ｒｅ ｅ ｎｇ ｉ ｎｅ ｅ ｒ ｉ ｎ ｇ．ＨＵＡＮ Ｇ Ｚｈ ｉ－Ｑ ｉ ｕ， Ｐｈ ． Ｄ． ， ｐ ｒｏｆ ｅｓ ｓｏ ｒ．Ｈ ｉ ｓｒ ｅｓ ｅａ ｒｃ ｈｉ ｎ ｔ ｅｒｅ ｓｔ ｓｉ ｎｃｌ ｕ ｄｅ ｓ ｏ ｆｔ ｗａ ｒｅ ｅ ｎ ｇ ｉ ｎ ｅｅ ｒ ｉ ｎｇ ，ｆｏ ｒｍ ａ ｌ ｍｅ ｔ ｈ ｏｄ ｓ ．ＸＵＥＬｅ ｉ ， Ｍ ． Ｓ．？ ｓ ｅｎ ｉ ｏｒ ｅｎｇ ｉ ｎｅ ｅ ｒ． Ｈ ｉ ｓ ｒｅ ｓ ｅ ａ ｒｃ ｈ ｉ ｎ ｔ ｅｒ ｅｓ ｔ ｓｉ ｎｃ ｌ ｕ ｄｅ  ｅｍ ｂ ｅ ｄ ｄｅ ｄｓ ｏｆ ｔ ｗａ ｒ ｅ ｖｅ ｒｉ ｆ ｉ ｃａ ｔ ｉ ｏｎ，ｅｍｂ ｅｄ ｄ ｅｄｓ ｏ ｆ ｔ ｗａ ｒ ｅｓｙ ｓｔ ｅｍ ｄ ｅ ｓ ｉ ｇ ｎ．Ｂ ａ ｃｋ ｇｒｏ ｕ ｎ ｄＴｈ ｅ  ｆ ｏｒｍａ ｌ ｖｅ ｒｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ｏｆ  ｔ ｈｅ Ａ Ａ ＤＬ ｍｏ ｄｅ ｌ ｏ ｆ ｃ ｏｍ ｐｌ ｅｘｓ ａ ｆ ｅ ｔ ｙ－ｃ ｒ ｉ ｔ ｉ ｃ ａｌ  ｓｏｆ ｔ ｗａ ｒｅ ｉ ｓ ｖｅｒ ｙｃ ｈａｌ ｌｅ ｎｇ ｉ ｎｇ． Ｅ ｘｉ ｓｔ ｉ ｎｇｖ ｅｒｉ ｆｉ ｃ ａ ｔ ｉｏ ｎｍｅ ｔ ｈ ｏｄ ｓ ｏｆ ｔ ｅ ｎ ｄｉ ｒｅ ｃ ｔｌ ｙ ｖｅ ｒ ｉ ｆ ｙｔ ｈ ｅ“ｆ ｌａ ｔ ｔ ｅ ｎ ｉ ｎ ｇ” ｅ ｎ ｔｉ ｒｅ ｍｏ ｄｅｌ．Ｉ ｎ ｔ ｈ ｉ ｓｗ ａ ｙ ，ｔ ｈ ｅ  ｖｅ ｒｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ｏ ｆ ｃ ｏｍｐ ｌ ｅ ｘｓ ｙ ｓｔ ｅｍ ｓ ｏｆ ｔ ｅ ｎ ｆ ａ ｃｅ ｓｔ ｈ ｅ ｐ ｒ ｏ ｂｌ ｅｍ ｏ ｆ ｓ ｔ ａ ｔ ｅ ｓ ｐａ ｃ ｅ  ｅ ｘｐ ｌ ｏ ｓ ｉ ｏｎ ．Ｂａ ｓ ｅ ｄｏ ｎｔ ｈ ｅ ｅ ｘ ｉ ｓ ｔ ｉ ｎｇｒ ｅｓ ｅ ａ ｒｃ ｈ ｗｏ ｒｋ ，ｔ ｈｉ ｓｐａ ｐ ｅ ｒ ｐｒｏｐｏ ｓｅ ｓ ａ  ｃ ｏｍｐｏｓ ｉ ｔ ｉ ｏ ｎａ ｌ ｖｅ ｒ ｉ ｆ ｉ ｃａ ｔ ｉ ｏ ｎｍｅ ｔ ｈ ｏｄ ，ｗｈ ｉ ｃ ｈｃ ｏ ｍｂｉ ｎｅ ｓ ｔ ｈ ｅｃ ｏｍｐｏｓ ｉ ｔ ｉ ｏｎ ａ ｌ ｖｅ ｒ ｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ｏ ｆ ｔ ｈｅＡＡＤＬａ ｒｃ ｈｉ ｔｅ ｃｔ ｕｒｅｍｏ ｄｅ ｌ ａ ｎｄｔ ｈ ｅｆ ｕｎｃ ｔ ｉ ｏｎａ ｌ ｂ ｅｈａ ｖ ｉｏ ｒｖ ｅｒｉ ｆ ｉｃ ａ ｔ ｉ ｏｎｏ ｆＵＰ ＰＡ ＡＬ－ ｂａ ｓ ｅ ｄｌｅａ ｆｃ ｏｍｐｏｎ ｅ ｎｔ ｓ．Ｔｈ ｉ ｓｃ ｏｍｐ ｏｓ ｉ ｔ ｉ ｏｎ ａｌｖ ｅ ｒｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎｍｅ ｔ ｈ ｏｄ ｎｏ ｔ ｏｎ ｌ ｙｒｅ ｄ ｕｃ ｅ ｓ ｔ ｈｅ  ｐｒｏ ｂ ｌｅｍｏｆ ｓｔ ａ ｔ ｅｓｐａｃ ｅ ｅ ｘｐ ｌｏｓ ｉ ｏ ｎ， ｂ ｕ ｔ ａ ｌｓ ｏｖ ｅｒ ｉ ｆ ｉ ｅ ｓｔ ｈ ｅｃ ｏｒ ｒ ｅ ｃｔ ｎ ｅ ｓｓ ｏｆ ｔ ｈｅ ｓ ｙｓ ｔ ｅｍａ ｒ ｃ ｈｉ ｔ ｅ ｃｔ ｕ ｒ ｅ ａ ｎｄ ｔ ｈ ｅ ｆ ｕ ｎ ｃ ｔｉ ｏ ｎａ ｌｂ ｅ ｈａ ｖ ｉ ｏ ｒｏ ｆ ｔ ｈ ｅｕ ｎｄ ｅ ｒｌ ｙｉ ｎｇｃ ｏｍｐ ｏ ｎｅ ｎ ｔ ｓ ，ａ ｎｄｃｏ ｍｐ ｌｅ ｔ ｅ ｓ ｔ ｈｅ ｖ ｅ ｒ ｉ ｆｉ ｃ ａ ｔ ｉｏ ｎｏ ｆ ｔ ｈ ｅｅ ｎ ｔ ｉ ｒ ｅｃ ｏｍｐ ｌｅ ｘＡ Ａ ＤＬｍｏ ｄ ｅ ｌ ．Ｔ ｈｅ ｒｅ ｓｅ ａ ｒｃ ｈｉ ｎｔ ｈ ｅｐａ ｐｅ ｒ ｉ ｓ ａ ｐａ ｒ ｔｏ ｆ ｔ ｈ ｅＮ ａ ｔ ｉ ｏ ｎａ ｌＮ ａ ｔ ｕ ｒ ａ ｌＳ ｃ ｉ ｅ ｎ ｃ ｅＦ ｏ ｕ ｎｄ ａ ｔ ｉ ｏ ｎｏ ｆＣ ｈ ｉ ｎａ（６ １ ５ ０２ ２ ３ １  ） ，ｔ ｈ ｅＮａ ｔ ｉ ｏ ｎ ａ ｌ Ｋｅ ｙＲ ｅ ｓ ｅａ ｒｃ ｈａ ｎｄＤｅ ｖ ｅ ｌｏｐ ｍｅ ｎ ｔＰ ｒｏ ｇ ｒ ａｍｏ ｆ Ｃ ｈ ｉ ｎ ａ（ ２ ０ １ ６ ＹＦ Ｂ １ ０ ０ ０ ８ ０ ２ ） ，ｔ ｈ ｅＮ ａ ｔ ｉ ｏ ｎａ ｌＤｅ ｆ ｅ ｎｓ ｅ Ｂａ ｓ ｉ ｃ Ｓｃｉ ｅ ｎｔ ｉ ｆ ｉ ｃＲ ｅ ｓｅ ａ ｒ ｃ ｈＰ ｒ ｏｊ ｅ ｃ ｔ（ Ｊ Ｃ ＫＹ ２ ０ １ ６ ２ ０ ３ Ｂ０ １ １ ） ，ｔ ｈ ｅ Ａ ｖ ｉ ａ ｔ ｉ ｏ ｎ Ｓ ｃ ｉ ｅ ｎｃ ｅＦ ｕ ｎｄ ｏｆ Ｃ ｈ ｉ ｎ ａ（ ２ ０ １ ９ １ ９ ０ ５ ２ ００ ２ ） ， ａ ｎｄｔ ｈ ｅＦ ｏ ｕ ｎ ｄ ａ ｔ ｉ ｏｎｏ ｆＧ ｒａ ｄ ｕ ａ ｔ ｅ Ｉ ｎｎ ｏｖ ａ ｔ ｉ ｏ ｎＣ ｅ ｎｔ ｅ ｒ ｉ ｎ Ｎ ＵＡ Ａ（ Ｋ ＦＪＪ ２ ０ １ ８ １ ６ ０ ３ ） ．