基于层次组合抽象的智能系统形式化验证*

周益龙 韩 斌

（江苏科技大学计算机学院 镇江 212001）

1 引言

智能系统是将信息技术和嵌入式技术融为一体，实现智能控制的系统。随着软硬件规模的不断扩大，系统呈现出高并发的特点，急需一种全面有效的方法保证系统的安全性。

与传统的仿真和测试技术相比，形式化方法基于严格的数学理论，能够准确地描述系统模型并进行验证，具有高可信度的特点。因此，形式化方法已经被大量运用于软硬件系统的设计与开发中。文献［1］中，张杰等利用结构建模法对硬件电路形式化建模，并通过定理证明完成了验证；文献［2］中，Jin Song Dong等利用形式化语言TCOZ，描述物联网系统中的传感器感知模式、通信行为以及实时约束，通过定理证明的方式完成了模型的手动检验；文献［3］中，Chen等针对无线传感网络和无线体域网络这两个新型网络，提出了对其安全协议形式化验证的方法；文献［4］中，Sanghyun Yoon等提出了一种用于混成系统的验证技术，实现了利用SpaceEx来验证ECML模型以及搭建了混成系统的验证平台；文献［5］中，闫培等针对生命攸关的智能居家护理系统，提出了形式化建模的框架，利用PAT平台对模型进行了验证，找到设计缺陷并进行了改进。

本文针对智能系统提出了一种形式化建模与验证的方法，旨在发现系统设计中的缺陷，并以能源共享系统为例对建模过程，最后通过实验证明了该方法的有效性。

2 形式化方法

形式化方法（FormalMethod）基于严格的数学理论，常被用于计算机软硬件系统的设计与验证，其严谨的特点能够有效保证系统的安全性、可靠性等。与传统的仿真和测试方法相比，形式化方法在减少人力和时间投入的同时，能够准确清晰地对系统进行描述和验证，因此，形式化方法已经在多个领域中得到了广泛的应用，特别是安全苛求的系统。

其中，形式化规约和形式化验证是形式化方法研究的两项重要内容，如图1所示。

图1 形式化方法研究内容

形式化规约过程中，系统模型规约可以表述为系统的行为建模，系统属性规约可以表述为对系统需要满足的性质建模。通过对系统进行形式化规约后，可以形式化地验证系统是否需满足相应的性质，其中，模型检测是检测有限状态系统是否满足期望性质的一项技术，检测过程完全自动且高效。基本方式是通过对系统状态空间的暴力搜索，来搜寻是否存在不符合性质的情况，若存在，将会给出对应的反例路径，通过反例对系统设计进行分析和修改。

3 层次组合抽象模型

3.1 层次K ripke结构

定义1（层次Kripke结构）层次的Kripke结构可以表示为一个五元组（S，S0，AP，R，L），其中：

1）S表示系统所有状态的有限集合；

2）S0∈S表示系统初始状态的集合；

3）AP表示原子命题的集合，主要包括了该状态下的系统发生的动作行为；

将能源共享系统划分为应用层、系统层以及设备层，从应用层由上而下构建各层的Kripke结构，结果可以用带标签的有向图来表示，分别如图2、图3、图4所示。

图2 应用层模型

图3 系统层模型

图4 设备层模型

其中，每个椭圆表示系统的一个状态，圈内的原子命题表示系统的行为，有向曲线表示系统状态的转移关系。

3.2 组合抽象模型

为了得到简洁的系统模型，需要利用各个层次之间的相互联系，按照正确的组合规则，将层次Kripke结构模型进行组合建模，现定义层次Kripke结构的组合方式如定义2所示。

图5 系统组合模型

组合层次Kripke结构模型后，得到的系统组合模型状态数量非常多，模型十分冗杂，其中包含了许多对验证系统性质并无影响的状态，以及一些具有相似行为、可以融合的状态。因此，需要对系统的组合模型进行进一步的抽象处理，以达到精简系统模型的效果。

4）Ra，在抽象状态之间重新定义的转移关系，满足与之分别对应，并使得成立；

5）La，抽象状态的标记函数。

在对系统组合模型进行抽象时，去除不影响验证性质的状态，将行为相似、位于同一动作序列且无分支的状态进行合并；去除抽象状态之内的转移关系，并在新的抽象状态之间建立新的转移关系；重新定义抽象状态的标记函数。最终得到系统的组合抽象模型，如图 6 所示。

图6 系统组合抽象模型

3.3 组合抽象验证策略

组合抽象模型的验证策略可以分为简单组合策略和假设/保证（A/G）组合策略，在能源共享系统中，每个层次模块之间存在着相互制约的关系，采用简单组合策略时会忽略模块之间的相互影响，与实际情况不符合，因此，本文采用A/G组合策略来对系统模型进行检测。

A/G组合策略的基本模式如式（1）所示，为验证M1和M2的并发组合系统M 满足性质α和β，需要验证M1在任意环境下，满足性质α；在满足性质α的环境下，验证M2满足性质β即可。

本文对能源共享系统进行验证时，采用线性时序逻辑对性质进行描述。对于给定的LTL公式φ和ψ，只需检测M1|=φ是否成立，就能很容易验证形如 ＜ture＞Ma＜α＞ 是否成立；而要验证形如＜α＞M2＜β＞是否成立，根据文献［6］中的定理，对于给定的LTL公式φ和ψ，如果φ和ψ中出现的所有原子命题都在M的原子命题集中，那么＜φ＞M2＜ψ＞成立当且仅当M2|=φ→ψ，得到LTL公式的验证形式如式（2）所示。

在验证组合抽象模型是否满足性质时，需要根据组合模型和抽象模型的原子命题集之间的抽象对应关系，将LTL性质公式中的相关状态子公式进行等价的替换，如式（3）所示：

其中，p是LTL公式φ的状态子公式，α表示抽象映射，α(p)表示对状态子公式 p进行抽象映射以达到等价替换的效果。

然后，结合A/G组合验证策略，分别验证各个子系统的抽象性质，从而推断层次组合抽象系统的整体性质，组合抽象验证策略如式（4）所示：

4 实验验证结果分析

实验采用CSP#语言对能源共享系统模型进行形式化规约，得到模型状态图如图7所示。

图7 系统层次组合抽象模型状态图

抽取系统的安全性和活性进行LTL断言设计，其中，系统安全性包括了无死锁性和无冲突性，系统活性包括了可用性和节能性（设备开启后最终会关闭），性质申明分别表述为

1）无死锁性。系统不会一直处于停滞或等待的状态，死锁起因大多是进程间的相互等待。

2）无冲突性。一位用户使用的设备数量总是小于2，一台设备的使用者数量总是小于2。

3）可用性。用户在成功登录后，总是能够正常地使用各项功能。

4）节能性。用户在使用的过程中，设备最终都需要被关闭。

用进程分析工具PAT完成模型的自动验证，能源共享系统的性质验证结果如表1所示。

表1 系统性质验证结果

分析PAT工具给出的反例路径可以发现，1）系统冲突性主要原因是：不同用户登录成功后，同时通过扫码或者输入编码的方式获取同一台设备的信息，此时，如果这些用户未租借其他设备，而此设备也空闲，满足租赁条件，那么这些用户能够同时发起开启设备的请求，引发冲突。解决方案：在用户扫码或者输入编码后查看设备信息的同时，系统对该设备进行锁定，如果用户一定时间内未进行相关操作，系统就解锁该设备。2）系统不满足节能性的主要原因是：用户在租借设备后，可能进行了诸多其他无关操作，从而忘记了关闭正在使用中的设备，导致设备无限长时间内一直处于使用中状态，造成能源浪费。解决方案：用户租用设备后，系统在界面醒目位置显示结束使用的功能，并在一定时间后提醒用户关闭设备，如果用户长时间未关闭设备，系统自动关闭设备，结束租用。

使用抽象模型、组合模型和层次组合抽象模型分别对能源共享系统进行建模，用PAT进行验证后得到系统状态数随用户数量变化的对比图，如图8所示。

图8 结果对比图

通过状态数的对比实验可以得出，层次组合抽象模型既能够有效减少系统模型中的状态基数，也能减缓系统状态数随系统并发量增长的速度，在一定程度上缓解了模型检测中的状态空间爆照问题，使得模型检测工作能够更加有效率地进行。

5 结语

本文结合了层次Kripke结构和组合抽象技术，提出了利用层次组合抽象模型对智能系统进行形式化验证的方法，通过实例验证，证明该方法能够准确找出系统设计缺陷，并能有效缓解状态空间爆炸问题，提高模型检测的效率。