基于NuSMV的SysML模型形式化验证

2019-10-11邓刘梦葛晓瑜宛伟健

计算机技术与发展 2019年10期

邓刘梦，葛晓瑜，宛伟健

(南京航空航天大学计算机科学与技术学院，江苏南京 211106)

0 引言

在过去多年，软件开发面临了多个挑战，新的需求和存在系统不断增长，系统也变得越来越复杂，以至于很难及时地对它们进行构建。为了解决这些问题，出现了很多新的方法，其中最突出的一个就是模型驱动开发。

模型驱动开发代表了一套理论和工业化软件开发的方法框架，在软件开发全生命周期中系统的使用模型作为主要工件，主要是为了解决软件的两个根本危机：复杂性和变更能力。但与此同时，模型驱动开发也带来了一些问题：使用自然语言描述的需求与严格定义的模型之间的鸿沟无法很好地连通[1]。此外，对于SysML描述的图形化模型，目前缺乏严格有效的分析和验证方法。

针对以上存在的问题，文中给出了从SysML模型到NuSMV输入模型的转换规则，并实现自动化程序完成这一转换。接着利用NuSMV模型检测的方法来验证SysML模型的正确性。

1 SysML系统建模

SysML是目前业界常用的系统体系结构建模语言，可用于由软硬件、数据和人综合而成的复杂系统的分析与设计。然而，为了保证一定的易读性，SysML采用半形式化的描述方法来定义语义，使用自然语言描述约束和详细语义，力求在形式严格和易于理解间找到平衡[2]。在实际中，其图形化的建模方式十分简洁直观，关系链接与约束描述等方式也进一步缩小了模型驱动开发过程中需求描述与模型设计制品间的沟壑。但是，其牺牲的部分就是缺乏精确的语义，难以进行严格的语义分析以及正确性验证。

SysML是一种图形化建模语言，是对象管理组织(object management group，OMG)在对UML2.0的子集进行重用和扩展的基础上提出的一种新建模语言[3]。它为软件体系结构建模提供了丰富的图标，涵盖了从系统需求到设计阶段的各项要求，广泛应用于航空航天软件开发过程。它致力于建模具有众多组件、难以描述、理解、预测、管理、设计以及更改的系统，并提供了表达个人需求及其组成的手段，已被学术界和工业界所广为接受，作为一种标准建模语言[4]。

SysML为系统的结构模型、行为模型、需求模型和参数模型定义了语义。结构模型强调系统的层次以及对象之间的相互连接关系，包括类和装配。行为模型强调系统中对象的行为，包括它们的活动、交互和状态历史[5]。

文中主要使用SysML的块定义图对系统的静态结构进行描述，使用状态机图对系统的动态迁移进行描述。SysML中，块(block)是系统描述的最小建模单位，可以用来描述每一个单独的组件，同时也是描述系统结构特征和行为特征的单元。SysML块以UML类图为基础，并扩展了UML复合结构的一些特征[6]。块定义图(block definition diagram)则是用于描述块信息的图。它描述了块的属性值、块的组成部分、块的操作以及对其他块的参考等[7]。而状态机图(state machine diagram)则是用来描述系统的状态迁移情况[8]。其中状态转移用来描述对象对事件的响应情况。关于SysML块定义图以及状态机图的实例将在下一节给出。

2 NuSMV模型

针对SysML模型进行验证，采用NuSMV作为验证工具。

2.1 输入语言分析

NuSMV模型中，系统被描述为模块化的层次结构，支持定义组件的重用[9]。其支持的数据类型主要有枚举类型、布尔类型和固定数组等。基本上，一个完整的NuSMV模型文件主要由两部分组成：系统模型和待验证的系统性质[10-11]。

NuSMV系统模型部分主要用于描述系统的状态以及状态迁移关系，刻画出系统的静态结构与动态行为[12]。通过关键字MODULE来定义模块，通常每一个模块对应一个系统组件[13]。通过主模块中的SPEC字段进行待验证需求性质描述，同时支持计算树逻辑(computation tree logic，CTL)和线性时序逻辑(linear-time temporal，LTL)的表达式[14-15]。

2.2 SysML模型到NuSMV模型的转换

本节根据SysML模型与NuSMV模型的特点[16]，给出转化规则，并实现工具完成NuSMV模型实例的自动化生成。

首先对SysML中的静态图进行转换，文中主要使用的是块定义图。

规则1：模块名声明。

描述：对于NuSMV中的模块名根据块定义图中的名称进行命名。

规则2：静态变量声明。

描述：对于块定义图中定义的属性都须在相应的模块中通过VAR关键字进行声明。

规则3：变量初值。

描述：对于块定义图中所有属性的初值都须在相应的模块中通过ASSIGN关键字进行声明。

接下来对SysML中的动态行为模型进行转换。SysML中主要通过状态机图对系统的状态迁移进行刻画，系统中可能出现的状态迁移，都存在对应的状态机图[12]。从另一个侧面来看，状态图也可以理解为对块定义图动态的补充，故在转换中，应将其放入相应的模块中，而不是重新声明模块。

规则4：状态机图声明。

描述：对于状态机图转换不重新进行模块声明，将其状态迁移关系通过TRANS、next等关键字描述加入到从属的块定义图对应的模块中。

例如：Car对应的状态机图，其描述的状态迁移关系都应该加入到MODULE car中。

规则5：状态变量声明。

描述：如果一个块定义图存在一个对应的状态机图，则应该在此块对应的模块中通过VAR声明一个state变量。

规则6：状态变量赋值。

描述：状态机图中state的取值是由去除初始状态和结束状态后所有状态值构成的枚举集合，其初始值应为状态机图中Initial节点指向的第一个状态，通过ASSGIN声明。

例如：对于汽车car，通过一个状态机图描述其运行状态可能存在运行或者停止两种状态(见图1)，那么MODULE car中VAR字段就需加入car_state:{stop，running}声明，初始状态为stop，通过ASSGIN init(car_state):=stop字段进行声明。

图1 汽车运行状态机图实例

规则7：状态迁移。

描述：状态机图确定的状态转变使用next进行描述，并通过case来表达分支情况。

例如：car_state当前状态为stop下一状态为running和当前状态为running下一状态为stop表示如下：

next(car_state):=

case

car_state=stop:{running};

car_state=running:{stop};

esac

规则8：状态迁移条件。

描述：如果状态机图中的状态迁移存在迁移条件，则需将该守卫条件加入到迁移描述字段中(见图2)。

例如：在汽车启动前应确定车门是关闭的，否则无法启动。

next(car_state):=

car_state=stop&door.closed=1:{running};

图2 存在守卫条件的状态迁移实例

3 实验与案例分析

根据前几节的理论分析，实现了一个SysML模型到NuSMV模型自动转换的工具。下面通过案例演示。

案例的场景如下：在铁路控制系统中，在火车通过路口时需要关闭公路两侧的栅栏，保证在火车通过的过程中汽车无法驶入路口，避免发生火车汽车相撞的事故。首先通过SysML建模工具建立该场景的模型如下：

图3 铁路案例SysML块定义图

图3中块定义图描述了系统的静态结构信息，图4中状态机图则描述了系统的状态以及迁移关系。

图4 铁路案例SysML状态机图

在建模分别得到块定义图和状态机图后，利用工具将模型导出为XMI文件格式以供后续转换使用。接着将得到的SysML模型文件输入到自动转换工具中即可完成转换，得到铁路系统的SMV文件(见图5)。

图5 SysML模型转换工具界面

得到设计模型的实例后，即可利用已有的NuSMV工具来检测系统需求是否被设计模型所实现。首先给出一条安全需求：该系统模型不得出现汽车和火车同时驶入路口的情况，避免事故发生。接着在得到的SMV文件中写入该需求性质LTL表达式：LTLSPEC G!((Car_state=Car_in) & (Train_state= Train_in))。最后在Windows10下采用命令行形式运行NuSMV工具检测该SMV文件得到的结果如图6所示。