数控系统的模型转换形式化语义集成框架的实现方法

摘要

本发明提供了数控系统的模型转换形式化语义集成框架的实现方法，其构建了数控系统形式化语义集成框架，领域元模型实例化得到的领域应用模型可通过该集成框架自动转换为形式化应用模型，进而可通过工具解释器，导入第三方仿真验证工具中进行形式化验证，或者通过代码自动生成解释器，生成特定目标平台的可执行代码。本发明为数控系统开发提供严格定义的形式化规范以精确描述系统相应的操作语义，使得数控系统模型可以通过计算机工具进行精确化验证，大大提高系统可靠性、安全性等性能。

权利要求

1.数控系统的模型转换形式化语义集成框架的实现方法，其特征是实现计算机数控系统的形式化描述与模型自动转换仿真验证，包括以下步骤：

1）通过分析数控系统的行为特征，构建一组计算模型描述数控系统的不同方面，本系统中将该组计算机模型称为语义模块；所构建的数控系统形式化语义模块能从不同方面描述系统的不同行为；所述描述数控系统的不同方面包括：采用有限状态机语义模块，描述数控系统中与状态转换相关的语义行为；采用同步数据流语义模块，描述数控系统中的数据流动；采用同步数据流与有限状态机两种计算组合而成的语义模块，描述数控系统中状态转换和数据流动的混合行为；采用时间自动机与时间多任务两种MOC组合而成的语义模块，描述数控系统中与实时相关的状态转换和任务执行方式；

2）基于步骤1）的语义模块，采用类UML语言构建数控系统的形式化元模型；根据数控系统形式化元模型与一组数控系统领域元模型，构建系统的形式化语义转换规则；所构建的系统的形式化语义转换规则是基于步骤1）所构建的语义模块，并通过分析其系统结构与对应关系而获得的；所述数控系统形式化元模型是基于数控系统的多方面形式化语义，并将不同方面的形式化元模型集成为数控系统统一的语义域；在数控系统领域建模环境下构建一组领域应用模型，利用系统形式化转换规则与形式化元模型，通过模型转换，自动生成系统的形式化应用模型；

3）基于数控系统形式化元模型和相关仿真验证工具，构建系统形式化仿真验证解释器；基于数控系统的形式化应用模型与仿真验证解释器，对数控系统进行形式化仿真验证，在Matlab软件中仿真其轨迹，在UPPAAL中验证其实时性和状态可达性。

2.根据权利要求1所述的数控系统的模型转换形式化语义集成框架的实现方法，其特征是所构造的形式化仿真验证解释器最终实现数控系统的形式化模型的自动验证仿真，保证系统的功能与性能。

说明书

数控系统的模型转换形式化语义集成框架的实现方法

技术领域

[0001] 本发明涉及计算机数控领域，特别涉及面向数控系统开发的模型转换形式化语义集成方法。

背景技术

[0002] 现代高性能数控系统朝着高速高精、智能化、多功能、多任务以及开放式体系结构的趋势发展，加上数控系统固有的强实时特性，使得传统的设计方法不能满足数控系统的性能需求。面向领域建模与领域逻辑直接相关，其模型构成符合领域逻辑的思维习惯，方便领域专家和软件开发人员的交流，具有直观性、领域特定性以及平台独立性的特点。基于领域模型的系统开发方法，可提高系统的开发效率，实现系统的可重用性。但是，现有的数控建模方式缺乏形式化的表达规范，因此无法精确描述系统，更缺乏基于形式化的仿真验证机制，从而导致系统语义不明确，无法从根本上解决系统的可靠性问题。

[0003] 发明内容：

[0004] 本发明为了克服数控系统开发中，模型的非形式化表征可能导致的系统语义不明确、正确性安全性得不到保证等问题，提供数控系统的模型转换形式化语义集成框架的实现方法。为实现上述目的，包含以下步骤：

[0005] 数控系统的模型转换形式化语义集成框架的实现方法，该方法能实现计算机数控系统的形式化描述与模型自动转换仿真验证，包括以下步骤：

[0006] 1）通过分析数控系统的行为特征，构建一组计算模型描述数控系统的不同方面，本系统中将该组计算机模型称为语义模块；

[0007] 2）基于步骤1）的语义模块，采用类UML语言构建数控系统的形式化元模型；根据数控系统形式化元模型与一组数控系统领域元模型，构建系统的形式化语义转换规则；

[0008] 3）基于数控系统形式化元模型和相关仿真验证工具，构建系统形式化仿真验证解释器；基于数控系统的形式化应用模型与仿真验证解释器，对数控系统进行形式化仿真验证，在Matlab软件中仿真其轨迹，在UPPAAL中验证其实时性和状态可达性。

[0009] 上述的数控系统的模型转换形式化语义集成框架的实现方法中，步骤1）所构建的数控系统形式化语义模块能从不同方面描述系统的不同行为。

[0010] 上述的数控系统的模型转换形式化语义集成框架的实现方法中，步骤1）所述描述数控系统的不同方面包括：采用有限状态机语义模块，描述数控系统中与状态转换相关的语义行为；采用同步数据流语义模块，描述数控系统中的数据流动；采用同步数据流与有限状态机两种计算组合而成的语义模块，描述数控系统中状态转换和数据流动的混合行为；采用时间自动机与时间多任务两种MOC组合而成的语义模块，描述数控系统中与实时相关的状态转换和任务执行方式。

[0011] 上述的数控系统的模型转换形式化语义集成框架的实现方法中，步骤2）所构建的系统的形式化语义转换规则是基于步骤1）所构建的语义模块，并通过分析其系统结构与对应关系而获得的。

[0012] 上述的数控系统的模型转换形式化语义集成框架的实现方法中，所构建的数控系统形式化元模型是基于数控系统的多方面形式化语义，并将不同方面的形式化元模型集成为数控系统统一的语义域；在数控系统领域建模环境下构建一组领域应用模型，利用系统形式化转换规则与形式化元模型，通过模型转换，自动生成系统的形式化应用模型。

[0013] 上述的数控系统的模型转换形式化语义集成框架的实现方法中，所构造的形式化仿真验证解释器最终实现数控系统的形式化模型的自动验证仿真，保证系统的功能与性能。

[0014] 与现有技术相比，本发明具有如下优点和技术效果：现有的数控建模方式缺乏形式化的表达规范，因此无法精确描述系统，更缺乏基于形式化的仿真验证机制，从而导致系统语义不明确，无法从根本上解决系统的可靠性问题。本发明构建了数控系统形式化语义集成框架，领域元模型实例化得到的领域应用模型可通过该集成框架自动转换为形式化应用模型，进而可通过工具解释器，导入第三方仿真验证工具中进行形式化验证，或者通过代码自动生成解释器，生成特定目标平台的可执行代码。本发明为数控系统开发提供严格定义的形式化规范以精确描述系统相应的操作语义，使得数控系统模型可以通过计算机工具进行精确化验证，大大提高系统可靠性、安全性等性能。

附图说明

[0015] 图1为数控系统的模型转换形式化语义集成框架的实现流程图。

具体实施方式

[0016] 以下结合附图对本发明的实施作进一步说明。

[0017] 数控系统的模型转换形式化语义集成框架为数控系统开发提供严格定义的形式化规范以精确描述系统相应的操作语义，使得数控系统模型可以通过计算机工具进行精确化验证。形式化语义集成框架包括基于平台的定义和基于应用的实现两个方面。在平台层，定义领域元模型、形式化元模型和元模型层的模型转换规则，通过该转换规则，将领域元模型和形式化元模型进行匹配，使得在应用层，由领域元模型实例化得到的领域应用模型可通过模型转换器自动转换为形式化元模型实例化得到的形式化应用模型，进而可通过工具解释器，导入第三方仿真验证工具中进行形式化验证，或者通过代码自动生成解释器，生成特定目标平台的可执行代码。

[0018] 数控系统的模型转换形式化语义集成框架的实现包括：

[0019] 1）形式化语义模块构建

[0020] 通过分析数控系统的行为特征，采用一组计算模型描述数控系统的不同方面，本系统中将其称为语义模块，如采用有限状态机语义单元，描述数控系统中与状态转换相关的语义行为；采用同步数据流语义模块，描述数控系统中的数据流动；采用同步数据流与有限状态机两种计算组合而成的语义模块，描述数控系统中状态转换和数据流动的混合行为；采用时间自动机与时间多任务两种MOC组合而成的语义单元，描述数控系统中与实时相关的状态转换和任务执行方式。

[0021] 2）形式化元模型构建

[0022] 形式化元建模基于数控系统形式化语义模块的特征，通过类UML语言，以及约束描述语言OCL，构建系统的建模形式、抽象语法以及它们之间的关系和组织方式。

[0023] 3）形式化转换规则构建

[0024] 领域描述和形式化描述的抽象语法均采用UML和OCL定义，因此，定义两种抽象语法之间的转换需要使用同样的语言。采用图形重写与转换的方式，通过将源语言的抽象语法与目标语言的抽象语法对应，以图形化的方式实现模型之间的转换，形成一组层次化的模型转换规则，该规则包含目标图形生成、生成条件以及属性映射。通过执行该规则，实现由领域元模型实例化的领域模型自动转化为由形式化元模型实例化的形式化模型，进而实现形式化语义映射。

[0025] 4）形式化应用模型自动生成

[0026] 数控系统的领域元模型可自动生成数控系统开发环境，并在该环境下构建系统应用模型。形式化模型转换工具则集成在系统开发环境中，基于该环境，可通过模型转换，将数控系统领域应用模型转换为数控系统形式化应用模型。

[0027] 5）形式化仿真验证解释器构建

[0028] 通过构建从形式化模型到相关仿真验证工具模型的转换规则，实现形式化仿真验证解释器的构建。

[0029] 6）基于形式化应用模型的仿真验证与实现

[0030] 基于生成的解释器，可将形式化应用模型自动转化为相关第三方仿真验证工具中，如Matlab（Simulink是MATLAB最重要的组件之一，它提供一个动态系统建模、仿真和综合分析的集成环境）、UPPAAL等环境下的相关模型，对其进行实时性验证。

[0031] 实例：以构建数控系统时间自动机与时间多任务两种MOC组成的语义模块为例，说明数控系统的形式化语义集成框架的实现过程。

[0032] 1）采用时间自动机和时间多任务两种MOC，描述系统与时间相关的状态转换和实时任务的执行行为。数控系统是典型的实时多任务系统，因此，该语义模块适用于描述数控系统的任务实施行为，以通过实时性验证，保证数控系统实时性能。时间自动机通过使用有限个真值时钟变量表示有时间约束的状态转换图，用来表示实时系统中具有时间约束的状态转换。时间多任务描述数控系统的时间多任务语义行为，通过定义任务执行方式刻画实时系统的实施行为，采用固定优先级的可抢占调度方式，任务通过周期性或非周期性的事件触发，根据其优先级高低可抢占式执行。采用时间自动机描述任务内部的状态转换行为规则，采用时间多任务描述任务之间进行调度的行为规则，从而保证其实施模型具有完备的形式化执行语义。

[0033] 2）基于时间自动机和时间多任务两种MOC所描述的语义规则，构建该MOC的形式化元模型。

[0034] 3）在GME中构建数控系统领域元模型，进而生成数控系统领域模型开发环境，用户可在该环境下构建数控系统的领域应用模型。基于数控领域元模型和形式化元模型，采用图形化转换方式，实现领域规则到形式化规则的映射，即实现时间自动机和时间多任务的语义集成。采用层次化结构描述模型转换规则定义从领域语言构建的任务模型到形式化中的时间自动机模型之间的映射。这些规则将领域模型中的对象分别对应于形式化语义单元中的对象上，并通过属性映射定义所构建的新的对象的属性信息。采用该转换规则，数控系统任务模型可自动转换成由该形式化语义模块所定义的形式化模型，如图所示，调度器（Scheduler），时钟（Timer）和任务（Task）被转换为时间自动机模型，并定义了其内部所包含的带时间参数的状态转换规则，

[0035] 任务模型定义了四个数控系统的任务和任务调度模块，并通过右边的窗口设定了任务的实时性能参数属性，包括系统的最坏执行时间（WCET）、周期（Period）、截止时间（Deadine）、优先级（Priority）等属性。通过转换规则，可转换为形式化TA模型。

[0036] 4）在数控系统领域建模环境下，构建系统应用模型，则可基于之前的形式化映射规则，通过模型自动转换，自动生成时间自动机和时间多任务语义模块的形式化应用模型。

[0037] 5）基于生成的解释器，可将形式化应用模型自动转化为UPPAAL环境下的相关模型，对其进行实时性验证。