彭展

（廣東石油化工學(xué)院實(shí)驗(yàn)教學(xué)部，茂名 525000）

0 引言

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

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

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

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

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

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

2 形式化方法及其應(yīng)用

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

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

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

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

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

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

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

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

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

4 結(jié)語

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

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

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

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

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

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