本文根據最近整理的CPNtools論文和CPNtools官網上的說明，以及參照了烏克蘭敖德薩 ---國家電信研究院運輸和通信部關於 電信系統協議仿真關於CPNtools的學生講義。基於此和和自己的理解整理的關於CPNtools在協議建模狀態空間分析以及其他的一些特征。具體的介紹基於對CPNtools的工具的實際操作來說明。
因為CPNtools是丹麥奧爾胡斯大學（Aarhus University）大學團隊開發的軟件，所以在該學院的 Department of Computer Science 部門有很多相關使用該軟件做的工作。 學院官網地址：https://cs.au.dk/ 可以在搜索欄中檢索相關的CPNtools資料
因為考慮了一下寫的內容可能比較多，所以大體上分成幾個章節來寫。如果后續寫的太多，我會在每個博客做超鏈接到其他博客頁面。（這項工作我會分成大概一周時間完成）
因為CPNtools官網上的介紹沒有針對如何建模協議來講，而且手冊部分也很簡單對做協議分析內有什么大的幫助。所以綜合了很多材料，對CPNtool如何來建模協議模型想具體的寫點東西。算是對自己論文的一個輔助材料，凡做事必須講究認真。嚴謹的邏輯，不可捕風捉影，協議的形式化分析也必須是合乎規定，任何協議的形式化建模之前必須要根據協議組織的規范文檔來做。
第一部分：界面的功能組件的介紹
1.1 CPNtools的安裝
Windows安裝：在官網上 http://cpntools.org/ 上下載界面下載 基於Windows版本的最近版本 ，下載之后安裝即可
Linux 安裝：Linux安裝之后會出現調用公用庫的 libxml2.so.2 報錯的問題，提示報錯信息：: libxml2.so.2 cannot open shared object file: No such file or directory 解決問題的方法：使用 find 命令查詢是否存在該庫， 如果存在是否是對應軟件版本和系統版本的不匹配問題， 如果沒有下載安裝即可， 如果有但是關聯存在問題，使用 ln -sf 命令 對庫文件的地址執行關聯。 具體的執行步驟見圖
如果按照上面的操作還是提示不能讀取文件，提示下面的信息：
./cpntools: error while loading shared libraries: libxml2.so.2: cannot open shared object file: No such file or directory
- 、首先打開/etc/ld.so.conf文件
- 、加入動態庫文件所在的目錄：執行vi /etc/ld.so.conf，在"include ld.so.conf.d/*.conf"下方增加"/usr/local/lib"。(具體的看自己的文件庫位置)
- 、保存后，在命令行終端執行：/sbin/ldconfig -v；其作用是將文件/etc/ld.so.conf列出的路徑下的庫文件緩存到/etc/ld.so.cache以供使用，因此當安裝完一些庫文件，或者修改/etc/ld.so.conf增加了庫的新搜索路徑，需要運行一下ldconfig，使所有的庫文件都被緩存到文件/etc/ld.so.cache中，如果沒做，可能會找不到剛安裝的庫。 一般情況下可以解決共享庫不能加載的問題，但是有時候用戶還是提示不能加載庫，這個時候應該考慮是否是用戶自己添加的軟件或者自己生成的 .so動態庫沒有執行權限。
安裝完成之后操作的主界面如下。
1.1.1 我們先舉一個簡單的登錄協議的模型
setp 1 首先創建兩個庫所，分別表示 Send 和 Reciver ,在創建一個變遷表示 網絡 NET
接下來聲明顏色集合變量的類型，建模的簡單模型結構件下圖：
step2 這里注意，顏色集綁定的數值標記定義好之后，在變遷NEt中會自動出現，變遷的綁定初始值，這個時候我們需要點擊變遷的左下方的小三角，來選擇需要綁定的初始值，也就是將變遷使能。變遷使能綁定初始值見下圖，這里我么選擇綁定(n=1,p="one")
step3 在弧上寫上弧表達式， 我們定義了 var n=INT p=DATA ， 所以從 SEND---->Reciver 弧的表達式為 （n,p）, 這里 從變遷NET到 Reciver端我們 使用函數 來判斷發送的數據。
step4 ,現在我們來模擬數據從Send 發送到Reciver端，條件不符合的時候輸出 fail ,條件滿足的時候輸出 sucess
這里我們要注意的是幾點容易出錯的問題：
- 顏色集申明的時候 不能和 默認的（Standard declarations）中的申明重復
- 在標記顏色集的數值的時候，注意 1`(1,"shijian")++ 中的符號 ` 不是英文的分隔符 ’
- 變遷的初始值綁定是根據在於其輸出的庫所中的值決定的，但是需要自己手動來綁定
我本想這將主款工具界面操作部分漢化，但是官網上不發布 CPNtools的源代碼版本，只支持對托管源代碼的Subversion存儲庫開放。
1.1.2 tools BOX 的介紹
我從最常用的工具開始介紹：
Creat： 創建工具。 （功能介紹部分我全部放在圖像上面，這樣方便大家閱讀。）
菱形表示創建一個變遷， 橢圓表示創建一個庫所，單箭頭表示創建弧
1.2 Petri網--CPNtools 層級網絡介紹
CPNtools最近被Nokia 被用來模型驅動的新一代手機的開發， CPN建模工具提出了強大的Petri網建模工具，一個抽象對象可以使用層級網絡建模分析，簡單的（）
第二部分： 原理的介紹
第三部分：簡單協議的建模舉例
第四部分：協議建模分析
第五部分：協議狀態空間分析
第六部分：協議添加攻擊模型的分析
第七部分：
參考文獻：
[1] Simonsen K I F , Kristensen L M . Towards a CPN-based modelling approach for reconciling verification and implementation of protocol models.[C]// International Workshop on Model-based Methodologies for Pervasive & Embedded Software. Springer, Berlin, Heidelberg, 2012.
[2] Yiqin Lu, Fang Fang, Runqing Quan. A simulating model of NGN based on CPN tools[M]// Theoretical and Mathematical Foundations of Computer Science. 2011.
[3]D.A.Zaitsev, T.R.Shmeleva. Simulatiing of Telecommunication Systems with CPN Tools[M]// Affiliated on meeting of Communication Networks Department Transaction NO 4 of 10.11.2006.
[4] Wells L . Performance Analysis using CPN Tools[C]// Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, Pisa, Italy, October 11-13, 2006. DBLP, 2006.
[5]Kent Inge Fagerland Simonsen, Lars M. Kristensen, Ekkart Kindler. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification[M]. Springer Berlin Heidelberg, 2016.
[6]Kent Inge.Code Generation from Pragmatics Annotated Coloured Petri Nets Simonsen.[M]//
[7]https://www.cpntools.org
[8]Ole Martin Dahl. Using Colored Petri NEts in Penetration Testing