智能油庫管理系統的形式化分析研究

彭展

（廣東石油化工學院實驗教學部，茂名 525000）

0 引言

油庫作為存儲石油資源的主要場所，為提高油庫的管理效率，該領域很早就進行信息化建設，但早期建設的信息系統往往功能較為單一，自動化程度較低，系統功能也不夠完善。在國家大力號召和鼓勵石化行業進行技術創新的背景下，市場對石化行業的管理效率有了新的要求，油庫管理系統不斷向著綜合性強、自動化程度高的方向發展，從而演化為智能油庫管理系統。但是系統功能的不斷增加，智能化程度的不斷提高，軟件系統的規模和復雜度也急劇增加，新的系統缺陷和錯誤也不斷出現，甚至會出現軟件危機。同時，石油作為易燃易爆物品，對油庫存儲狀況和安全監控顯得尤其重要，管理系統的缺陷容易帶來嚴重的后果，如何開發高質量的智能油庫管理系統顯得尤為重要。

本文提出把軟件開發形式化方法應用到智能油庫管理系統的開發過程，用形式化語言對智能油庫管理系統進行描述，接著進行形式化分析和驗證，以期減少軟件缺陷，提高系統開發質量，在提高油庫的運營管理效率的同時也保障好油庫的安全。本文首先是智能油庫管理系統的架構和功能描述，接著是軟件開發形式化方法的介紹，然后是智能油庫管理系統的形式化分析與驗證方案，最后是結束語。

1 智能油庫管理系統的架構及功能

最初的油庫信息系統都是功能較為單一的自動化系統，如自動發油控制系統，隨著業務的需要，在這基礎上逐漸增加了儲油罐液位自動計量系統、油庫安防監控系統等，這些系統在大大提高了油庫的工作效率，和油庫的安全性，提高了經濟效益。隨著這些系統的增加，陸續也暴露出不少問題，由于這些單獨的系統一般都是由不同的承包商開發，開發運行時間不一致，導致數據格式、系統接口等差異性較大，各個系統相互間不能進行交互和數據共享。不同設備和系統之間的信息沒有整合，就難以對油庫進行有效的分析和為管理人員的決策提供數據支持[1]。因次要整合油庫區域的設備和需求，建立統一的智能油庫管理系統，對油庫進行智能化綜合管理，智能油庫管理系統利用大數據建模和分析技術，對庫區各種類型數據進行統一采集、處理、分析等，實現油庫的作業處理、庫區運營監控、信息處理、安全預警等業務的一體化和自動化，以提高業務效率，降低油庫管理運營成本。

智能油庫管理系統根據油庫的實際情況和需求進行建設，一般情況下主要架構包括三大子系統：油庫作業自動化子系統、安全監控及報警子系統和綜合信息處理子系統。油庫作業自動化子系統是智能油庫管理系統最基礎也是最重要的功能，包括自動收發油功能模塊和罐區液位計量模塊。自動收發油功能是指利用自動化技術，幫助進入油庫區域的運輸車輛完成收油或者發油任務；罐區液位計量是通過液位計等完成石油液位計量任務。安全監控及報警子系統主要完成油庫區域的設備、環境、出入車輛和人員等進行監控，必要時進行報警提醒，主要包括消防報警模塊、設備及管道監控模塊、油庫周界監控模塊、門禁監控模塊和油氣濃度監控模塊。綜合信息處理子系統主要對油庫區域產生的各種數據進行記錄、處理和分析，在準確記錄庫區各種數據的同時，也能對數據進行分析和挖掘等，以提煉出用戶需要的、有價值的信息，主要包括收發油記錄與數據分析模塊和油罐儲量記錄與分析模塊。

圖1 智能油庫管理系統的主要功能模塊

2 形式化方法及其應用

軟件形式化方法是指建立在嚴格的數學模型上，具有精確數學語義的軟件系統開發方法[2]。形式化方法能夠有效地提高軟件開發質量。形式化方法的使用主要由形式化規格說明和形式化驗證兩大部分組成。形式化規格說明是根據系統的需求用形式化方法或規格說明語言對系統進行描述，建立系統的形式化規格；形式化驗證是在指對建立的形式化規格進行正確性驗證。典型的形式化方法和規格說明語言包括B方法、Z、Object-Z、LOTOS語言等。Z語言采用了集合、序列、包、關系、函數、類型、對象等抽象的數學理論，是一種數學語言[3]。Z語言的使用方法包含Z形式化規格說明和Z形式化驗證兩部分，先開發出系統的Z形式化規格，再進行正確性驗證。

形式化方法正在走向工業界，很多知名的科技企業均引入形式化方法進行研究和應用[4]。在很多關鍵的、對軟件質量要求高的領域，如電信服務系統領域[5],引入軟件開發形式化方法，把形式化方法應用到軟件開發過程，將能夠大大提高軟件開發質量，同時也降低開發成本。

3 智能油庫管理系統的形式化分析

智能油庫管理系統的規模龐大，功能模塊之間交互較多，復雜度大，在后期系統的使用過程中隨著實際的需要，系統功能可能還會繼續增加。由于油庫管理系統對質量性和可靠性要求極高，石油屬于易燃易爆危險品，智能油庫管理如果產生錯誤，既會損害經濟效益，還會帶來安全隱患，甚至生產事故。因此在智能油庫開發的過程中可以進行形式化分析及形式化驗證，把形式化方法貫穿到整個開發過程，具體步驟如下：（1）首先對智能油庫管理系統進行充分的需求分析；（2）對智能油庫管理系統進行詳細設計；（3）用形式化規格語言Z、Object-Z、LOTOS等開發出系統各個功能模塊的形式化規格并修改；（4）用相應語言的驗證工具或方法對形式化規格進行驗證，若驗證通過，則轉到步驟（5），否則返回步驟（3）繼續修改；（5）在正確嚴謹的智能油庫管理系統形式化規格的基礎上進行形式化方法和算法分析，找出功能模塊之間的故障或缺陷；（6）對缺陷進行修改并驗證正確性；（7）依靠形式化規格進行智能油庫管理系統的代碼編寫工作。（8）依靠形式化規格進行智能油庫管理系統的代碼測試工作。形式化方法在智能油庫管理系統開發過程的應用如圖2所示。

從圖2中可以清楚看到，形式化開發方法比起傳統方法主要增加了步驟（3）、（4）、（5）、（6），這 4個步驟是智能油庫管理系統的形式化分析及驗證的關鍵步驟。在傳統的開發過程中，從詳細設計到代碼編寫，程序員需要一個很大的跨越，往往程序員還不是很清楚每個功能模塊的細節，系統中存在歧義和不確切的地方在哪里，甚至功能模塊中可能會產生沖突，在這些情況還沒有確切認識的情況下就開始編寫代碼，容易造成代碼的質量不高，潛在隱蔽的錯誤，當發生錯誤或缺陷后再回來修改代碼，往往需要付出巨大的代價甚至還會產生新的錯誤和缺陷。

圖2 形式化方法在智能油庫管理系統開發過程的應用

在圖2中，智能油庫管理系統形式化分析的4個步驟具體作用如下：步驟（3）用形式化規格語言開發系統的形式化規格，就是用精確數學語義的表達方法對系統進行建模，讓程序員確切認識系統中每個將要實現的細節，這些細節如何定義，如何實現，這些均需要進行準確的描述；步驟（4）中的驗證，讓程序員掌握自己的定義和實現過程是否嚴密、正確，如果不正確，需要返回步驟（3）繼續完善；步驟（5）是用算法分析，找出系統功能與功能之間的錯誤，由于某些功能單獨運行是正確的，但多個功能同時運行的時候，就容易產生沖突，因此需要在編寫代碼之初就能夠挖掘出來；步驟（6）是對步驟（5）功能模塊之間的缺陷進行修改并驗證。因此我們可以知道運用形式化開發方法與傳統方法，最大的區別在于在詳細設計與代碼編寫之間，形式化開發方法有形式化分析的過程，而傳統開發方法沒有這個過程。具體如表1所示。

表1 形式化方法與傳統方法的對比

智能油庫管理系統的代碼規模龐大，功能模塊之間交互頻繁，可能出現的錯誤和缺陷數量大。如果軟件開發人員在詳細設計后直接進行代碼編寫，則容易產生較多的錯誤，并讓系統隱藏較多的缺陷，影響系統的正常運行，甚至造成安全事故。相比于傳統開發方法，形式化分析與驗證過程在正式的代碼編寫之前進行，經過一個完整的形式化分析過程，可以充分對系統進行嚴密、正確的描述，再在這個基礎上編寫代碼，可以大大減少錯誤的產生，減少代碼返工和錯誤修改的情況出現，提高智能油庫管理系統的開發質量。

4 結語

在國內外軟件工程領域，軟件開發形式化應用到大型復雜軟件系統的開發過程已有一定的案例，本文提出把形式化方法應用到智能油庫管理系統的開發過程，用形式化方法對系統進行分析和驗證，以期減少系統錯誤的產生，提高系統開發質量，對提高我國石油行業信息化建設水平具有積極的推動作用。

[1]曹巍,劉亞儒,侯巖松,喬學軍.數字化油庫綜合信息管理系統方案[J].信息系統工程，2017，7:117-118.

[2]鄭宇軍，張蓓，薛錦云.軟件形式化開發關鍵部件選取的水波優化方法[J].軟件學報，2016，27（4）：933-942.

[3]趙正旭,溫晉杰，趙衛華.Z規格說明自動生成器[J].計算機系統應用，2016，25（4）:148-155.

[4]陳鋼，于林宇，裘宗燕，王穎.基于邏輯的形式化驗證方法:進展及應用[J].北京大學學報(自然科學版)，2016，52（2）:363-373.

[5]彭展，梁根，周炳.電信服務系統特征交互的Z規格及驗證[J].計算機工程，2016，42（8）:19-23.