摘 要：容错和控制系统的安全性验证是自发机扑系统成功的关键，一种叫做任务数据系统MDS (Mission Data Symstem)的控制框架的软件理论被提了出来，而它的产生则推动了一种基于对象的控制方法的产生。本文将讨论一种设计方法，该方法的设计目的是将对象网络控制程序转化为线性混合系统。该线性混合系统在使用信号模拟检测器进行检测时，在出现错误时是可以证明其安全性的。本文将结合例子介绍这种方法。
    关键词：安全性验证；机扑系统；MDS；模式检测器

    天然形成的自发机扑系统有着复杂的控制系统。总的来说，为这些系统设置的错误提供必要的检测、隔离、恢复软件是复杂的，同时在模拟时会遇到一些出错。在自发机扑系统中，需要一种系统地包含容错功能的方法。一种实现的方式是产生一种当出现错误时能够自行重新配置的可变的控制系统。不过，假如该控制系统不能被证明是安全的，那么重新配置所产生的附加复杂性可能降低系统容错能力的有效性。
    对模拟信号容错控制系统来说，一种特别有用的方法是混合系统。关于混合系统的控制业界已经付出了很多的努力，当系统的联系动力已经是足够简单时，就可以验证混合系统的运行不会进入不安全的状态。有些软件可以用于分析，包括HyTech、UPPAAL和VERITI。这都是信号模拟检测器。本文所使用的检测器是HyTech中一种叫做PHAVer的检测器。通常为容错混合控制系统所做的安全验证，确保了当一定的错误产生时,不会使系统进入一种不安全的状态。控制系统必须通过一些合适的方式转化为一种可接受的形式。一种这样的工具是为了智能代理的转化而产生，是叫做AgentSpeak的指向目标的控制语言，其包含两种模式转化器。另一种流行的方式是从Buchi自动机对无限的字符使用设计控制程序进行更正。
    本文控制程序的软件控制框架是基于任务数据系统(MDS)开发的。而MDS又是基于叫做状态分析器的系统工程概念产生的。MDS能够在连续衍生状态中严格地认定有着分段恒定幅度的线性混合系统，同时能够任意地处理大量的数据。使用MDS的系统被对象网络所控制，该对象网络在超时的时候直接对物理状态表示约束的目的。本文将讨论一个由对象网络向线性混合系统自动转化的过程。
1 背景信息
1.1 状态分析和任务数据系统(MDS)
    状态分析是一种引擎方法论，该方法论的设计集中于一种基于当前状态的系统设计方法。被控制系统中状态效果的模式被用于状态变量、系统控制、计划和目的日程的评估。状态变量是系统状态或被控制或处于控制状态属性的代称。状态变量的例子可能包括机器人的位置坐标、环境的温度、感应器的稳定性、转换器的位置。
    对象和对象描述产生于模式。对象处于一种目的的特殊语句中，该目的用来控制约束状态变量的系统。基于对象类型、规则、目的的父对象可以详细描述子对象。状态分析的核心概念在于被用于设计控制系统的语言应该与使用该控制系统的语言一致。因此，这种MDS软件构架应该与状态分析紧密相关。
    一个叫做软件状态变量的数据结构是MDS的中心。一个状态变量可以控制许多信息。例如，在飞机自动机中的位置状态变量可以控制自动机的位置坐标(x，y)、组件形式中的速度、每条信息中的不确认值。每个状态变量的速度，但是却会使位置和不确定值无法得到控制。
    对象网络代替命令串成为系统的控制输入。一个对象网络由含有互相联系的开始结束时间点的对象和暂存约束组成。一个对象的暂存约束可能基于执行时间或者对象的完整性。对象可以引发由同样性质的或者其他偶然相关的状态变量所描述的约束的产生。在对象网络或对象的定义中，对象通过对象调度软件来进行调度，保证运行时没有冲突发生。然后每个被调度的对象将被寄存器或状态变量控制器所接收。
    定义表使MDS比基于命令行的控制体系能更灵活处理事物。一个例子如容错，如果系统中存在物理冗余性，对错误对象的重定义有许多的处理方式。比如：有许多方式同样能够完成这项工作，或者为这项工作降低操作模式强度，对象的定义类可能会包含许多预定义策略。这些策略能通过不同的方式完成对象目的；而且它们可能被基于语法定义逻辑条件的描述器所选择。这些能力使许多普通错误类型能自动地被控制系统所包容。
1.2 线性混合自动机
    有一些可用的抽象模式检测器能够验证线性混合自动机。一个线性自动机由下面的组件组成：(1) 一个完整有序并包含连续状态变量的表，x={X1, X2,…Xn}及它们相对应的导出表y={Y1, Y2, …Yn}。(2) 一个有向图(V, E)，V是系统控制模式或存储空间的集合，E是在不同系统模式之间控制边的集合。(3) 每个存储空间的非变量集合inv(v)，初始条件集合init(v)，以及可变条件集合。在这些集合中v∈V。(4) 连接符号∑和连接操作A的集合。(5) 同步符号S的集合。以上组件完整地描述了一个可以使用PHAVer检测器成功验证的线性混合系统。在该混合自动机的安全验证中使用的可达性分析法可以得出在一个有效回合里所以连接到一个确定状态的所有状态的集合。这可能引起该状态空间巨大的溢出。PHAVer可以通过两种方法处理该问题：(1) 通过把存储空间分为简单部分。(2) 使用存储空间集合的过度近似值来限制系统的复杂性及加速聚合并促使过程停止。在分析中过度近似值并没有要求，因为安全存在着严格的保证。
1.3 对象网络转换和验证过程
    混合系统分析工具可以被用来验证一个混合系统的安全行为，因此，对对象网络验证来说，一个由对象网络向混合系统转化的过程是对象网络验证的重要工具。转化对象网络的人工操作过程在图1的转换图中可以表示出来。这些对象网络由一些状态变量和对象描述层，不过时间点必须加以严格控制，这意味着时间点在命令处于描述区的表中时开始计时。

    对象网络中每一个状态变量可被定义为可控制的、不可控制的或独立的。一个可控状态变量（简称CSV）直接地与一个命令类连接起来；一个不可控状态变量(简称USV)无论如何都不与一个命令类发生联系；一个独立状态变量(简称DSV)至少在一个可控状态变量处有模块独立性。不同的混合自动元产生于这些不同状态变量的对象。
    一个关于CSVs和DSVs的对象转化过程的概述要点如下：
    (1)在CSV和连续DSV上，分别为每个描述约束的对象建立描述和转换逻辑表。
    (2)向组中的连续点之间放置对象。
    (3)在每个组中，通过连续叶对象和所有的父对象和约束CSVs的兄弟对象的方式产生存储空间（模式）。为所有CSVs和约束在存储单位中连续的DSVs设置标签，标签包括每一个有着动态更新方程的存储空间。
    (4)使用以上的描述和过度逻辑表在存储单位和组之间产生以下转换：①面向组的描述逻辑控制的转换。②组内存储单位间错误的转换。③逻辑转换控制一个组向下个组或者下个存储空间的转换。
    (5)增加基于时间的出口和失败转换，转换为包含时间约束对象的存储空间。当转换为连接组接口的存储空间时，增加入口行为即重置时间变量为零。
    (6)移除不必要的位置、组和转化。
    对每个USV来说，一个独立的混合自动机的形式源于来自于离散状态或离散变量状态集合的存储空间的产生。转换条件是或然率或基于状态模式。对安全验证来说，混合自动机被转化为PHAVer代码而且合适的转化在自动机之间同步。不安全的集合被确认而且条件将使混合自动机进入不安全集合，这样使用验证软件的条件就符合了。假如没有这样的条件符合，那么对象网络就得以验证。
2 转换软件设计
    对象网络转化过程的软件版本不象早先提出的软件版本那么复杂。但是大部分的重要能力都已经包括在内了。为了适应表结构显示与它的相应模式功能库的要求，该软件是以数学方式写的。
2.1 软件的输入
    转化软件的输入产生于一个可用对象网络的必要设计组件。5个条件表(goals、usv、merge、elab、trans)是初始条件。在对象网络中，对象表是一个关于所有可控制和独立状态变量的表。这些对象由父对象控制，没有任何对象可以先于父对象出现。对象描述是一个由上到下的过程，因而对对象控制的约束是应该获得的基本条件。每一个对象入口都必须包含如下信息：
    (1)对象数。这是为父约束设定的。
    (2)时间表{Ts,Te}。该子表有两个元素，开始时间点数和结束时间点数。这两个时间点在指令控制下进行计数，且Ts=Te总为真。
    (3)父对象数。假如对象没有祖先时总为0。
    (4)策略数。假如对象没有父对象时为0。
    (5)约束表{Sv,type,{C₁,…Cn}}。该子表的第一个元素是独立可控制的状态变量数字字符（可控制的状态变量集是强制定义的），即C₁～Cn都是type制定类型的。状态变量约束类型的数目，定义的约束类型在对象网络中定义的所有不可控制变量组成了USV表。这些不可控制状态表的命令都是强制型的。
    每一个USV入口必须有如下信息:
    (1)状态变量名。在所有描述和错误逻辑中使用的符号。这些符号对每一个不可控制状态变量是独一无二的。
    (2)离散数值表{V₁,…V_m}。该子表包含m离散数值或者未被控制的状态变量数值集合。m的数值可以是数字或者是字符串，对特定的USV是唯一的，但不是对所有的USV都是唯一的。
    (3)转换表。{{{c,Vi},…},…,{{c,Vj},…}}。该表有m子表，每一个USV都含有一个离散数值。每一个子表中，都含有可以从状态值中引出的转换所组成的集合表。这些表中的第一个元素指转换条件，第二个元素指转换的结果。
    融合表有一些子表，在数字命令中每一个子表都包含一个可控制和相关状态变量。这些子表包含了两部分：
    (1)描述可被代替的对象约束类型。
    (2)假如两个或更多同种状态变量的约束同时活跃的话，这些约束类型是如何相互融合的。在这些子表中，还有一些关于自身融合和与比该约束数值大的约束融合的约束表。
    这部分的表包括以下内容：
    (1)融合类型。假如在约束中融合是有条件的，该值为-1。假如融合是不可能发生的，值为0，而且此时没有更多的表元素。假如融合始终可能，该值为融合约束类型的数值。
    (2)融合约束规则。这是指融合过程中，被实际约束值替代的和抽象化的规则。这可能是融合时最后入口。
    (3)融合类型。仅仅对条件融合来说，约束类型的数目就是融合产生的结果。
    在目的表中，描述表为每个对象设立了一个子表。假如对象为父对象时，每个子表为不同的逻辑类型和条件单独列表；若不是，为目的建立的子表就为空。这些详细描述逻辑信息类型列表如下：
    (1)“开始”逻辑。这种策略包括产生优势策略的详尽描述的各种条件。
    (2)“失败”逻辑。这种策略表包括策略失败和为了某种对象设定的策略失败的条件。这时可能每一个策略不止一个条件，集和对象。该策略可能无法转向安全状态。同时，一个失败的条件可能是标有的“CGE”子对象的失败的原因。
    每一个包含可控制和独立的状态变量的转化表都有一个子表，子表中的表所以的条件在每一个含有可控制或独立的状态变量的约束类型中心必须为真，这些条件包含如下两部分：
    (1)输入转换逻辑。这个条件在输入约束类型的时候必须为真。
    (2)输出转换逻辑。这个条件表明了一种约束类型的完整性。
2.2 软件输出
    自从所有的USV自动机必要信息（除流以外）被输入到软件中，软件就只有关于CSV/DSV目的自动机的信息了。这种叫做cdsva的结构包括许多部分，开始被编入组然后编入区。在每个区表中，可以依次列出下列信息。
    (1)已存在的对象表。表中内容为对象数据。
    (2)融合约束表。包括CSV和DSV数据，融合约束类型和约束值。
    (3)开始转化条件。只有当条件已知时，转化来自已存在组和当前组之间的组连接器。
    输入和输出的转化条件---这些转化是从已存在的组连接器向存储空间的转化以及从存储空间分别向后继组连接器的转化。条件则包括被约束于该空间的CSVs和DSVs。
    (4)输出错误转换。包括列出的条件和可接受存储空间。可能每个位置不只一个输出。
    (5)输出错误条件。条件和初始存储空间都已列出。可能每个空间不只一个输出。
2.3 转换算法
    在图2中显示了转换软件总的流程图。在该图中，转换算法包括4个主要部分：存储单元的产生、约束融合、转换的产生和存储单元的释放。以下对这4个部分进行分别描述。

    存储单元产生算法将对象输入结构，同时使用时间点、父对象和策略信息将对象分配进不同的组，然后分配进不同的存储单元。由时间点信息首先开始这个过程。假如Te>Ts+1时，一些对象可以在不止一个组中产生。然后，父信息和策略信息将被用来在这个组中对每个对象查找它们所有的不相容对象。在不同的策略中，这些不相容对象不能像对象一样在同样的存储单元中产生，是由于它们或者是写入同样的父对象，或者是来自同样的父对象的对象所遗传。然后，每一组分支对象都被找到而且都在存储单元中产生；兄弟分支对象也合并入该位置。分支对象在这个组中没有孩子，兄弟对象是写入相同策略的对象或是在该组中没有祖先的根对象（即与兄弟对象没有共同的祖先），双亲对象和它们的兄弟在根对象到达时才被添加到每个存储单元。每个存储单元被其他可相容的单元联合。当没有更多的单元可供融合时，多余的位置就被移除。可融合的位置一般共享到更多的位置，而且没有一个存储单元的对象是在其他单元的对象的不可相容对象表中的。这些步骤确保了每一个在两个时间点之间的对象网络执行过程能够明确地在一个位置被代表。
    约束融合算法使用寄存单元产生算法，对象和约束融合输入将在每个存储空间中所有的可控和独立的状态变量合并产生约束。对同一状态变量的约束对象类型进行对比可以发现融合输入的合适区域。然后符号的融合条件和融合约束值被对象输入中的实际约束所代替。如果融合是成功的，新的融合类型和融合约束被增加到该存储空间。如果融合不成功，该空间将被释放。
    转换产生算法产生三种转换：(1)由之前接入每个组的存储空间的组连接器的转换；(2)在一个组中存储空间之间的失败转换；(3)从一个存储空间向下一个组连接器的转换（该连接器使用对象、elab、trans、usv和融合约束算法输出部分作为输入）。在每个存储单元中，某一对象的“开始”逻辑通过“与”运算简化后检查是否为真。如果逻辑结果表达式为假，那么该转换被抛弃。存储空间中基于结束类型的所有的约束状态变量的转换逻辑也是经过运算并简化。在每个存储单元中，每个对象的错误逻辑将会被列举出来，同时在同一存储空间中的失败转化也会通过“或”运算进行运算并简化。将要接受失败转化的存储空间将被更新并反映这一事实。一个未被简化的cdsva结构是这一算法部分的输出。
    存储单元释放算法检查一些保证存储单元或每一个存储单元组的释放的条件，并在条件为真时释放存储单元，这些条件包括：(1)输入条件的缺失；(2)一个总为真的失败条件；(3)存储空间的释放包括所有其他原因该存储空间及替代被删除空间的重新赋值的新存储空间的错误条件的释放；(4)出口条件是所有的输入转化条件的子集。算法的输出cdsva表是软件的最终输出。
3 举例
    一个已知的正方形房子被分为4个区域（如图3），一个机器人在该房子中寻找目标，它可能在或区中，假如机器人在某区中找到了，那么它就将停在那里;否则它将继续寻找。被用来解决该问题的一段对象网络和混合自动机软件结构如图4所示。该软件的输入由10个对象，一个可控状态变量，包含两个约束类型（驱动和停留）的坐标，一个不可控状态变量，目标的存储空间。该空间包含3个离散状态（P2,P4,或不存在），以及含有描述逻辑的4个父对象。

    当目标不存在或者机器人离开P2或P4区找到目标时，按照本算法设计的混合自动机在运行时会被PHAVer检测到处于一个不安全或者不正确的集合中。模式检测器就找不出使机器人进入不安全状态的混合自动机的不安全执行进程了。这个问题的解决办法可以简便地通过该对象网络转换和验证过程得以发现并验证。
    本文所给的对象网络转换软件能够快速与精确地将复杂的对象网络转化为线性混合自动机。该自动机可以通过现在的符号模式检测软件如PHAVer得到验证。该自动工具能使更多的对象网络得以验证，因而对于基于对象控制程序特别是如MDS的控制构架有特别的促进作用。
参考文献
[1] 张达科,胡跃明.一类仿射非线性混合系统的去混合化控制[J]. 华南理工大学学报, 2004，32(11): 32-35.
[2] 董威,王戟,齐治昌. 并发和实时系统的模型检验技术[J]. 计算机研究与发展，2001，06: 24-27.
[3] 康宇,奚宏生,季海波，等. 一类不确定混合线性系统鲁棒自适应控制[N].中国科学技术大学学报，2004(6): 45-48.
[4] 吴为民.数字系统的形式化验证[N]. 计算机世界报，2005，37:11-12.
[5] 王巧丽.SPIN模型检测的研究与应用[J]. 贵州大学学报,2006，10：17-20.
[6] Holzmann, Gerard .The SPIN Model Checker, Pearson.
[7] Labinaz G,Bayoumi M.M, Rudie K.A survey of modeling and control of hybrid systems. Annual Reviews of Control,1997.
[8] Henzinger T, Ho P.-H, Toi H W. HyTech:A model checker for hybrid systems. International Journal on software Tools for Technology Transfer, 1997.
[9] Henzinger T, Ho P. -H. Automatic symbolic verification of embedded systems.IEEE Transactions on Software Engineering,1996, 22 (3). 181-201.
[10] Dvorak D,Rasmussen R, Starbrid T. State knowledge representation in the Mission Data System. IEEE Aerospace Conference, 2002.