Petri 網在STM32 主函數程序編寫方法中的應用

孫 霞，繆玉婷，趙厚群，張坤乾，張 潔

（安徽理工大學 電氣與信息工程學院 ，安徽 淮南 232001）

主函數是STM32 單片機執行程序代碼真正實現功能的地方.復雜主函數程序編寫過程中，需要分段編寫并對其進行編譯，查看是否存在錯誤.[1]Petri 網可以通過圖形建模方式描述和分析復雜的工作流程[2]，提高程序編寫的效率和準確性.本文通過Petri 網建模，對STM32 在Keil5-MDK 環境下主函數邏輯性編程，實現程序編寫與運行的準確性與快速性，降低程序編寫出錯概率，提高效率.

1 基本概念

定義1[3]（流程模型）四元組N=(S,T;F,C) 滿足以下條件，則稱為有向網：

(1)S∪T≠?；(2)S∩T=?；(3)；(4) dom(F) ∪cod(F) =S∪T. 其中，dom(F)={x|?y:(x,y)∈F};cod(F)={y|?x:(x,y)∈F}.S元素代表庫所，在Petri 網中一般用圓圈來表示；T元素代表變遷，在Petri 網中一般用方框表示；兩種元素中至少一個元素為非空集合.F為流關系，一般用箭頭表示，其只能連接不同類元素.

定義2[4]（變遷發生規則）令∑=(S,T;F,M) 為網系統，M是N=(S,T;F) 上的標識，t∈T，則具有以下的變遷發生規則：（1）t在M有發生權的條件是?s∈S:s∈.t→M(s) ≥1，t在M有發生權的事實記作M[t＞.（2）若t在M有發生權，則在標識M下，變遷t可以發生，從標識M發生變遷t得到一個新的標識M′（記為M[t＞M′），對?s∈S,

定義3[5]（可達性）設∑=(S,T;F,M) 為一個網系統，如果存在t∈T, 使得M[t＞M′，則稱M′為從M直接可達的，如果存在變遷序列t1，t2，…,tk和標識序列M1，M2，…,Mk使得M[t1＞M1[t2＞M2…Mk-1[tk＞Mk，則稱Mk為從M可達的. 從M可達的一切標識的集合記為R(M).

定義4[6]（行為輪廓）設(N,M0)是一個網系統，初始標識為M0，對任給的變遷對(x,y)∈(T×T)滿足下列關系：（1）若x＞y 且y ≯x，則稱嚴格序關系，記作x →y；（2）若x ≯y 且y＞x，則稱嚴格逆序關系，記作x →-1y；（3）若x ≯y 且y ≯x，則稱排他關系，記作x+y；（4）若x＞y且y＞x，則稱交叉序關系，記作x‖y.

上述幾種關系構成了網系統的行為輪廓，記作BP={ →,→-1,+,‖}

2 程序語句基本結構的Petri 模型

（1）順序結構.順序結構的程序語句Petri 網模型如圖1 所示，語句1，2，3 執行順序對應圖中的T0，T1，T2，庫所表示是否滿足程序語句的執行條件，滿足則執行，P0 與T0 執行語句1，以此類推.

圖1 順序結構的程序語句Petri 網模型

圖2 分支結構的程序語句Petri 網模型

圖3 循環結構的程序語句Petri 網模型

（2）分支結構. 分支結構的程序語句Petri 網模型如2 所示，語句1，3 執行順序對應圖中的T0，T1，T3. 其中，T0 為判斷變遷，判斷程序語句的執行分支. 若判斷變遷T0 確定執行T1 表示的語句1，庫所P1 滿足執行條件后，開始執行程序語句1.

（3）循環結構. 循環結構的程序語句Petri 網模型如3 所示，語句2 執行順序對應Petri 網模型圖中的T2 到T1，T2 表示的程序語句2 執行完畢后，直接以庫所P1 為執行條件，滿足條件，開始執行T1，若不滿足跳出循環結構.

3 主函數程序編寫邏輯的Petri 模型

由于程序語句本身多樣復雜，且編寫時存在不同的結構與嵌套關系，致使程序員，尤其針對編程語言初學者，在編寫STM32 主函數的程序時，不得不在編寫一段程序后，就需要編譯一次，再下載到單片機，查看是否能夠實現預期功能.如果程序員將主函數中的所有程序全部編寫完畢后再編譯下載，除資深程序員外，出錯機率高. 一旦出錯，則需按照MDK5 編程工具報錯之處，逐句改正，并且在改正時，往往會牽扯到程序的邏輯結構，出現“牽一發而動全身”現象.

本文利用Petri 網對STM32 的主函數程序編寫邏輯進行建模. 此程序語句的Petri 網建模只針對STM32 單片機的主函數編程，以C 語言程序語句的邏輯結構為切入點，建立Petri 網模型，程序語句邏輯結構包括順序結構、分支結構和循環結構. 主函數程序編寫邏輯的Petri 網模型如圖4 所示.

圖4 主函數程序編寫邏輯的Petri 網模型

圖中庫所P0 中的托肯代表程序員，T0 到T6 為順序結構，程序員在編寫主函數前，首先需要調用頭文件包括傳感器、定時器、蜂鳴器等設備具有功能定義性質的源文件，并依次對溫濕度與光度的數值上限、蜂鳴器報警機制以及數據端口進行定義，編寫主程序.首先，對端口與外設進行初始化，接下來開始執行程序；T6，T7 和T24 為分支結構，T6 為判斷變遷，判斷程序語句的執行分支，若判斷變遷T6 確定執行T7 分支，則T7，T8，T9 發生，編寫程序采集并讀取溫濕度信息且將數據通過串口輸出在OLED 屏.T10，T11，T23；T11，T12，T18；T13，T14，T17 和T29，T20，T22 同樣為分支結構，T16 到T6 為循環結構，T7 到T9 程序編寫結束后，程序員再編寫T10，判斷溫濕度是否超過上限值，若超過上限值，再判斷是過溫還是過濕，若過溫，則編寫T13，增加一次報警次數，當報警次數達到3 次時編程T15，T16，開始報警，報警結束之后延時一段時間繼續循環執行程序，否則直接延時后繼續循環執行程序，過濕程序的編寫方法依此類推；若溫濕度不超過上限值，則直接延時一段時間后繼續開始循環機制；編寫的T24 支路程序語句編寫步驟與T7 支路相同.

4 主函數程序編寫邏輯的Petri 網性能分析與驗證

4.1 靜態性質分析

主函數程序編寫邏輯的Petri 網的性能可用關聯矩陣A來分析其系統結構，關聯矩陣的第i行j列的矩陣元素aij表示當變遷Ti發生時，庫所Pi中消耗或產生n個托肯，其中n為負數時，表示消耗，反之表示產生.[7]

根據主函數的邏輯性編程的Petri 網的關聯矩陣A，可得到公式AY=θ的通解Y，即A的S_不變量：

由結果知：從庫所到變遷時消耗1 個托肯，從變遷到庫所時產生1 個托肯.Petri 網中每一個S_都覆蓋了一個庫所，每個庫所都會有托肯流過，S_不變量能夠反映托肯的流動路徑，具有不變性，因此此Petri 網的流程和托肯的流動路徑是固定的.所以主函數邏輯性編程的Petri 網靜態結構是穩定的.

4.2 動態性質分析

可達性是Petri 網最基本的動態性質.[8]主函數程序編寫邏輯可達圖如圖5 所示，Mi代表可達狀態標識集，可達標識集中“1”表示庫所中有托肯，“0”表示無托肯，箭頭方向表示狀態轉移.由圖可知系統在運行過程中可以達到指定的狀態，因此系統具有可達性.

圖5 主函數程序編寫邏輯可達圖

4.3 模型仿真檢驗

為檢驗Petri 網模型的正確性與可行性，用Petri 網分析軟件PIPE 繪制模型圖. 通過運行State Space Analysis 函數，對模型進行檢驗. 模型仿真檢驗圖檢驗輸出結果顯示，系統的安全性、死鎖性和有界性都是正確的，所以系統可以有效運行，此模型正確并且可行.

5 結 語

本文對主函數程序編寫步驟進行Petri 網建模，分析主函數編寫的流程，用PIPE 軟件進行檢驗，證明其正確性與合理性. 本方法對簡單的主函數的編寫作用不明顯，但對于外設多，須添加連接云平臺，同時實現數據采集、設備控制、云平臺信息指令上傳下行的主函數，具有更好的效果.