一种从TASM时间抽象状态机到扩展NTA自动机的转换方法

摘要

本发明涉及应用领域中间模型进行转换的方法，提供一种能够直接将TASM时间抽象状态机模型转换为扩展NTA自动机的方法，以进一步帮助用户实现设计结论的验证。本发明方法的主要步骤如下：（1）建立基于TASM时间抽象状态机源模型结构和扩展NTA自动机目标模型结构的元模型。（2）创建TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换规则。（3）利用转换规则，实施TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换。

说明书

技术领域

本发明涉及应用领域中间模型进行转换的方法，特别涉及一种从TASM（TimedAbstactStateMachine，时间抽象状态机）时间抽象状态机到扩展NTA（NetworkofTimedAutomata，时间自动机网络）自动机的转换方法。

背景技术

基于模型驱动开发的理论意义是：第一，模型有利于早期设计方案的验证与测试。如可基于敏捷开发的方法，快速构造不同的设计方案，对于那些正在迭代中的方案，利用基于模型的代码生成技术，迅速产生代码框架，并可进行实质的验证或测试，以分析设计方案的质量。

第二，利用模型可以生成程序的框架，减轻设计者的设计负担和程序员的编码压力，有利于自动化软件生成。

当前，能够满足上述要求的中间模型有很多，如Petri网（一种对离散并行系统的数学表示方法）和TASM等。其中，设计者选择TASM作为中间模型的理由是：第一，TASM是抽象状态机（AbstractStateMachine，ASM）的一种扩展，既支持时序和资源消耗，同时也支持行为和通信的规约；第二，TASM支持层次组合、并发和通信等概念；第三，TASM采用并行执行的主机（mainmachine）集合来支持并行行为的规约，并提供子机（sub-machine）和功能机（function-machine）调用以支持层次行为的规约；第四，通信仅发生在主机之间并可以使用通道同步和共享变量；第五，TASM语言具有形式化语义，这一语义能够成为一种可执行的规范。

同时，TASM可作为某种（如AADL，ArchitectureAnalysisandDesignLanguage，体系结构分析与设计语言）嵌入式实时系统的高层设计的中间模型（即TASM时间抽象状态机），该中间模型表示的设计结论与实际的业务处理平台无关。因此，当需要对采用AADL语言描述的嵌入式实时系统的高层设计实施具体的验证活动时，需要将该TASM时间抽象状态机模型与具体的验证平台进行绑定，即需要将该TASM时间抽象状态机模型转换成某种具体验证平台的输入文件。

UPPAAL（一个使用扩展NTA自动机作为输入模型的仿真验证平台）就是这样一种针对嵌入式实时系统提供形式化验证的平台，其输入形式采用了扩展NTA自动机，输出为验证的结论。然而现有技术中没有将TASM模型直接转换为扩展NTA自动机模型的方法，因此无法实现设计结论的验证。

发明内容

本发明的目的在于针对上述问题与不足，提供一种能够直接将TASM时间抽象状态机模型转换为扩展NTA自动机的方法，以进一步帮助用户实现设计结论的验证。

为达到上述目的，本发明采用如下的技术方案。

本发明提供一种从TASM时间抽象状态机到扩展NTA自动机的转换方法，本方法步骤执行的前提是，已知一个TASM时间抽象状态机模型的源文件，该文件的格式为XMI（XML-basedMetadataInterchange，使用标准通用标记语言的子集可扩展标记语言）格式。本发明方法步骤完成转换后所得到的是NTA自动机模型，该文件为XMI格式。

本发明方法的主要步骤如下：

（1）建立基于TASM时间抽象状态机源模型结构和扩展NTA自动机目标模型结构的元模型。

采用以Ecore（EMF所提供的一种元模型结构）模型为父类的元模型来描述待转换的TASM时间抽象状态机源模型结构和转换后的扩展NTA自动机目标模型结构。具体选择Eclipse提供的EMF（EclipseModelingFramework，Eclipse所提供的模型开发框架）包来支持对Ecore元模型进行建模，具体对Ecore元模型进行建模的工具为EMF提供的Ecore建模器。将Ecore建模器所分别建立的TASM时间抽象状态机模型的元模型与扩展NTA自动机目标模型的元模型，使用持久化技术存入数据库中。

（2）创建TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换规则。

依据得到的TASM时间抽象状态机模型的元模型与扩展NTA自动机模型的元模型，按照TASM时间抽象状态机模型的元模型与扩展的NTA自动机模型的元模型之间的结构与语义关系，使用ATL转换规则编辑器建立这两种元模型之间的ATL（AtlasTransformationLanguage，Atlas转换语言）转换规则集。

具体创建转换规则时，即对TASM时间抽象状态机模型中的构件转换时，考虑三种情况。

第一种，变量：将TASM时间抽象状态机模型中的变量转换为扩展NTA自动机中的变量，由于TASM时间抽象状态机模型中变量的类型多于扩展NTA自动机所支持的变量类型，故需要对这些扩展NTA自动机不能直接支持的变量类型进行语义转换，即对TASM时间抽象状态机模型中的变量中那些无法直接用扩展NTA自动机变量表示的变量，使用扩展NTA自动机变量集进行表示。

第二种，规则：TASM时间抽象状态机模型中的规则表示了变量之间的关系。由于扩展NTA自动机并不存在这样的规则，而是对于这种规则采用了状态迁移的这种表示，因此需要建立一种将TASM时间抽象状态机模型中的规则转换为扩展NTA自动机中相应状态迁移的映射方法。具体做法是，将TASM规则中的条件部分，转换为扩展NTA自动机中的卫士条件；将TASM规则中的条件满足后的执行部分，转换为扩展NTA自动机中的分派任务。

第三种，作用域：TASM时间抽象状态机模型是自动机的集合，在转换为NTA自动机时，将TASM时间抽象状态机集合按照元素的划分来划分转换后的扩展NTA自动机的作用域。

将以上三种情况编辑成的ATL转换规则，使用持久化技术存入数据库中。

（3）利用转换规则，实施TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换。

首先，输入TASM时间抽象状态机元模型所对应的源文件、TASM时间抽象状态机元模型、建立的从TASM时间抽象状态机模型源文件转换成扩展NTA自动机目标文件的ATL转换规则、扩展NTA自动机元模型；其次，使用ATL开发包中的ATL转换虚拟机实现扩展NTA自动机目标文件的生成；最后，将待转换的TASM时间抽象状态机元模型源文件与转换完成的扩展NTA自动机目标文件，使用持久化技术存入数据库中。

在上述技术方案中，步骤（2）中所述的创建TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换规则，具体步骤为：

步骤1，使用ATL集成开发环境提供的ATL规则编辑器，创建ATL模型转换中的TASM时间抽象状态机源模型的元模型与扩展NTA自动机目标模型的元模型之间的转换规则集，具体做法是，在Eclipse中建立ATL模型转换工程，并新建模型ATL转换规则文件，填写源模型与目标模型的信息，包括元模型名称与对应的元模型文件，ATL集成开发环境将自动生成ATL模型转换中所用到的配置文件；

步骤2，针对TASM时间抽象状态机构件中的变量创建转换规则，对于扩展NTA自动机中直接支持的那些变量类型，直接通过OCL语言创建对应的扩展NTA自动机变量，并将TASM时间抽象状态机构件中的变量值复制到转换后的扩展NTA自动机变量中，对于无法用单一变量表达的TASM时间抽象状态机中所定义的变量类型，使用扩展的NTA自动机中所提供的标准变量类型解释为变量集，并用OCL语言在扩展的NTA自动机文件中创建这样的变量集；

变量集生成的具体做法是：

步骤2.1，将TASM时间抽象状态机中的离散变量，映射到扩展NTA自动机的整形变量中；

步骤2.2，将TASM时间抽象状态机中的枚举型变量，映射到扩展NTA自动机的整数常数上；

步骤2.3，将TASM中的连续变量类型，根据用户可接受的误差范围（位数），通过采样的方式，将连续变量映射到一个整数集上，这个整数集上的最小值设为转换后的扩展NTA自动机的下边界，这个整数集的最大值则设为转换后的扩展NTA自动机的上边界；

步骤3，针对TASM时间抽象状态机构件中的作用域创建转换规则，将TASM时间抽象状态机中的一个自动机单元，使用OCL语法填充在扩展NTA自动机中的一个“<template>”标签中，并将该标签的属性“name”设置为唯一标识字段，当扩展NTA自动机的模板A中的状态迁移将要访问模板B中的变量时，对模板A中状态迁移语句中所有属于模板B中的变量标识符的最左边，加上模板B的标识符和下划线“_”，以避免标识符冲突造成的二义性或不一致性；

步骤4，针对TASM时间抽象状态机构件中的规则创建转换规则，将TASM时间抽象状态机中所定义的规则集中以条件语句出现的形式，解释为<卫士条件，分派任务>二元组；

步骤4.1，将原条件语句中的条件部分，使用扩展NTA自动机的语法转换为卫士条件，具体做法是：

（4.1.1）将TASM时间抽象状态机中的条件语句中的判断子句中的操作符，替换为扩展NTA自动机中的操作符；

（4.1.2）将TASM时间抽象状态机中的条件语句中的判断子句中的语句结构，替换为扩展NTA自动机中的语句结构；

（4.1.3）将TASM时间抽象状态机中的条件语句中的变量标识符，替换为扩展NTA自动机中的标识符，该标识符的访问名按照步骤3中所述方法处理；

（4.1.4）按照与TASM时间抽象状态机中用来表示自动机状态的枚举型用户定义变量对应的扩展NTA自动机变量的名称，创建名称相同的扩展NTA自动机的自动机状态，并将转换后的扩展NTA自动机中的卫士条件中操作这些自动机状态变量的语句全部删除；

步骤4.2，将原条件语句中的执行语句，使用扩展NTA自动机的语法转换为分派任务，具体做法是：

（4.2.1）将TASM时间抽象状态机中的条件满足后的执行语句中的判断子句中的操作符，替换为扩展NTA自动机中的操作符；

（4.2.2）将TASM时间抽象状态机中的条件满足后的执行语句中的判断子句中的语句结构，替换为扩展NTA自动机中的语句结构；

（4.2.3）将TASM时间抽象状态机中条件满足后的执行语句中的变量标识符，替换为扩展NTA自动机中的标识符，该标识符的访问名按照步骤3中所述方法处理；

（4.2.4）按照与TASM时间抽象状态机中用来表示自动机状态的枚举型用户定义变量对应的扩展NTA自动机变量的名称，创建名称相同的扩展NTA自动机的自动机状态，并将转换后的扩展NTA自动机中的卫士条件中操作这些自动机状态变量的语句全部删除；

步骤5，将步骤2、3和4中的创建的规则添加到ATL转换规则文件中；

步骤6，将编辑完成的ATL转换规则，使用持久化技术存入数据库中。

在上述技术方案中，按照步骤（3）中所述的方法实施TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换，具体步骤如下：

步骤1，将TASM时间抽象状态机源文件，使用持久化技术将aaxl模型文件储存在数据库中；

步骤2，使用数据库技术，将TASM时间抽象状态机源模型到扩展NTA自动机目标模型的ATL模型转换中所需要的TASM时间抽象状态机源文件、TASM时间抽象状态机元模型文件、扩展NTA自动机元模型文件从数据库中提取出来，并输入到ATL模型转换虚拟机中；使用ATL模型转换虚拟机将生成模型转换后的扩展的NTA自动机模型文件；

步骤3，使用持久化技术，将生成的扩展NTA自动机模型文件存入数据库中。

本发明方法与现有技术相比具有以下优点：其一，沿用标准化的TASM时间抽象状态机模型作为本发明的输入，用户可以沿用以前的开发流程以及习惯；其二，对TASM时间抽象状态机模型的验证与实时仿真功能进行了扩充，使得用户可以在模型开发的各个阶段对模型进行实时仿真与验证；最后，TASM时间抽象状态机模型在转换为扩展NTA自动机模型后，使得用户在无需投入更多资源开发的情况下，充分利用扩展NTA自动机模型所兼容的工具，获得更多功能。

附图说明

图1为本发明方法的整体框架示意图。

其中：持久化控制器，为使用持久化技术编写，用来将文件转储到持久化介质（数据库）或恢复到文件系统中的程序。

具体实施方式

下面结合附图和实施例对本发明作进一步的描述。

本实施例提供一种从TASM时间抽象状态机到扩展NTA自动机的转换方法，本具体实施方式各步骤中所涉及到的名词由表1所示。

表1.具体实施方式中所涉及到的名词表

名词缩写名词名词含义/名称WindowsWindows视窗操作系统EclipseEclipse一种Java集成开发环境MyEclipseMyEclipse一种Java集成开发环境OSATEOpen Source AADL Tool Environment开源AADL工具环境SDKSoftware Development Kit软件开发包EPackageEPackage一种Ecore模型所提供的顶层级类型Property窗口Property窗口用来编辑元模型属性的窗口

本实施例的具体实施步骤如下：

步骤1，搭建开发环境。

假设当前平台仅有操作系统，操作系统为Windows（如Windows7x），现建立满足本发明的开发环境。

步骤1.1，搭建Eclipse开发环境。

下载并安装任意兼容Eclipse的开发环境套件（如Eclipse的各实现版本、MyEclipse、OSATE等）。

步骤1.2，安装EMF框架开发包。

下载并安装Eclipse官方所提供的EclipseModelingFramework。

步骤1.3，安装ATL集成开发环境。

下载并安装EclipseMarketplace中的AtlasTransformationLanguageSDK开发包。

步骤1.4，安装测试用实验环境。

根据需要安装测试用实验环境，如可安装UPPAAL仿真验证工具作为测试用实验环境。

步骤2，建立基于TASM时间抽象状态机源模型结构和扩展NTA自动机目标模型结构的元模型。

步骤2.1，使用步骤1.2中的EMF框架所提供的编辑器，根据TASM时间抽象状态机的模型语法结构建立TASM时间抽象状态机的元模型；根据扩展NTA自动机模型结构，建立扩展NTA自动机元模型；具体实施如下：在本节步骤1.1中的Eclipse开发环境中，新建EclipseModelingFramework（EMF）中的EcoreModel，设置该模型的顶层组件为EPackage，并在此基础上依据TASM语法，建立满足TASM定义的Ecore模型的各子项，必要时可以通过Property窗口来编辑所建立TASM元模型的各种属性。

步骤2.2，将Ecore建模器所分别建立的TASM模型的元模型与NTA模型的元模型，使用持久化技术存入数据库中。

步骤3，创建TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换规则。

本步骤分为6个子步骤进行实施。

步骤3.1，使用本节步骤1.3中的ATL集成开发环境提供的ATL转换规则编辑器，创建ATL模型转换中的TASM时间抽象状态机源模型的元模型与扩展NTA自动机目标模型的元模型之间的转换规则集。具体做法是，在本节步骤1.1中的Eclipse中建立ATL模型转换工程，并新建模型ATL转换规则文件，填写源模型与目标模型的信息，包括元模型名称与对应的元模型文件，ATL集成开发环境将自动生成ATL模型转换中所用到的配置文件；

步骤3.2，针对TASM时间抽象状态机构件中的变量创建转换规则，对于扩展NTA自动机中直接支持的那些变量类型，直接通过OCL语言复制到转换后的扩展NTA自动机目标文件中，对于无法用单一变量表达的TASM时间抽象状态机中所定义的变量类型，使用扩展的NTA自动机中所提供的标准变量类型解释为变量集，并用OCL语言在扩展的NTA自动机文件中创建这样的变量集；

步骤3.3，针对TASM时间抽象状态机构件中的规则创建转换规则，将TASM时间抽象状态机中所定义的规则集中以条件语句出现的形式，解释为以<卫士条件，分派任务>的二元变量组。原条件语句中的条件使用扩展NTA自动机的语法转换为卫士条件；原条件语句中的执行部分则使用扩展NTA自动机的语法转换为分派任务。最后将这些变量组使用OCL语言填充到扩展的NTA自动机目标文件中。

步骤3.4，针对TASM时间抽象状态机构件中的作用域创建转换规则，将TASM时间抽象状态机中的一个自动机单元，使用OCL语法填充在扩展NTA自动机中的一个“<template>”标签中，并将该标签的属性“name”设置为唯一标识字段（如自动机名或校验码等）。

步骤3.5，将本节步骤3.2、3.3和3.4中的创建的转换规则添加到ATL转换规则文件中，将该规则用以下的模板表达。

--注：

--（1）上下文：ATL转换虚拟机在进行转换时驻留在改转换规则区域内的对象定义环境

--（2）附加的判定条件：用来从获取的上下文中筛选出特定上下文的过滤条件

--pathTASM=tasm对应的ecore文件

--pathNTA=扩展的NTA自动机对应的ecore文件

moduleTASM;

createOUT:NTAfromIN:TASM;

rule规则名称{

from

源文件的上下文:源模型对应的元模型中的构件(附加的判定条件)

using{

使用的额外变量

}

to目标上下文1:目标模型对应的元模型中的构件(

目标文件的上下文1<-源上下文的语义转换结果

目标文件的上下文1<-源上下文的语法转换结果

)

目标文件的上下文2,

目标文件的上下文n

}

}

步骤3.6，将编辑完成的ATL转换规则，使用持久化技术存入数据库中。

步骤4，利用转换规则，实施TASM时间抽象状态机源模型到扩展NTA自动机目标模型的转换。

步骤4.1，将提供的TASM时间抽象状态机源文件，使用持久化技术将aaxl模型文件储存在数据库中。

步骤4.2，首先，使用数据库技术，将TASM时间抽象状态机源模型到扩展NTA自动机目标模型的ATL模型转换中所需要的TASM时间抽象状态机源文件、TASM时间抽象状态机元模型文件、扩展NTA自动机元模型文件从数据库中提取出来，并输入到ATL模型转换虚拟机中；其次，使用ATL模型转换虚拟机将生成模型转换后的扩展的NTA自动机模型文件；

步骤4.3，使用持久化技术，将生成的扩展NTA自动机模型文件存入数据库中。