彭展

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

0 引言

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

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

1 智能油庫管理系統(tǒng)的架構(gòu)及功能

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

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

圖1 智能油庫管理系統(tǒng)的主要功能模塊

2 形式化方法及其應用

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

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

3 智能油庫管理系統(tǒng)的形式化分析

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

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

圖2 形式化方法在智能油庫管理系統(tǒng)開發(fā)過程的應用

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

表1 形式化方法與傳統(tǒng)方法的對比

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

4 結(jié)語

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

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

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

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

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

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