[發明專利]TASM2UPPAAL模型轉換方法

有效

• 申請號: 201210027759.X
• 申請日: 2012-02-08
• 公開（公告）號: CN102609260A
• 公開（公告）日: 2012-07-25
• 發明（設計）人: 胡凱;張騰;楊志斌;顧斌;蔣樹;姜泮昌
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 暫無信息
• 代理人: 暫無信息

1.一種模型轉換方法，用于將TASM模型轉換為UPPAAL模型，其特征在于：

使用KM3描述目標語言UPPAAL的元模型；

針對TASM模型的環境變量與抽象機，執行規則語法元素，使用環境變量的轉換方法和主抽象機與執行規則的轉換方法，將TASM模型轉換為UPPAAL模型。

2.根據權利要求1所述的模型轉換方法，其特征在于：所述UPPAAL的元模型包括：

(1)nta：

UPPAAL模型的根節點，下轄節點包括對UPPAAL模型定義的普通變量、時鐘變量及同步通信信道進行聲明的節點declaration，時間自動機模板集合的節點template，對時間自動機進行聲明及實例化的節點system；

(2)declaration：

nta的下轄節點，放置用戶定義的變量的聲明及初始化定義；

(3)template

nta的下轄節點，定義時間自動機模板，其下轄以下節點：

●name：時間自動機的名字；

●declaration：時間自動機局部變量，時鐘的聲明；

●Parameters：時間自動機的輸入參數，在實例化中使用；

●location：時間自動機中的位置，在位置上設置屬性：緊急urgent、不變量invariant；

●transition：各個位置之間的遷移，包括遷移的起始位置source和目的位置target，上面設置轉換條件guard，對變量的賦值update，時間自動機之間的同步sync；

●init：定義時間自動機的初始位置location；

(4)system：

nta的下轄節點，對UPPAAL模型的時間自動機模板進行聲明及實例化；

(5)Label：

在時間自動機的元模型定義中，時間自動機位置(1ocation)上的屬性以及狀態轉換(transition)上的條件(guard)、賦值(assignment)、同步(synchronization)都在元模型中的label節點中被描述。

3.根據權利要求1所述的模型轉換方法，其特征在于：將TASM的整型、布爾型以及用戶自定義類型的數據類型轉換為UPPAAL模型中的有界整型一種數據類型，包含以下規則：

整型變量映射為UPPAAL中的int，布爾類型的變量boolean{False，True}映射到UPPAAL中的類型為int[0，1]，即取值范圍為0或1的整型變量；擁有n個取值e1到en的用戶自定義變量User-defined?type{e1，e2，....en}被映射到UPPAAL中的類型為int[0，n-1]，即取值范圍為0到n-1的整型變量，其中e1被映射到0，en被映射到n-1。

4.根據權利要求1所述的模型轉換方法，其特征在于：所述主抽象機(main?machine)與執行規則的轉換方法包括以下規則：

主抽象機到UPPAAL時間自動機(automata)的轉換：每一個主抽象機對應UPPAAL中的一個時間自動機，為每一個時間自動機定義一個中心緊急位置(urgent?location)pivot以及時鐘變量c；

主抽象機規則的轉換方法：在時間自動機上為與其對應抽象機的每一條規則定義一個中間位置，時間將在中間位置上消耗時間直到進行狀態變遷，每一條規則的執行被映射為UPPAAL時間自動機中的兩個狀態變遷，其中，各種類型規則所對應的轉換方法為：

1)一般規則到UPPAAL的轉換

設一般規則為Ri＝<Gi，t，Ei>，其中，Gi為規則Ri的約束條件(guard)，t為Ri的執行時間，被表示為t＝[tmin，tmax]，tmin≤tmax，Ei為規則的執行動作，對此規則，定義中間位置Ri，定義從pivot到Ri的狀態變遷，約束條件為Gi，執行動作為重置時鐘，在位置Ri上定義時間不變量c＜＝tmax，定義從Ri到pivot的狀態變遷，約束條件定義為c＞＝tmin，執行動作為Ei；

2)帶有同步的一般規則到UPPAAL的轉換

設帶有同步的一般規則Ri＝<Gi，t，Ei>，其中，Gi為規則Ri的約束條件(guard)，t為Ri的執行時間，被表示為t＝[tmin，tmax]，tmin≤tmax，Ei為下列語句：Update；Syn；其中Update為除同步通信以外的動作語句集合；Syn語句為同步通信語句，發送同步信號為“chan！”，接收同步信號為“chan？”，此規則，定義中間位置Ri，定義從pivot到Ri的狀態變遷，約束條件為Gi，執行動作為重置時鐘，在位置Ri上定義時間不變量c＜＝tmax，定義緊急位置U，定義從Ri到U的狀態變遷，約束條件定義為c＞＝tmin，執行動作為Update，定義從位置U到pivot的狀態變遷，執行動作為Syn；

3)帶有t：＝next時間結構和else規則到UPPAAL的轉換設規則Re＝<Ge，t，Ee>，其中，Ge為空；t：＝next；Ee為規則Re的執行動作，對此規則，定義中間位置Re，定義從pivot到Re的狀態變遷，設抽象機的其它規則的約束條件G1到Gn，定義狀態變遷的約束條件為！(G1||G2...||Gn)，定義從Re到pivot的狀態變遷，約束條件是(G1||G2...||Gn)，執行動作為Ee，定義從Re到pivot狀態變遷上的緊急同步信道“cElse？”以及發送同步信號“cElse?！”的時間自動機；

4)帶有一般執行時間表示的else規則到UPPAAL的轉換設規則Re＝<Ge，t，Ee>，其中，Ge為空；t為Re的執行時間，被表示為t＝[tmin，tmax]，tmin≤tmax；Ee為規則Re的執行動作，對于此規則，定義中間位置Re，定義從pivot到Re的狀態變遷，設抽象機的其它規則的約束條件G1到Gn，定義狀態變遷的約束條件為！

(G1||G2...||Gn)，執行動作為重置時鐘，在Re上定義時間不變量c＜＝tmax，定義從Re到pivot的狀態變遷，約束條件是c＞＝tmin，執行動作為Ee；

5)帶有t：＝next時間結構的一般規則到UPPAAL的轉換設Ri＝<Gi，t，Ei>，其中，Gi為規則Ri的約束條件(guard)；t為Ri的執行施行時間被表示為t：＝next；Ei為規則Ri的執行動作，對于此規則，定義中間位置Ri，定義pivot到Ri的狀態變遷，約束條件是Gi，定義從Re到pivot的狀態變遷，約束條件是(G1||G2...||Gn)，執行動作為Ee，定義從Re到pivot狀態變遷上的緊急同步信道“urgent？”以及發送同步信號“urgent！”的時間自動機。