Petri 網(wǎng)在STM32 主函數(shù)程序編寫方法中的應(yīng)用

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

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

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

1 基本概念

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

(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 網(wǎng)中一般用圓圈來表示；T元素代表變遷，在Petri 網(wǎng)中一般用方框表示；兩種元素中至少一個(gè)元素為非空集合.F為流關(guān)系，一般用箭頭表示，其只能連接不同類元素.

定義2[4]（變遷發(fā)生規(guī)則）令∑=(S,T;F,M) 為網(wǎng)系統(tǒng)，M是N=(S,T;F) 上的標(biāo)識(shí)，t∈T，則具有以下的變遷發(fā)生規(guī)則：（1）t在M有發(fā)生權(quán)的條件是?s∈S:s∈.t→M(s) ≥1，t在M有發(fā)生權(quán)的事實(shí)記作M[t＞.（2）若t在M有發(fā)生權(quán)，則在標(biāo)識(shí)M下，變遷t可以發(fā)生，從標(biāo)識(shí)M發(fā)生變遷t得到一個(gè)新的標(biāo)識(shí)M′（記為M[t＞M′），對(duì)?s∈S,

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

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

上述幾種關(guān)系構(gòu)成了網(wǎng)系統(tǒng)的行為輪廓，記作BP={ →,→-1,+,‖}

2 程序語句基本結(jié)構(gòu)的Petri 模型

（1）順序結(jié)構(gòu).順序結(jié)構(gòu)的程序語句Petri 網(wǎng)模型如圖1 所示，語句1，2，3 執(zhí)行順序?qū)?yīng)圖中的T0，T1，T2，庫所表示是否滿足程序語句的執(zhí)行條件，滿足則執(zhí)行，P0 與T0 執(zhí)行語句1，以此類推.

圖1 順序結(jié)構(gòu)的程序語句Petri 網(wǎng)模型

圖2 分支結(jié)構(gòu)的程序語句Petri 網(wǎng)模型

圖3 循環(huán)結(jié)構(gòu)的程序語句Petri 網(wǎng)模型

（2）分支結(jié)構(gòu). 分支結(jié)構(gòu)的程序語句Petri 網(wǎng)模型如2 所示，語句1，3 執(zhí)行順序?qū)?yīng)圖中的T0，T1，T3. 其中，T0 為判斷變遷，判斷程序語句的執(zhí)行分支. 若判斷變遷T0 確定執(zhí)行T1 表示的語句1，庫所P1 滿足執(zhí)行條件后，開始執(zhí)行程序語句1.

（3）循環(huán)結(jié)構(gòu). 循環(huán)結(jié)構(gòu)的程序語句Petri 網(wǎng)模型如3 所示，語句2 執(zhí)行順序?qū)?yīng)Petri 網(wǎng)模型圖中的T2 到T1，T2 表示的程序語句2 執(zhí)行完畢后，直接以庫所P1 為執(zhí)行條件，滿足條件，開始執(zhí)行T1，若不滿足跳出循環(huán)結(jié)構(gòu).

3 主函數(shù)程序編寫邏輯的Petri 模型

由于程序語句本身多樣復(fù)雜，且編寫時(shí)存在不同的結(jié)構(gòu)與嵌套關(guān)系，致使程序員，尤其針對(duì)編程語言初學(xué)者，在編寫STM32 主函數(shù)的程序時(shí)，不得不在編寫一段程序后，就需要編譯一次，再下載到單片機(jī)，查看是否能夠?qū)崿F(xiàn)預(yù)期功能.如果程序員將主函數(shù)中的所有程序全部編寫完畢后再編譯下載，除資深程序員外，出錯(cuò)機(jī)率高. 一旦出錯(cuò)，則需按照MDK5 編程工具報(bào)錯(cuò)之處，逐句改正，并且在改正時(shí)，往往會(huì)牽扯到程序的邏輯結(jié)構(gòu)，出現(xiàn)“牽一發(fā)而動(dòng)全身”現(xiàn)象.

本文利用Petri 網(wǎng)對(duì)STM32 的主函數(shù)程序編寫邏輯進(jìn)行建模. 此程序語句的Petri 網(wǎng)建模只針對(duì)STM32 單片機(jī)的主函數(shù)編程，以C 語言程序語句的邏輯結(jié)構(gòu)為切入點(diǎn)，建立Petri 網(wǎng)模型，程序語句邏輯結(jié)構(gòu)包括順序結(jié)構(gòu)、分支結(jié)構(gòu)和循環(huán)結(jié)構(gòu). 主函數(shù)程序編寫邏輯的Petri 網(wǎng)模型如圖4 所示.

圖4 主函數(shù)程序編寫邏輯的Petri 網(wǎng)模型

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

4 主函數(shù)程序編寫邏輯的Petri 網(wǎng)性能分析與驗(yàn)證

4.1 靜態(tài)性質(zhì)分析

主函數(shù)程序編寫邏輯的Petri 網(wǎng)的性能可用關(guān)聯(lián)矩陣A來分析其系統(tǒng)結(jié)構(gòu)，關(guān)聯(lián)矩陣的第i行j列的矩陣元素aij表示當(dāng)變遷Ti發(fā)生時(shí)，庫所Pi中消耗或產(chǎn)生n個(gè)托肯，其中n為負(fù)數(shù)時(shí)，表示消耗，反之表示產(chǎn)生.[7]

根據(jù)主函數(shù)的邏輯性編程的Petri 網(wǎng)的關(guān)聯(lián)矩陣A，可得到公式AY=θ的通解Y，即A的S_不變量：

由結(jié)果知：從庫所到變遷時(shí)消耗1 個(gè)托肯，從變遷到庫所時(shí)產(chǎn)生1 個(gè)托肯.Petri 網(wǎng)中每一個(gè)S_都覆蓋了一個(gè)庫所，每個(gè)庫所都會(huì)有托肯流過，S_不變量能夠反映托肯的流動(dòng)路徑，具有不變性，因此此Petri 網(wǎng)的流程和托肯的流動(dòng)路徑是固定的.所以主函數(shù)邏輯性編程的Petri 網(wǎng)靜態(tài)結(jié)構(gòu)是穩(wěn)定的.

4.2 動(dòng)態(tài)性質(zhì)分析

可達(dá)性是Petri 網(wǎng)最基本的動(dòng)態(tài)性質(zhì).[8]主函數(shù)程序編寫邏輯可達(dá)圖如圖5 所示，Mi代表可達(dá)狀態(tài)標(biāo)識(shí)集，可達(dá)標(biāo)識(shí)集中“1”表示庫所中有托肯，“0”表示無托肯，箭頭方向表示狀態(tài)轉(zhuǎn)移.由圖可知系統(tǒng)在運(yùn)行過程中可以達(dá)到指定的狀態(tài)，因此系統(tǒng)具有可達(dá)性.

圖5 主函數(shù)程序編寫邏輯可達(dá)圖

4.3 模型仿真檢驗(yàn)

為檢驗(yàn)Petri 網(wǎng)模型的正確性與可行性，用Petri 網(wǎng)分析軟件PIPE 繪制模型圖. 通過運(yùn)行State Space Analysis 函數(shù)，對(duì)模型進(jìn)行檢驗(yàn). 模型仿真檢驗(yàn)圖檢驗(yàn)輸出結(jié)果顯示，系統(tǒng)的安全性、死鎖性和有界性都是正確的，所以系統(tǒng)可以有效運(yùn)行，此模型正確并且可行.

5 結(jié) 語

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