嵌入式控制軟件的形式化規(guī)格說明構(gòu)建的工程方法

在當前的工業(yè)界嵌入式控制軟件開發(fā)領(lǐng)域，形式化方法的實際應(yīng)用仍面臨許多現(xiàn)實困難。從軟件需求分析角度看，存在如下主要問題：1)缺乏面向領(lǐng)域的合適的形式化建模語言。2)缺乏系統(tǒng)化的形式化規(guī)格說明構(gòu)建的工程方法。3) 形式化規(guī)格說明有效性(validity)檢測手段不完善,效率低，缺乏實用的手段。 面對這一挑戰(zhàn)，我們提出一種構(gòu)造嵌入式控制軟件形式規(guī)格說明的形式工程方法。受國家自然科學(xué)基金青年基金資助，課題執(zhí)行期間取得了如下研究成果：1）提出了一種面向嵌入式控制軟件需求建模的輕量級形式化建模語言；2）結(jié)合形式化工程方法，建立了一種演化式的形式化模型構(gòu)建方法，提高了形式化建模過程的效率；3）提出了一種基于圖形的需求審查方法，有效地提升了需求審查的錯誤探測能力；4）提出了一種基于場景的需求模型測試方法，支持在需求分析階段即可進行仿真分析；5）研發(fā)了面向軌道交通車輛控制軟件的需求建模工具，使得該方法在企業(yè)獲得直接應(yīng)用，顯示了該方法具有明確的工程應(yīng)用價值。

針對形式化方法在工業(yè)界嵌入式控制軟件開發(fā)過程中難以有效應(yīng)用的問題，本課題主要研究嵌入式控制軟件的形式化規(guī)格說明構(gòu)建工程方法，建立工程化形式化規(guī)格說明構(gòu)建過程，并通過規(guī)格說明審查和測試保障規(guī)格說明的一致性和有效性。主要研究內(nèi)容包括：為嵌入式控制軟件形式化規(guī)格說明語言SPARDL提供與形式化語義一致的圖形化描述；建立圖形化描述引導(dǎo)的形式化規(guī)格說明工程化構(gòu)建過程，引導(dǎo)開發(fā)者從原始需求出發(fā)通過不同階段構(gòu)建形式化規(guī)格說明；研究規(guī)格說明審查以保證規(guī)格說明的一致性；研究規(guī)格說明測試技術(shù)以保證規(guī)格說明的有效性。研究測試用例生成、測試過程動畫模擬及測試結(jié)果分析等方法；開發(fā)相應(yīng)的軟件工具。課題將豐富當前的形式化建模理論與方法，為工業(yè)界嵌入式控制軟件的開發(fā)者提供有效而實用的形式化規(guī)格說明構(gòu)建工程方法。該課題對提高嵌入式控制軟件的質(zhì)量有重要意義，研究成果可有效推動形式化方法在工業(yè)界嵌入式控制軟件開發(fā)中的實際應(yīng)用。

從建筑設(shè)計到建成過程中，既符合力學(xué)規(guī)律，又遵循結(jié)構(gòu)特征；同時也符合從藝術(shù)審美角度去審視其自身所應(yīng)具有的美學(xué)法則；加之能在建造實施過程中保持其以上特征的過程。

建構(gòu)包括設(shè)計、構(gòu)建、建造等內(nèi)容，是一個三位一體的集合，是一個全過程的綜合反映。2100433B

工業(yè)控制系統(tǒng)作為國計民生關(guān)鍵設(shè)施自動化生產(chǎn)的基礎(chǔ)組件，是國家安全戰(zhàn)略的重要組成部分。隨著工業(yè)4.0、互聯(lián)網(wǎng) 時代的到來，工控系統(tǒng)與外界網(wǎng)絡(luò)環(huán)境的交互越來越密切，系統(tǒng)體系架構(gòu)也越來越復(fù)雜，工控系統(tǒng)的安全性與智能化程度都亟需提高，這給安全關(guān)鍵工控系統(tǒng)軟件的發(fā)展帶來了新的挑戰(zhàn)。本項目針對工控系統(tǒng)軟件高安全性的要求，運用嚴格的形式化方法對具備典型特征的工控系統(tǒng)軟件進行建模。研究形式化建模語言及其語義模型，設(shè)計適用于多物理設(shè)備資源的工控程序代數(shù)演算規(guī)則，完成軟件模型的分解與轉(zhuǎn)換，保證工控系統(tǒng)軟件的安全性和可靠性，從而形成面向多物理設(shè)備資源的工控程序開發(fā)理論與方法。該開發(fā)方法全程由形式化方法作為技術(shù)支撐，不僅提高了開發(fā)效率而且保證了軟件質(zhì)量，對工控系統(tǒng)的發(fā)展具備重要的意義。

(1)多功能模塊處理：在一個復(fù)雜的具有多臺變壓器的變電站里，每臺主變壓器和每一段母線都可能獨立運行，也可能并列運行。因此VQC的調(diào)節(jié)與控制應(yīng)能適用各種運行方式下的調(diào)節(jié)。

(2)電壓與無功的上下限值動態(tài)變化：對應(yīng)于不同的高峰和低谷時段，電壓與無功的上下限值應(yīng)不同，以適應(yīng)逆調(diào)壓和無功功率調(diào)節(jié)的要求。

(3)調(diào)節(jié)方式的多樣性：由于變電站中有時變壓器或電容器組需要停運檢修，因此考慮VQC調(diào)節(jié)時，調(diào)節(jié)方式應(yīng)設(shè)置“只調(diào)電壓”或“只調(diào)電容器”。對于控制策略中出現(xiàn)的矛盾，應(yīng)能“智能”變化。例如有時電容器組已經(jīng)全部投入或退出運行，這時已無電容器可調(diào)，應(yīng)能“智能”地改為有載分接頭的相應(yīng)調(diào)節(jié)。軟件VQC還應(yīng)設(shè)置“只監(jiān)視不控制”方式，以適應(yīng)運行需要，它相當于只投入運行不投連接片的保護運行方式。

(4)實現(xiàn)遠方控制VQC：就地VQC應(yīng)能接受調(diào)度端的控制，實現(xiàn)投退某個電容器組或有載調(diào)節(jié)變壓器的分接頭。

(5)閉鎖條件有如下幾條：

1)保護閉鎖。在對變壓器有載調(diào)壓分接頭開關(guān)和電容器組監(jiān)視控制過程中，如監(jiān)測到系統(tǒng)及變壓器、母線、電容器發(fā)生故障和異常的保護信號，應(yīng)立即閉鎖VQC的調(diào)節(jié)。

2)遙測閉鎖。當遙測值超過VQC要求的范圍時，閉鎖VQC。

3)遙信閉鎖。當變電站主接線運行方式改變時，閉鎖VQC。

4)其他閉鎖。VQC的TV斷線，主變壓器調(diào)壓控制器、電容器組的控制回路斷線或異常時，閉鎖VQC。

(6)相關(guān)信號上送調(diào)度：軟件VQC應(yīng)適應(yīng)無人值班變電站的需要，把一些必要的信號，如VQC調(diào)節(jié)閉鎖、調(diào)節(jié)拒動、調(diào)節(jié)動作信號上送調(diào)度端以便于遠方管理。

(7)并列運行、拒動、滑檔等：在變壓器并列運行時，VQC應(yīng)使并列的變壓器有載分接頭開關(guān)同步操作。母線并列時對應(yīng)的軟件模塊也應(yīng)做并列的相應(yīng)處理。主變壓器有載分接頭開關(guān)拒動、滑檔時應(yīng)立即停止調(diào)節(jié)并發(fā)出拒動和滑檔的信號上送調(diào)度，多次拒動、滑檔時應(yīng)閉鎖相應(yīng)操作。

(8)登錄操作：每一次調(diào)節(jié)都應(yīng)有相應(yīng)的記錄，包括對象、動作類型、時間、調(diào)節(jié)結(jié)果等。