智能油库管理系统的形式化分析研究

彭展

（广东石油化工学院实验教学部，茂名 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.