一种用于机器人分布式控制系统的形式建模方法及装置

摘要

本发明实施例提供了一种用于机器人分布式控制系统的形式建模方法及装置，方法包括：针对所述机器人分布式控制系统，根据各微体系结构模型xMAS元件的同步等式，对各xMAS元件在逻辑编程语言ACL2中形式化，得到所述机器人分布式控制系统对应的xMAS元模型；其中，所述各xMAS元件包括Arbiter及以下至少一项：Fork、Join、Switch、Merge、Queue、Sink、Source、和Function；在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证；根据所述xMAS元模型，建立所述机器人分布式控制系统对应的xMAS网络。本发明实施例中，能够针对机器人分布式控制系统，创建对应的xMAS网络，进而可以根据xMAS网络实现对机器人分布式控制系统的全面验证。

说明书

技术领域

本发明涉及计算机技术领域，特别是涉及一种用于机器人分布式控制系统的形式建模方法及装置。

背景技术

机器人系统是机器人信息处理和控制的核心，其设计质量对机器人系统的整体行为和性能起到至关重要的作用。随着机器人技术的迅速发展，机器人系统的安全性问题也凸显出来，特别是机器人系统中实时分布式控制部分，其任务通常安全攸关，保证其设计实现的正确性和可靠性非常重要。机器人控制实际上是对各个关节的运动进行控制，使其协同工作，从而完成更加复杂的任务。因此，如何对机器人控制系统进行验证变得越来越重要。

系统的形式验证通常有模型检验和定理证明两种方法，其中模型检验方法是根据系统状态以自动机的形式进行建模，对于复杂系统或分布式控制系统，这种方法容易产生状态爆炸，定理证明的方法通常是将系统描述成逻辑表达式进行验证，这种方法建模时通常抽象层次较高，不容易保留底层设计的结构信息。本申请中采用微体系结构模型进行形式建模，具体地，可以通过xMAS(eXecutable MicroArchitectural Specification，微体系结构模型)来进行系统验证的方法。该方法主要可以是基于图形原语在微体系结构级上进行系统设计、形式建模和验证。其中，定义了8个图形原语，也可以称为xMAS元件：Fork、Join、Switch、Merge、Queue、Sink、Source、以及Function。由于这些原语是形式定义的，因此用xMAS表达的模型可以很方便实现形式化推理和分析。

但是，由于机器人分布式控制系统中存在数据信息及控制信息的优先级传输需求，而上述方式不能实现优先级的验证，因此，如何实现对机器人分布式控制系统的全面验证，成为一个亟待解决的问题。

发明内容

本发明实施例的目的在于提供一种用于机器人分布式控制系统的形式建模方法及装置，以实现对机器人分布式控制系统的全面验证。具体技术方案如下：

第一方面，本发明实施例提供了一种用于机器人分布式控制系统的形式建模方法，所述方法包括：

针对所述机器人分布式控制系统，根据各微体系结构模型xMAS元件的同步等式，对各xMAS元件在逻辑编程语言ACL2中形式化，得到所述机器人分布式控制系统对应的xMAS元模型；其中，所述各xMAS元件包括Arbiter及以下至少一项：Fork、Join、Switch、Merge、Queue、Sink、Source、和Function；

在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证；

根据所述xMAS元模型，建立所述机器人分布式控制系统对应的xMAS网络。

可选地，所述方法还包括：

通过所述xMAS网络，对所述机器人分布式控制系统进行自动验证。

可选地，所述机器人分布式控制系统为基于控制器局域网CAN总线的机器人分布式控制系统，所述通过所述xMAS网络，对所述机器人分布式控制系统进行自动验证的步骤包括：验证以下条件是否均成立：

当所述xMAS网络中每个接收端都有存储空间时，所述xMAS网络输出数据；

所述CAN总线从每个发送端仲裁出优先级最高的数据包输入所述CAN总线上；

当所述CAN总线上有数据发送时，所述数据将发送到接收端；

发送端发出的数据包有接收端接收；

当接收端收到的数据包是发送给自己时，接收该数据包；当接收端收到的数据包不是发送给自己时，遗弃该数据包；

当接收端收到的数据是正确的命令时，执行并且反馈正常信息；当接收端收到的数据是错误的命令时，直接反馈错误信息。

可选地，所述通过所述xMAS网络，对所述机器人分布式控制系统进行自动验证之前，所述方法还包括：

对所述xMAS网络进行正确性验证。

可选地，所述xMAS网络包括：xMAS元件、xMAS信道、xMAS时序网络；所述对所述xMAS网络进行正确性验证的步骤包括：验证以下条件是否均成立：

所述xMAS元件、所述xMAS信道、所述xMAS时序网络中的每一项都不重复；

所有的xMAS元件的输入输出端口数量的总和为所述xMAS信道中所有信道数量总和的两倍；

针对每条xMAS信道，该xMAS信道为与该信道相连的终端xMAS元件的输入信道，且为与该信道相连的起始端xMAS元件的输出信道；

针对每个xMAS元件，该xMAS元件为该元件输入信道的终端元件，且为该元件输出信道的起始端元件。

可选地，所述对所述xMAS网络进行正确性验证的步骤包括：

通过预设的验证函数，对所述xMAS网络进行正确性验证。

可选地，所述方法还包括：

创建xMAS模型库，其中，所述xMAS模型库包括所述xMAS元模型和所述xMAS网络。

可选地，当所述各xMAS元件包括Arbiter、Fork、Join、Switch、Merge、Queue、Sink、Source、和Function时，所述在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证的步骤包括：验证以下条件是否均成立：

针对Fork元件，当输入信道连通时，两个输出信道同时连通；

针对Join元件，当两个输入信道连通时，输出信道同时连通；

针对Switch元件，当输入信道连通时，其中一个输出信道同时连通；

针对Merge元件，当其中一个输入信道连通时，输出信道同时连通；

针对Function元件，当输入信道连通时，输出信道同时连通；

针对Queue元件，当队列为空时，下一个状态输入信道的读信号为真，且输出信道的写信号为假；当队列满时，下一个状态输入信道的读信号为假，且输出信道的写信号为真；当队列不空不满时，下一个状态输入信道的读信号为真，且输出信道的写信号为真；

针对Sink元件，当输入信号oracle为真时，下一个状态输入信道的读信号为真；

针对Source元件，当输入信号oracle为真时，下一个状态输出信道的写信号为真。

第二方面，本发明实施例提供了一种用于机器人分布式控制系统的形式建模装置，所述装置包括：

形式化模块，用于针对所述机器人分布式控制系统，根据各微体系结构模型xMAS元件的同步等式，对各xMAS元件在逻辑编程语言ACL2中形式化，得到所述机器人分布式控制系统对应的xMAS元模型；其中，所述各xMAS元件包括Arbiter及以下至少一项：Fork、Join、Switch、Merge、Queue、Sink、Source、和Function；

第一验证模块，用于在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证；

建立模块，用于根据所述xMAS元模型，建立所述机器人分布式控制系统对应的xMAS网络。

可选地，所述装置还包括：

第二验证模块，用于通过所述xMAS网络，对所述机器人分布式控制系统进行自动验证。

可选地，所述机器人分布式控制系统为基于控制器局域网CAN总线的机器人分布式控制系统，所述第二验证模块，具体用于验证以下条件是否均成立：

当所述xMAS网络中每个接收端都有存储空间时，所述xMAS网络输出数据；

所述CAN总线从每个发送端仲裁出优先级最高的数据包输入所述CAN总线上；

当所述CAN总线上有数据发送时，所述数据将发送到接收端；

发送端发出的数据包有接收端接收；

当接收端收到的数据包是发送给自己时，接收该数据包；当接收端收到的数据包不是发送给自己时，遗弃该数据包；

当接收端收到的数据是正确的命令时，执行并且反馈正常信息；当接收端收到的数据是错误的命令时，直接反馈错误信息。

可选地，所述装置还包括：

第三验证模块，用于对所述xMAS网络进行正确性验证。

可选地，所述xMAS网络包括：xMAS元件、xMAS信道、xMAS时序网络；所述第三验证模块，具体用于验证以下条件是否均成立：

所述xMAS元件、所述xMAS信道、所述xMAS时序网络中的每一项都不重复；

所有的xMAS元件的输入输出端口数量的总和为所述xMAS信道中所有信道数量总和的两倍；

针对每条xMAS信道，该xMAS信道为与该信道相连的终端xMAS元件的输入信道，且为与该信道相连的起始端xMAS元件的输出信道；

针对每个xMAS元件，该xMAS元件为该元件输入信道的终端元件，且为该元件输出信道的起始端元件。

可选地，所述第三验证模块，具体用于通过预设的验证函数，对所述xMAS网络进行正确性验证。

可选地，所述装置还包括：

创建模块，用于创建xMAS模型库，其中，所述xMAS模型库包括所述xMAS模型和所述xMAS网络。

可选地，当所述各xMAS元件包括Arbiter、Fork、Join、Switch、Merge、Queue、Sink、Source、和Function时，所述第一验证模块，具体用于验证以下条件是否均成立：

针对Fork元件，当输入信道连通时，两个输出信道同时连通；

针对Join元件，当两个输入信道连通时，输出信道同时连通；

针对Switch元件，当输入信道连通时，其中一个输出信道同时连通；

针对Merge元件，当其中一个输入信道连通时，输出信道同时连通；

针对Function元件，当输入信道连通时，输出信道同时连通；

针对Queue元件，当队列为空时，下一个状态输入信道的读信号为真，且输出信道的写信号为假；当队列满时，下一个状态输入信道的读信号为假，且输出信道的写信号为真；当队列不空不满时，下一个状态输入信道的读信号为真，且输出信道的写信号为真；

针对Sink元件，当输入信号oracle为真时，下一个状态输入信道的读信号为真；

针对Source元件，当输入信号oracle为真时，下一个状态输出信道的写信号为真。

本发明实施例提供了一种用于机器人分布式控制系统的形式建模方法及装置，方法包括：针对所述机器人分布式控制系统，根据各微体系结构模型xMAS元件的同步等式，对各xMAS元件在逻辑编程语言ACL2中形式化，得到所述机器人分布式控制系统对应的xMAS元模型；其中，所述各xMAS元件包括Arbiter及以下至少一项：Fork、Join、Switch、Merge、Queue、Sink、Source、和Function；在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证；根据所述xMAS元模型，建立所述机器人分布式控制系统对应的xMAS网络。

本发明实施例中，能够针对机器人分布式控制系统，创建对应的xMAS网络，并且，该xMAS网络中包括表达优先级的Arbiter元件，从而根据xMAS网络能够实现对机器人分布式控制系统的全面验证。

附图说明

为了更清楚地说明本发明实施例或现有技术中的技术方案，下面将对实施例或现有技术描述中所需要使用的附图作简单地介绍，显而易见地，下面描述中的附图仅仅是本发明的一些实施例，对于本领域普通技术人员来讲，在不付出创造性劳动的前提下，还可以根据这些附图获得其他的附图。

图1为本发明实施例提供的一种用于机器人分布式控制系统的形式建模方法的流程图；

图2为本发明实施例提供的一种用于机器人分布式控制系统的形式建模方法的另一流程图；

图3为本发明实施例提供的一种用于机器人分布式控制系统的形式建模装置的结构示意图；

图4为本发明实施例提供的一种用于机器人分布式控制系统的形式建模装置的另一结构示意图；

图5为本发明实施例的机器人分布式控制系统的结构示意图；

图6为本发明实施例的机器人分布式控制系统中主控节点的xMAS元模型；

图7为本发明实施例的机器人分布式控制系统中其中一个关节节点的xMAS元模型；

图8为本发明实施例的机器人分布式控制系统中另一个关节节点的xMAS元模型；

图9为本发明实施例的机器人分布式控制系统中再一个关节节点的xMAS元模型；

图10为本发明实施例的CAN网络的xMAS元模型；

图11为本发明实施例的元件Arbiter的图形表示示意图。

具体实施方式

为了实现对机器人分布式控制系统的全面验证，本发明实施例提供了一种用于机器人分布式控制系统的形式建模方法及装置。

下面将结合本发明实施例中的附图，对本发明实施例中的技术方案进行清楚、完整地描述，显然，所描述的实施例仅仅是本发明一部分实施例，而不是全部的实施例。基于本发明中的实施例，本领域普通技术人员在没有做出创造性劳动前提下所获得的所有其他实施例，都属于本发明保护的范围。

需要说明的是，在不冲突的情况下，本发明中的实施例及实施例中的特征可以相互组合。下面将参考附图并结合实施例来详细说明本发明。

本发明实施例提供了一种用于机器人分布式控制系统的形式建模方法过程，如图1所示，该过程可以包括以下步骤：

S101，针对机器人分布式控制系统，根据各微体系结构模型xMAS元件的同步等式，对各xMAS元件在逻辑编程语言ACL2中形式化，得到所述机器人分布式控制系统对应的xMAS元模型。

本发明实施例提供的方法可以应用于电子设备。具体地，该电子设备可以为台式计算机、便携式计算机、智能移动终端等。

在本发明实施例中，电子设备可以针对机器人分布式控制系统，创建对应的验证模型，以对该机器人分布式控制系统进行验证。

具体地，电子设备可以针对机器人分布式控制系统，根据各xMAS元件的同步等式，对各xMAS元件在ACL2(A Computational Logic for Applicative Common Lisp，逻辑编程语言)中形式化，得到该机器人分布式控制系统对应的xMAS元模型，也即得到机器人分布式控制系统的图形化表示。

例如，当机器人分布式控制系统包括多个关节节点时，电子设备可以分别得到各关节节点对应的xMAS元模型，以及机器人分布式控制系统对应的网络xMAS元模型；进而可以根据各关节节点对应的xMAS元模型，以及机器人分布式控制系统对应的网络xMAS元模型，组合得到机器人分布式控制系统对应的xMAS元模型。

其中，上述各xMAS元件可以包括Arbiter及以下至少一项：Fork、Join、Switch、Merge、Queue、Sink、Source、和Function。在本发明实施例中，可以根据机器人分布式控制系统，选择Arbiter元件以及其余的一种或多种元件进行形式化，以得到机器人分布式控制系统对应的xMAS元模型，本发明实施例对此不做限定。

下面针对各xMAS元件在形式化过程中所用的同步等式进行介绍：

Arbiter元件为表达优先级的元件，其同步等式可以为：

next(o.irdy):＝pre(a.irdy)or pre(b.irdy)

next(o.data):＝pre(a.data)if u*and pre(a.irdy)

pre(b.data)if not u*and pre(b.irdy)

next(a.trdy):＝u*and pre(o.trdy)and pre(a.irdy)

next(b.trdy):＝not u*and pre(o.trdy)and pre(b.irdy)；

其中，u*函数定义如下：

Fork为将一路输入同时分叉成两路输出的元件，其同步等式可以为：

next(a.irdy):＝pre(i.irdy)and pre(b.trdy)

next(a.data):＝f(pre(i.data))

next(b.irdy):＝pre(i.irdy)and pre(a.trdy)

next(b.data):＝g(pre(i.data))

next(i.trdy):＝pre(a.trdy)and pre(b.trdy)

其中，f为a端的数据转换函数，g为b端的数据转换函数。

Join为将两路输入联结成一路输出的元件，其同步等式可以为：

next(o.irdy):＝pre(a.irdy)and pre(b.irdy)

next(o.data):＝h(pre(a.data),pre(b.data))

next(a.trdy):＝pre(o.trdy)and pre(b.irdy)

next(b.trdy):＝pre(o.trdy)and pre(a.irdy)

其中，h为Join元件数据转换函数。

Switch为为数据包选择传输路径的元件，其同步等式可以为：

next(a.irdy):＝pre(i.irdy)and s(pre(i.data))

next(b.irdy):＝pre(i.irdy)and not s(pre(i.data))

next(a.data):＝pre(i.data)

next(b.data):＝pre(i.data)

next(i.trdy):＝pre(a.trdy)and s(pre(i.data))or pre(b.trdy)and not s(pre(i.data))

其中，s为路径选择函数，当s为真时，将数据传输到a端，否则传输到b端。

Merge为一种起到仲裁器作用的元件，其同步等式可以为：

next(o.irdy):＝pre(a.irdy)or pre(b.irdy)

next(o.data):＝pre(a.data)if u and pre(a.irdy)

pre(b.data)if not u and pre(b.irdy)

next(a.trdy):＝u and pre(o.trdy)and pre(a.irdy)

next(b.trdy):＝not u and pre(o.trdy)and pre(b.irdy)

其中，u是用于确保公平性输出的函数，定义如下：

u:＝1 if pre(a.irdy)and not pre(b.irdy)

0 if not pre(a.irdy)and pre(b.irdy)

pre(u)otherwise

Queue为能够存储数据的元件，其同步等式可以为：

其中，pre返回的是前一个状态的值，next返回的是下一个状态的值。queue是队列的存储数据列表，num为队列的当前占有量。

Sink为用于消耗数据包的元件，其同步等式可以为：

next(i.trdy):＝oracle or pre(o.irdy)

其中，oracle为用于控制元件是否接收数据的变量。

Source为用于发送数据包的元件，其同步等式可以为：

next(o.irdy):＝oracle or pre(i.trdy)

next(o.data):＝e

其中，e为Source元件发送的数据。

Function为用于数据转换的元件，其同步等式可以为：

next(o.irdy):＝pre(i.irdy)

next(i.trdy):＝pre(o.trdy)

next(o.data):＝f(pre(i.data))

其中，f为Function元件的数据转换函数。

S102，在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证。

在xMAS元件形式化之后，引用这些元件就必须满足元件本身固有的属性，因此，在本发明实施例中，得到机器人分布式控制系统对应的xMAS元模型后，可以在ACL2中对该xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证。

其中，当各xMAS元件包括Arbiter、Fork、Join、Switch、Merge、Queue、Sink、Source、和Function时，组合逻辑元件包括Function、Fork、Join、Switch、和Merge元件；时序逻辑元件包括Source、Sink和Queue元件。

具体地，组合逻辑元件需要满足输入信道和输出信道的连通情况是同步的。其中，当一个信道的写信号irdy和读信号trdy同时为真时，那么这个信道就连通了。

例如，电子设备可以验证以下条件是否均成立：

针对Fork元件，当输入信道连通时，两个输出信道同时连通；

针对Join元件，当两个输入信道连通时，输出信道同时连通；

针对Switch元件，当输入信道连通时，其中一个输出信道同时连通；

针对Merge元件，当其中一个输入信道连通时，输出信道同时连通；

针对Function元件，当输入信道连通时，输出信道同时连通；

针对Queue元件，当队列为空时，下一个状态输入信道的读信号为真，且输出信道的写信号为假；当队列满时，下一个状态输入信道的读信号为假，且输出信道的写信号为真；当队列不空不满时，下一个状态输入信道的读信号为真，且输出信道的写信号为真；

针对Sink元件，当输入信号oracle为真时，下一个状态输入信道的读信号为真；

针对Source元件，当输入信号oracle为真时，下一个状态输出信道的写信号为真。

S103，根据所述xMAS元模型，建立所述机器人分布式控制系统对应的xMAS网络。

xMAS元模型是基于图像语言的模型，计算机不能对其直接进行识别运行，因此，在本发明实施例中，在得到机器人分布式控制系统对应的xMAS元模型，并通过预设属性的验证后，为了创建计算机能够识别的语言，进而能够对机器人分布式控制系统进行自动验证，电子设备可以根据xMAS元模型，建立机器人分布式控制系统对应的xMAS网络。

例如，电子设备可以首先对xMAS网络进行如下定义：

(1)xMAS网络由三部分组成：元件(components)、信道(channels)和时序网络(sequential-networks)；其中时序网络用于负责所有队列的数据包更新。

(2)xMAS元件component＝<id type ins ous param>，其中id用来标识不同的元件；type表示元件的类型，type只能在queue、function、source、sink、fork、join、switch和merge中取值；ins表示元件的所有输入信道的集合，输入信道的条数由元件的类型决定；ous表示元件的所有输出信道集合，输出信道的条数也是由元件的类型决定；param表示元件本身的参数。

(3)xMAS信道channel＝<id init target param data>，其中id标识不同的信道；init表示信道起始端元件的id；target表示信道终端元件的id；param表示与信道连接的两端元件的参数；data表示信道的值。信道由<irdy trdy data>组成，irdy表示信道的写信号，trdy表示信道的读信号，data表示信道传输的数据。

(4)xMAS时序网络sequential-network＝<init target connect-channels>，其中init表示时序元件(source和queue)组成的集合，当满足一定条件时，集合中的所有元件会同时进行数据输出操作。target表示时序元件(sink和queue)组成的集合，当满足一定条件时，集合中的所有元件会同时进行数据输入操作。connect-channels是由init为起点和target为终点的网络之间所连接的信道集合。当connect-channels都连通时，init集合中的每个元件都会输出数据包，target集合中的每个元件都会输入数据包，并且connect-channels集合中的信道将重置。

根据上述的四个定义，可以根据xMAS元模型，建立机器人分布式控制系统对应的xMAS网络，它表达出来了xMAS元模型的整体结构。

本发明实施例中，能够针对机器人分布式控制系统，创建对应的xMAS网络，并且，该xMAS网络中包括表达优先级的Arbiter元件，从而根据xMAS网络能够实现对机器人分布式控制系统的全面验证。

作为本发明实施例的一种实施方式，如图2所示，本实施例提供的用于机器人分布式控制系统的形式建模方法，还可以包括以下步骤：

S104，通过所述xMAS网络，对所述机器人分布式控制系统进行自动验证。

在本发明实施例中，当电子设备获得机器人分布式控制系统对应的xMAS网络后，其可以进一步通过该xMAS网络，对机器人分布式控制系统进行自动验证。例如，可以采用ACL2定理证明器对机器人分布式控制系统的功能正确性进行验证。

具体地，电子设备对机器人分布式控制系统进行自动验证时，可以验证以下条件是否均成立：

当xMAS网络中每个接收端都有存储空间时，xMAS网络输出数据；

CAN总线从每个发送端仲裁出优先级最高的数据包输入CAN总线上；

当CAN总线上有数据发送时，数据将发送到接收端；

发送端发出的数据包有接收端接收；

当接收端收到的数据包是发送给自己时，接收该数据包；当接收端收到的数据包不是发送给自己时，遗弃该数据包；

当接收端收到的数据是正确的命令时，执行并且反馈正常信息；当接收端收到的数据是错误的命令时，直接反馈错误信息。

本实施例中，可以通过xMAS网络，对机器人分布式控制系统进行自动验证。

可选地，为了保证从基于图形语言的xMAS元模型到xMAS网络转换的正确性，通过xMAS网络，对机器人分布式控制系统进行自动验证之前，可以首先对xMAS网络进行正确性验证。

具体地，电子设备对xMAS网络进行正确性验证的步骤可以包括：验证以下条件是否均成立：

xMAS元件、xMAS信道、xMAS时序网络中的每一项都不重复；

所有的xMAS元件的输入输出端口数量的总和为xMAS信道中所有信道数量总和的两倍；

针对每条xMAS信道，该xMAS信道为与该信道相连的终端xMAS元件的输入信道，且为与该信道相连的起始端xMAS元件的输出信道；

针对每个xMAS元件，该xMAS元件为该元件输入信道的终端元件，且为该元件输出信道的起始端元件。

其中，电子设备可以通过预设的验证函数，对xMAS网络进行正确性验证。如，可以通过xmasnetworkp函数对xMAS网络进行正确性验证。

xMAS网络的运行主要包括信道控制信号值的计算和队列中数据的更新。在ACL2中，可以用channel-calculate函数完成信道控制信号的计算任务，用data-transfer函数完成所有队列数据的更新任务。用run-network-n函数完成xMAS网络的运行，先调用channel-calculate计算出所有信道的值，然后调用data-transfer完成所有队列数据的更新任务。

作为本发明实施例的一种实施方式，得到机器人分布式控制系统对应的xMAS元模型和xMAS网络后，电子设备还可以创建包括该xMAS元模型和xMAS网络的xMAS模型库，以方便重复利用。

例如，电子设备可以按照以下步骤，创建xMAS模型库：

第一步：定义一个空包，取名可以为XMAS；

第二步：将xMAS元件和xMAS网络相关函数定义在XMAS包中。创建一个新的lisp文件，取名为xmas,在文件开头加入(in-package"XMAS")，然后将已经定义好的函数放到一个文件下；

第三步：将lisp文件编译成库函数。

本实施例中，可以创建包括xMAS元模型和xMAS网络的xMAS模型库，从而可以重复利用。

相应于上面的方法实施例，本发明实施例还提供了相应的装置实施例。

图3为本发明实施例提供的一种用于机器人分布式控制系统的形式建模装置，所述装置包括：

形式化模块310，用于针对所述机器人分布式控制系统，根据各微体系结构模型xMAS元件的同步等式，对各xMAS元件在逻辑编程语言ACL2中形式化，得到所述机器人分布式控制系统对应的xMAS元模型；其中，所述各xMAS元件包括Arbiter及以下至少一项：Fork、Join、Switch、Merge、Queue、Sink、Source、和Function；

第一验证模块320，用于在ACL2中对所述xMAS元模型中的组合逻辑元件和时序逻辑元件进行预设属性的验证；

建立模块330，用于根据所述xMAS元模型，建立所述机器人分布式控制系统对应的xMAS网络。

本发明实施例中，能够针对机器人分布式控制系统，创建对应的xMAS网络，并且，该xMAS网络中包括表达优先级的Arbiter元件，从而根据xMAS网络能够实现对机器人分布式控制系统的全面验证。

作为本发明实施例的一种实施方式，如图4所示，所述装置还包括：

第二验证模块340，用于通过所述xMAS网络，对所述机器人分布式控制系统进行自动验证。

作为本发明实施例的一种实施方式，所述机器人分布式控制系统为基于CAN总线的机器人分布式控制系统，所述第二验证模块340，具体用于验证以下条件是否均成立：

当所述xMAS网络中每个接收端都有存储空间时，所述xMAS网络输出数据；

所述CAN总线从每个发送端仲裁出优先级最高的数据包输入所述CAN总线上；

当所述CAN总线上有数据发送时，所述数据将发送到接收端；

发送端发出的数据包有接收端接收；

当接收端收到的数据包是发送给自己时，接收该数据包；当接收端收到的数据包不是发送给自己时，遗弃该数据包；

当接收端收到的数据是正确的命令时，执行并且反馈正常信息；当接收端收到的数据是错误的命令时，直接反馈错误信息。

作为本发明实施例的一种实施方式，所述装置还包括：

第三验证模块(图中未示出)，用于对所述xMAS网络进行正确性验证。

作为本发明实施例的一种实施方式，所述xMAS网络包括：xMAS元件、xMAS信道、xMAS时序网络；所述第三验证模块，具体用于验证以下条件是否均成立：

所述xMAS元件、所述xMAS信道、所述xMAS时序网络中的每一项都不重复；

所有的xMAS元件的输入输出端口数量的总和为所述xMAS信道中所有信道数量总和的两倍；

针对每条xMAS信道，该xMAS信道为与该信道相连的终端xMAS元件的输入信道，且为与该信道相连的起始端xMAS元件的输出信道；

针对每个xMAS元件，该xMAS元件为该元件输入信道的终端元件，且为该元件输出信道的起始端元件。

作为本发明实施例的一种实施方式，所述第三验证模块，具体用于通过预设的验证函数，对所述xMAS网络进行正确性验证。

作为本发明实施例的一种实施方式，所述装置还包括：

创建模块(图中未示出)，用于创建xMAS模型库，其中，所述xMAS模型库包括所述xMAS模型和所述xMAS网络。

作为本发明实施例的一种实施方式，当所述各xMAS元件包括Arbiter、Fork、Join、Switch、Merge、Queue、Sink、Source、和Function时，所述第一验证模块，具体用于验证以下条件是否均成立：

针对Fork元件，当输入信道连通时，两个输出信道同时连通；

针对Join元件，当两个输入信道连通时，输出信道同时连通；

针对Switch元件，当输入信道连通时，其中一个输出信道同时连通；

针对Merge元件，当其中一个输入信道连通时，输出信道同时连通；

针对Function元件，当输入信道连通时，输出信道同时连通；

针对Queue元件，当队列为空时，下一个状态输入信道的读信号为真，且输出信道的写信号为假；当队列满时，下一个状态输入信道的读信号为假，且输出信道的写信号为真；当队列不空不满时，下一个状态输入信道的读信号为真，且输出信道的写信号为真；

针对Sink元件，当输入信号oracle为真时，下一个状态输入信道的读信号为真；

针对Source元件，当输入信号oracle为真时，下一个状态输出信道的写信号为真。

下面结合一个具体的实施例，对本发明提供的用于机器人分布式控制系统的形式建模方法进行详细介绍。

机器人控制实际上是对各个关节的运动进行控制，使其协同工作，从而完成更加复杂的任务。如图5所示，本发明实施例的机器人分布式控制系统可以由上位机主控模块、通信模块和下位机关节控制器模块组成。其中上位机主控模块负责整个系统的调度管理、轨迹规划和人机交互等功能；下位机关节控制器模块控制各个关节的运动；通信模块负责上位机主控模块与下位机关节控制器模块之间的实时信息交换。

机器人分布式控制系统中通信方式的选择至关重要，既要满足通信的高可靠性和实时性，又要求硬件连接简单，易扩展。本发明实施例中，机器人分布式控制系统采用CAN(Controller Area Network，控制器局域网)总线标准，CAN总线的高性能和可靠性已被认同，现场总线是当今自动化领域技术发展的热点之一，被誉为自动化领域的计算机局域网。

机器人分布式控制系统整体上是由CAN节点和CAN网络两部分组成。CAN节点大体分为三部分：CAN收发器、CAN控制器和微控制器，其中CAN控制器是CAN节点中的核心内容，本实施例中对CAN节点建立的xMAS元模型是对CAN控制器建立的xMAS元模型。

发明实施例的机器人分布式控制系统可以由四个节点通过CAN网络相互连接而成，其中一个主控节点发送指令信息，接收关节节点的反馈信息，三个关节节点接收主控节点的指令信息和发送反馈信息。对机器人分布式控制系统建立xMAS元模型，分为对CAN节点和CAN网络建立xMAS元模型两部分。

请参考图6-图9，图6示出了主控节点的xMAS元模型，图7-图9分别示出了三个关节节点(关节节点1、关节节点2、关节节点3)的xMAS元模型。

CAN总线分布式机器人控制系统通常是对通信数据包进行编码。这种方式不仅减轻了CAN网络路由选择的压力，而且便于添加新的通信节点。本系统采用消息结构，即(IDDATA)。ID代表数据包的标识，同时也代表着优先级的高低，ID越小，数据包的优先级越高。DATA代表传输的数据包。本系统涉及到三种数据包：错误反馈数据包，正常接收反馈数据包和数据包。它们的优先级由高到低分别是错误反馈数据包，正常接收反馈数据包和数据包。错误反馈数据包ID为0～9，正常接收反馈数据包ID为10～19，数据包ID为20～29。

对于CAN网络采用非破坏性总线仲裁技术。当多个节点向总线发送数据时，节点信息优先级低的主动退出发送，而最高优先级的节点可不受影响的继续传输数据。在本发明实施例中，创建Arbiter元件之后，可以建立CAN网络的xMAS元模型，如图10所示，满足了CAN网络非破坏性总线仲裁的要求，使得优先级高的数据包优先传输，其中，图11示出了元件Arbiter的图形表示。

在主控节点中，为了xMAS元模型的正常运行，需要对图6中的Switch元件com_22和Source元件com_31进行参数配置。Switch元件com_22接收的数据包如果ID为1～6，即为错误反馈数据包，则通过信道chan_33传输；如果ID为11～16，即为正常反馈数据包，则通过信道chan_34传输。Source元件com_31可以发送ID为21～26的数据包，ID为21和22的数据包发送给关节节点1，ID为23和24的数据包发送给关节节点2，ID为25和26的数据包发送给关节节点3。

在关节节点1中，为了xMAS元模型的正常运行，需要对图7中的Switch元件com_42、com_44和Function元件com_49、com_50进行参数配置。Switch元件com_42接收的数据包如果ID为21或22，即发送给自己的数据包，需要节点接收，则通过信道chan_44传输；否则，即为不是发送给自己的数据包，需要节点抛弃，则通过信道chan_45传输。Switch元件com_44接收的数据包DATA为up或down，即动作指令正确，则通过信道chan_47传输；否则，即动作指令错误，则通过信道chan_48传输。Function元件com_50将ID为21和22的数据包，转换成ID为11和12，DATA为Success的正常反馈数据包。Function元件com_49将ID为21和22的数据包，转换成ID为1和2，DATA为Error的错误反馈数据包。

在关节节点2中，为了xMAS元模型的正常运行，需要对图8中的Switch元件com_62、com_64和Function元件com_69、com_70进行参数配置。Switch元件com_62接收的数据包如果ID为23或24，即发送给自己的数据包，需要节点接收，则通过信道chan_64传输；否则，即为不是发送给自己的数据包，需要节点抛弃，则通过信道chan_65传输。Switch元件com_64接收的数据包DATA为left或right，即动作指令正确，则通过信道chan_67传输；否则，即动作指令错误，则通过信道chan_68传输。Function元件com_69将ID为23和24的数据包，转换成ID为13和14，DATA为Success的正常反馈数据包。Function元件com_70将ID为23和24的数据包，转换成ID为3和4，DATA为Error的错误反馈数据包。

在关节节点3中，为了xMAS元模型的正常运行，需要对图9中的Switch元件com_14、com_16和Function元件com_33、com_34进行参数配置。Switch元件com_14接收的数据包如果ID为25或26，即发送给自己的数据包，需要节点接收，则通过信道chan_84传输；否则，即为不是发送给自己的数据包，需要节点抛弃，则通过信道chan_85传输。Switch元件com_16接收的数据包DATA为front或back，即动作指令正确，则通过信道chan_87传输；否则，即动作指令错误，则通过信道chan_88传输。Function元件com_33将ID为25和26的数据包，转换成ID为15和16，DATA为Success的正常反馈数据包。Function元件com_34将ID为25和26的数据包，转换成ID为5和6，DATA为Error的错误反馈数据包。

将图6、7、8、9和10中标号相同的信道连接起来，为CAN总线分布式机器人控制系统的图形化表达，即机器人分布式控制系统的xMAS元模型。

进一步地，根据xMAS网络的定义，即xMAS网络分三部分：components、channels、sequential-networks，可以将xMAS元模型转换为xMAS网络，即xMAS元模型的静态结构。

具体地，可以将xMAS元模型中图形化表达的元件转换成ACL2可识别的符号化表达，如表1所示。

表1

将xMAS元模型中图形化表达的信道转换成ACL2可识别的符号化表达，如表2所示。

表2

将xMAS元模型中时序网络转换成ACL2可识别的符号化表达，如表3所示。

表3

对于装置实施例而言，由于其基本相似于方法实施例，所以描述的比较简单，相关之处参见方法实施例的部分说明即可。

需要说明的是，在本文中，诸如第一和第二等之类的关系术语仅仅用来将一个实体或者操作与另一个实体或操作区分开来，而不一定要求或者暗示这些实体或操作之间存在任何这种实际的关系或者顺序。而且，术语“包括”、“包含”或者其任何其他变体意在涵盖非排他性的包含，从而使得包括一系列要素的过程、方法、物品或者设备不仅包括那些要素，而且还包括没有明确列出的其他要素，或者是还包括为这种过程、方法、物品或者设备所固有的要素。在没有更多限制的情况下，由语句“包括一个……”限定的要素，并不排除在包括所述要素的过程、方法、物品或者设备中还存在另外的相同要素。

本说明书中的各个实施例均采用相关的方式描述，各个实施例之间相同相似的部分互相参见即可，每个实施例重点说明的都是与其他实施例的不同之处。尤其，对于系统实施例而言，由于其基本相似于方法实施例，所以描述的比较简单，相关之处参见方法实施例的部分说明即可。

以上所述仅为本发明的较佳实施例而已，并非用于限定本发明的保护范围。凡在本发明的精神和原则之内所作的任何修改、等同替换、改进等，均包含在本发明的保护范围内。