基于需求的形式化建模与验证方法研究

李 勇，曹子宁

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

基于需求的形式化建模与验证方法研究

李 勇，曹子宁

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

软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响。为了能够在早期发现错误，降低开发成本，精确、简明地验证和规范软件系统和性质，在模型的形式化开发方法和模型检测的自动验证技术的研究基础上，提出了一种基于需求的形式化建模与验证的框架。运用基于四变量模型的需求状态机语言RSML-e建立了形式化模型，并给出了形式化的转换规则，将RSML-e模型转换为模型检测器NuSMV的输入模型，并进行了检测，建立起了一套整体的形式化开发框架，并以航空电子系统特定实例进行了建模与验证。验证结果表明，已建航电系统模型的安全性和可靠性是有效的。

形式化方法;RSML-e;模型检测;NuSMV

0 引 言

随着软件系统日益增长的复杂性和系统集成的问题，潜在的错误不断增加并可能影响到系统的安全性和可靠性。传统的软件工程方法已经很难满足需求，迫切需要新的方法来设计开发安全性更高、开发成本更低的大型复杂系统。为了解决这些实际问题，形式化开发方法在系统开发过程中被广泛应用，通过给出需求描述严格的形式定义，设计可执行的原型系统，然后通过模型检测以及新兴的代码自动生成等形式化技术的运用，大大提升了系统的安全性和可靠性，同时也大大节省了时间和成本[1-2]。目前面向需求形式化方法的研究也是形式化方法研究的热点。文献[3]借鉴π演算的进程构造能力和类型系统表达能力，以π演算为需求建模语言，提出一种需求建模的形式化方法，给出构造功能行为交互系统的良类型性质。文献[4]提出了一种面向航天嵌入式系统的名为SPARDL的形式化建模方法，还设计了代码生成方法。文献[5]提出了一种基于UML-NuSMV需求建模方法，并用该方法对列控系统的安全性进行了分析。

在形式化方法研究的基础上，运用需求状态机语言RSML-e对系统进行形式化需求规约，创建系统的形式化模型，在建模过程中能够发现大量系统描述中的错误，而且能够作为与用户交互的实模型，并能够以仿真的形式向客户执行。但RSML-e不支持直接的模型检测[6]。

为此，将模型转换为以工具直接验证的形式化模型，选取已经十分成熟的NuSMV符号化模型检测工具，给出模型的形式化转换规则，将RSML-e的规格说明通过形式化转换规则换为NuSMV的输入模型，并规约航空电子系统的飞行导航系统的属性，用建立的基于需求的形式化建模与验证框架对其进行了实验验证。结果表明，已建系统模型的安全性和可靠性是有效的，为进一步开发可靠安全的系统奠定了基础。

1 背景简介

1.1 RSML-e

RSML(Request State Machine Language，需求状态机语言)是由加州大学的Nancy Leveson研究组开发的一种基于状态的描述语言，用于对过程控制系统的行为建模。在研究过程中，为了解决显式事件的依赖性引入的错误，美国的明尼苏达大学关键系统组开发了RSML-e(RSML没有显式事件)，消除了显式事件且是同步语言[7]。

和SCR方法类似，RSML-e也是基于四变量方法[8]的思想，是基于状态机的形式化建模语言。RSML-e语言易读易理解，能够让客户更多地参与到系统开发中，从而实现设计人员和客户之间对于需求描述的理解的一致性。RSML-e形式化地描述了系统的行为模型，能够方便地转换为定理自动证明和模型检测的输入形式，使模型可执行，通过模型检测和定理自动证明来保证系统行为的完备性和一致性，从而提升系统的安全性。基于这种需求描述的需求形式化分析方法，可以在需求阶段找出大量错误，大大减少后续排错的工作和时间消耗。

1.2 NuSMV

模型检测的基本思想将系统行为抽象为一个有限状态机M，系统约束规范使用时序逻辑公式F表示。状态迁移系统M是否具有所期望的性质，可以用公式Μ|=?F表示[9]。模型检测面临的一个重大问题是状态爆炸，为了解决该问题，引入二元决策图，以符号表示状态空间。虽然还是有状态空间的大小限制，但符号模型检测器可以比显式状态模型检测更大的状态空间。

CMU和IRST联合开发的符号模型检测工具NuSMV，用于检测有限状态系统是否满足CTL约束公式。NuSMV是一种开放的模型检测结构，它可以可靠地用于工业设计的验证，执行过程为用户将表示系统模型和约束规范的SMV程序作为输入，NuSMV自动检测约束规则在模型检测中是否成立，若成立则输出true，否则输出false，并给出反例。

NuSMV2扩展了以前版本的NuSMV几个新特性，尤其是与执行的可能性SAT-based有界模型检查,释放提供了一些新功能，许多错误修复和优化，大量不同的软件建筑和建筑系统，是NuSMV新模型检测算法和延伸技术，允许一个更强大的操作模型，可以生成平面模型对整个语言，同时也允许锥的影响减少。所给出的模型转换规则主要适用于最新版本的NuSMV工具[10]。

2 形式化建模与验证框架

首先给出需求模型、模型转换、模型检测的一般框架，如图1所示。

图1 形式化建模与验证框架

2.1 RSML-e模型

一个RSML-e描述由变量、状态、转移、功能函数、宏、常量和接口组成[11]。需求描述中的变量用于存储外部传感器的输入值，也用于暂存系统的输出值。RSML-e以分层的形式组织状态，其中状态转移由一个原状态，一个目的状态，一个触发事件，一个监督条件和一组动作事件组成，控制着一个状态到其他状态的转移。为了执行一次状态转移，当触发事件发生时监督条件同时为真。监督条件是在不同的状态和变量之间的一种谓词逻辑表达式。为了克服命题逻辑符号语言的复杂性问题，RSML-e使用析取范式(DNF)来表示，这种表格称为AND/OR表[12]。AND/OR表格的最左一列列出了逻辑短语。其他的列是这些逻辑短语的连接，并且列出了表达式的逻辑真值。规定只要有某一列的值为真，则整个表的值就为真。而每列的真值为真当且仅当此列的真值与它们所关联的逻辑短语的真值都一致。图2为ANDOR表等同于DNF范式(Condition1∧Condition2)，‘*’表示不关心条件的真假。

图2 RSML-e中的ANDOR

2.2 NuSMV的输入与输出

SMV程序由一个或多个模块构成，和C语言一样，其中一个模块必须称为main，模块可以声明变量并赋值，程序最后给出要验证的性质，用CTL公式描述。如下给出了一段NuSMV程序的示例，包括主模块和要验证的性质。

MODULE main

VAR

request：boolean;

status:{ready,busy}

ASSIGN

init(status):=ready ;

next(status):=

case

reuqest:busy;

1:{ready,busy};

esac;

CTLSPEC

AG(request->status=busy);

2.3 转换规则

2.3.1 类型和变量的转换

RSML-e不仅支持布尔型、枚举型、整型、实型等基本的数据类型，还支持用户自定义的类型，但NuSMV不支持用户自定义的类型，所以RSML-e中自定义的类型就要转换为枚举等基本数据类型[13]。RSML-e中的输入和状态变量转换为NuSMV时，用关键词VAR表示为：

VAR identifier_name:var_type;

2.3.2 宏的转换

RSML-e中的宏对应转换为NuSMV中的一个子模块，可以做一一对应的转换，RSML-e对应的参数应保持转换，在NuSMV的子模块添加参数，此外，子模块必须在主模块中添加声明。

2.3.3 相对时间概念

RSML-e中用PREV的前缀表示当前研究状态的前状态，但NuSMV中只有next关键字表示后状态，所以在做对应转换时应将带有PREV前缀的状态描述为NuSMV中的当前状态，而不带前缀的描述为NuSMV中的后状态，在后面的实例中加以说明。

3 ASW具体实例

结合飞机系统中的高度按钮(Altitude Switch，ASW)的实例来说明转换规则。ASW的主要功能为接收的输入有禁止设备启动信号，系统重置信号，以及飞机的实时飞行高度，并当飞机的飞行高度低于某个阈值时，ASW按钮控制相关设备(Device Of Interest,DOI)的启动与触发，如图3所示的实例框架。

图3 ASW抽象框架

针对ASW，运用RSML-e进行建模。其中变量声明部分应包括输入变量高度的数据变量、禁止信号的变量、重置信号的变量，以及ASW的状态变量，图4给出高度变量和ASW状态变量的RSML-e模型。

VARaltitude

Type:real

InitialValue:UNDEFINED

Classifiedas:MONITORED

状态变量ASW：

STATE_VARIABLEASW

Type:{OFF,ON}

InitialValue:OFF

Classifiedas:State

图4 高度变量和ASW状态变量的RSML-e模型

模型中宏的声明包括对禁止和重置两个信号定义两个宏，判断高度值是否低于指定阈值的宏，这里给出禁止信号的宏以及系统的输出ASW宏：

MACRO when_inhibit_Pressed

Condition:

When(inhibit=ON);

MACRO when_ASW_Power_ON

Condition:

When(ASW=ON);

模型建立完成，接下来将模型转换为NuSMV的输入模型，根据第2节的变量转换规则，对VAR关键字定义的变量可以转换为：

MODULE main

VAR

altitude：real;

VAR

ASW:{OFF,ON};

ASSIGN

init(ASW):=OFF;

next(ASW):=

case

!m_when_inhibit_Pressed.result() & !m_when_inhibit_Pressed.result() &

m_when_altitide_below():ON;

m_when_inhibit_Pressed.result()|m_when_inhibit_Pressed.result() |

m_when_altitide_below():OFF;

esac;

根据宏的形式化转换规则，宏when_inhibit_Pressed转换为：

MODULEwhen_inhibit_Pressed()

VAR

result:boolean;

ASSIGN

init(result):=FLASE;

next(result):=When(inhibit=ON);

MODULE main

m_when_inhibit_Pressed: when_inhibit_Pressed()//主模式中的声明部分

验证其安全性和可靠性属性，给出其要验证的CTL逻辑公式[14]，给出安全性和活性两个验证的示例：

CTLSPEC

AG((Inhibit=TRUE)->m_when_ASW_Power_ON.result=TRUE)

AG((Reset=TRUE)->m_when_ASW_Power_ON.result=FLASE)

用NuSMV工具验证得到的结果如下：

--specification AG((Inhibit=TRUE->m_when_ASW_Power_ON.result=TRUE) is true

--specification AG((Reset=TRUE)->m_when_ASW_Power_ON.result=FLASE) is true

模型检测器NuSMV对示例中两个逻辑公式验证结果返回为true，表明建立的RSML模型满足示例中的两个属性，否则会给出反例。后续可对更多的安全性和活性的属性进行验证。

4 结束语

将基于需求的形式化方法应用在航电领域，基于需求建模语言RSML-e对飞行导航系统进行建模，并用模型检测器NuSMV对其进行形式化的模型转换与验证。具体实例的运行结果表明，所建立的模型满足安全性和可靠性，能够满足航电的技术要求。后续研究可将需求建模、体系结构建模相结合，将形式化方法运用于系统开发的各个阶段，从而给出从需求到验证的一套完整的系统的形式化开发框架。

[1] 吕 毅.形式化方法介绍及其在工程中的应用[J].微电子学与计算机,2003,20(10):26-31.

[2] 张广泉.关于软件形式化方法[J].重庆师范学院学报:自然科学版,2002,19(2):1-4.

[3] 雷义伟,贲可荣,何智勇.自适应软件需求的形式化建模与验证[J].海军工程大学学报,2015,27(6):73-78.

[4] 顾 斌,董云卫,王 政.面向航天嵌入式软件的形式化建模方法[J].软件学报,2015,26(2):321-331.

[5] 周玉平.基于UML-NuSMV模型的列控系统需求阶段的安全分析[D].北京:北京交通大学,2015.

[6] Jordan H,Beecham S,Botterweck G.Modelling software engineering research with RSML[C]//Proceedings of the 18th international conference on evaluation and assessment in software engineering.[s.l.]:ACM,2014:1-10.

[7] Choi Y,Heimdahl M P E.Model checking RSML-e,requirements[C]//International symposium on high assurance systems engineering.[s.l.]:IEEE,2002:109-118.

[8] Miller S P,Tribble A C.Extending the four-variable model to bridge the system-software gap[C]//Digital avionics systems.[s.l.]:[s.n.],2001.

[9] 杨 军,葛海通,郑飞君,等.一种形式化验证方法:模型检验[J].浙江大学学报:理学版,2006,33(4):403-407.

[10] 吕 审.NuSMV模型检测的研究及应用[D].武汉:武汉理工大学,2011.

[11] Cavada R,Cimatti A.NuSMV 2.6 manual[M].[s.l.]:[s.n.],2010.

[12] Miller S,Tribble A,Whalen M,et al.Proving the shalls[J].International Journal on Software Tools for Technology Transfer,2006,8(4-5):303-319.

[13] Heimdahl M P E，Leveson N G，Reese J D.Experience from specifying the TCASⅡ requirements using RSML[C]//Digital avionics systems conference.[s.l.]:[s.n.],2005.

[14] 鲍秋霜,张晋津.直觉主义计算树逻辑中的安全性和活性[J].计算机科学与探索,2016,10(2):163-172.

Investigation on Formal Modeling and Verification Method Based on Specification

LI Yong,CAO Zi-ning

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

In the process of software development,the mistakes introduced in requirements phase have a more significant effect of the security and reliability than the phase of designing.In order to be able to detect the errors in the early phase of the software development and reduce development costs,and to describe the software system precisely and concisely,a formal modeling and verification framework has been proposed with the technology of automatic verification,in which the RSML-emodel has been used and then the formal transformation rules have been given.Based on these rules,the proposed model can be transformed into the input model of the NuSMV,which is performed in model checking of the system.The specific instances of avionics system have been employed to implement modeling test experiments for verification.The experimental results show that the security and reliability of the established avionics system have been verified to be effective.

formal method;RSML-e;model checking;NuSMV

2016-06-30

2016-10-13 网络出版时间：2017-04-28

国家“973”重点基础研究发展计划项目(2014CB744900);航空科学基金(20150652008)

李 勇(1990-)，男，硕士生，研究方向为形式化方法;曹子宁，教授，博士生导师，研究方向为形式化方法、人工智能。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170428.1702.034.html

TP31

A

1673-629X(2017)06-0007-04

10.3969/j.issn.1673-629X.2017.06.002