基于ASK―CTL的集成体系结构一致性综合检验方法

摘要：针对集成体系结构静态产品模型与动态可执行模型的一致性问题，本文提出一种基于ASK-CTL与ML语言相结合的综合检验方法。通过集成体系结构可执行模型状态空间进行集成系统重点关注静态性质、动态行为的综合检验，完成集成体系结构一致性确认，并且能通过检验诊断找出失败原因以完成体系结构模型修订。论文最后以预警系统为例，对该方法进行了验证。

关键词：一致性检验 ASK-CTL CPN ML语言

中图分类号：TP302 文献标识码：A 文章编号：1007-9416（2015）12-0000-00

1 引言

集成体系结构一致性检验的目的是保证体系结构产品模型与可执行模型仿真分析结果的描述统一、功能一致和真实。集成体系结构一致性检验成为近年人们关注的研究议题，并且已经展开了一些研究。如文献[1]提出了基于可执行模型状态图的检验方法，文献[2][3][4]提出了对模型规则的检验方法，文献[5]提出了基于触发序列的检验方法等。但是这些研究大多集中于模型的某个特定方面，没有考虑到模型的结构性质和设计开发者所重点关注的系统行为性质的综合检验。另外，现有研究结果都没有给出检验失败情况下的解决办法，没有给出如何寻找模型出错路径及错误发生环节的指导。本文提出了一种基于时态逻辑ASK-CTL与ML（Meta Language）相结合的系统状态空间检验诊断方法，对模型系统重点关注的行为性质，如：作战规则、流程、并发冲突关系及模型结构性质，如：活性、家性、守衡性等各方面进行综合验证。针对检验失败的情况，结合模型检测和诊断技术，提出了一种故障诊断方法，帮助设计者找出错误发生的环节及出错路径以便对模型进行修正，防止危险状态出现。最后以预警系统为案例对该方法步骤进行了简单阐述。

2 体系结构检验方法

国防部体系结构框架（DoDAF： Department of Defense Architecture Framework）提供了集成系统体系结构设计的一般指导和设计产品的描述标准。DoDAF采用视图的产品（Products）来规范集成体系结构设计[6]，并规定国防系统需要采用相关视图产品来完成系统体系结构构设计。DoDAF体系结构产品为系统的静态表述，为了更好的反映系统的动态行为和特征，需要根据这些静态产品来构建可执行模型来演示体系结构的动态行为和性能特征。

着色Petri网（CPN：Colored Petri Nets）由丹麦奥尔胡斯大学Kurt Jensen教授提出的一种高级Petri网。它引入标准结构化元语言（SML）、着色令牌和层次建模技术，有效地解决了普通Petri网（OPN）的“维数灾”问题，是系统建模和分析的常用工具[7]。ASK-CTL是丹麦Cheng， A.， Christensen， S， and Mortensen， K.H.提出的一种基于CTL拓展的分支时间逻辑，ASK-CTL植于CPN建模工具CPN-TOOLs内部，无需借助于其它检测工具，就可直接对集成体系结构设计可执行（CPN）模型进行基于状态空间的一致性检验[8]。

采用ASK-CTL和ML语言相结合的形式，把所关注的DoDAF体系结构模型系统动态性质，如作战规则、流程、并发冲突关系等逐一表示成CPN-TOOLs内嵌分支时序逻辑ASK-CTL能接受的命题公式，例如：DoDAF的规则模型OV-6a中的规则及体系结构关注的行为特性如“A事件最终会发生”等。然后，通过对可执行（CPN）模型仿真和状态空间搜索来对公式进行检验，确保集成体系结构产品模型与可执行（CPN）模型的动态一致性。需要说明的是，系统动态一致性常考察的是系统的行为特性。而有些与网结构有关的动态行为性质，如守衡性（S不变量）、可循环性（T不变量）和局部守恒性等，则既是静态特性也是系统的动态特性。

基于DoDAF体系结构可执行模型的状态空间的一致性检验的具体方法和步骤如图1所示。

图1所示步骤中，如果出现检验失败的情况，则需要找出模型的错误环节及出错路径，以便设计开发人员对模型进行修正。结合ML语言和ASK-CTL逻辑，诊断步骤如表1所示。

CPN可执行模型修正完毕后，需重新开始对模型进行检验，如此循环，直至所有性质均检验通过为止。

此外，利用CPN可执行模型状态空间产生的发生图（Occurrence Graphs）、信息流图（Message Sequence Chart）与DoDAF体系结构产品模型的作战事件跟踪描述（OV-6c）进行比对检验，从而构成基于状态空间的DoDAF体系结构产品与CPN可执行模型一致性的综合检验途径。

3 案例分析

依据DoDAF标准进行系统体系结构设计的方法建立预警系统体系结构模型。依据DoDAF模型到CPN可执行模型转化方法，建立预警系统CPN可执行模型。模型首页如图2所示，其中库所Target表示来袭目标，替代变迁Search表示搜索目标功能，Detect表示测量目标功能，Comm表示数据传送功能，Data Processing表示数据处理功能，它们的具体功能由对应的子页模型实现，与DoDAF静态模型相对应。

图3所示模型为图1中替代变迁Data Processing的子页，主要进行威胁判定（变迁Picture Processing）、参数匹配（变迁Data Matching）、参数调整（变迁Modifed）、生成报告（变迁Synthetize）等功能。

按照上一节所述的步骤与方法对已经建立的CPN可执行模型进行验证。计算状态空间并导入ASK-CTL后，将我们所关注的性质写成ASK-CTL能接受的命题公式。

模型结构性质如变迁Synthetize具有活性：

fun IsConsideredBE a = st_TI（ ArcToTI a）） ="Data_Processing’Synthetize 1"；

val myASKCTLformula1 =INV（POS（MODAL（AF（"_"，IsConsideredBE））））；

静态性质如“如果连续扫描4次中有2次发现目标，则确认目标存在”：

fun Searchtimes n=ms_to_col（Mark.Search'Search_times 1 n）=4；

fun Foundtimes n=（#2 （ms_to_col（Mark.Search'Count 1 n）））>=2；

fun Foundtarget n=Mark.Searcht'Foundtarget 1 n[]；

val myASKCTLformula2 =POS（AND（POS（NF（"_"，Foundtarget）），

AND（NF（"_"，Searchtimes），NF（"_"，Foundtimes））））；

DoDAF模型作战状态转移序列OV-6b表征的动态行为验证如下：

val myASKCTLformula3=POS（AND（AND（POS（AF（"_"，Comm）），POS（AF（"_"，Alarm））），

AND（POS（AF （"_"， Synth）），AND（AND（POS（AF（"_"，Photo）），POS（AF（"_"，Infrared））），

AND（AF（"_"，Fire），POS（MODAL（NF（"_"，Foundtarget））））））））；

并发的行为“Take_Picture”和“Infrared Detect”可用如下公式表示：

fun Photo a=st_TI（ArcToTI（a））="Detect'Take_Picture 1"；

fun Infrared a=st_TI（ArcToTI（a））="Detect'Infrared_Detect 1"；

val T1=POS（AND（MODAL（AF（"_"，Infrared）），POS（MODAL（AF（"_"，Photo）））））；

val T2=POS（AND（MODAL（AF（"_"，Photo）），POS（MODAL（AF（"_"，Infrared）））））；

val myASKCTLformula4 =POS（AND（T1，T2））；

将所有性质都写为ASK-CTL命题公式后，对公式进行检验。如选取性质“连续扫描4次中有2次发现目标，则确认目标存在”写成的公式myASKCTLformula2进行检验，结果为“true”，表示检验通过，可以进行下一性质的检验。如果检验失败，则停止检验，利用上一节提出的模型诊断方法进行如下故障诊断。

fun Error n= let val X=ms_to_col （Mark.Searcht'Foundtarget 1 n）； in X="found target"； end；

val Errornodes =PredAllNodes （fn n => not （Error n））；

Int.min （List.hd Errornodes） （List.tl Errornodes）；

通过上述公式可快速定位至引起发现失败的动作变迁，以便设计者对模型进行相应修改，也便于对系统性能的分析。

4 结语

本文提出一种基于ASK-CTL与ML语言相结合的综合检验方法。采用ASK-CTL和ML语言相结合的形式，把所关注的DoDAF体系结构模型系统静态性质和动态行为如作战规则、流程、并发冲突关系等逐一表示成CPN-TOOLs内嵌分支时序逻辑ASK-CTL能接受的命题公式，通过对可执行（CPN）模型状态空间搜索，确保集成体系结构产品模型与可执行（CPN）模型的一致性。对模型检验失败情况提出了一种故障诊断方法，无需借助其它模型工具，即可快速找出模型故障原因，方便模型修正。并以预警系统为案例进行了说明。在本文基础上，从CPN可执行模型的结构性质分析（如关联矩阵，S、T不变量等）方面及发生图、信息流图方面深入检验与DoDAF体系结构产品模型及实际物理系统的一致性问题，有待进一步研究。

参考文献

[1]Wagenhals L.W.， Shin， I， Kim， D and Levis， A.H. C4ISR Architectures II ： Structured Analysis Approach for Architecture Design[J]. Systems Engineering， 2000， 3（4）： 248-287.

[2]Zaidi， A.K.， and Levis， A.H. Verification of System Architectures Using Modal Logics and Formal Model Checking Techniques[C]//Conference on Systems Engineering Research （CSER）， Los Angeles， CA， April 2006.

[3]Zaidi， A.K. Levis， A.H. Computational Verification of System Architectures[C]//Computational Intelligence in Security and Defense Applications（CISDA）， April 2007.

[4]姜军，罗雪山，罗爱民 等.可执行体系结构研究[J].国防科技大学学报，2008，30（3）：76～80.

[5]赵弘，蒋晓原，王春峰.CPN仿真的C4ISR体系结构验证评估[J].火力与指挥控制，2008， 33（9）：4～10.

[6]DoD Architecture Framework Working Group. DoD Architecture Framework Version 1.5， Volume I and II[M]. The United States： Department of Defense， 2007.

[7]Jensen， K.， Colored Petri Nets： Modeling and Validation of Concurrent Systems. Monographs in Theoretical Computer Science[M]， Springer-Verlag， 2009.

[8]Cheng， A.， Christensen， S， and Mortensen， K.H. Model Checking Colored Petri Nets Exploiting Strongly Connected Components[C]// In Proc. of the International Workshop on Discrete Event Systems， UK： Institution of Electrical Engineers， 1996： 169-177.