网络系统实时性模型的验证方法综述

杜泽民 王晓玲 陈宜成

摘 要：互联网技术的发展和应用在各个生产领域中发挥着越来越积极的作用，但随着网络技术应用的深入，网络系统的实时性成为影响网络安全的一大因素，因此对网络模型的通信实时性、威胁分析实时性的验证成为网络安全的重要保障。目前，国内外在实时性验证方面有诸多研究，形成了不同的方法体系。文章把主要的模型实时性验证方法，从理论和工具角度加以介绍分析，并对各个方法进行了比较。

关键词：网络安全；实时性；模型验证；实时性验证

中图分类号：TP393.0 文献标识码：A

1 引言

在互联网时代，网络安全问题是互联网建设的重要议题，而网络系统的实时性是网络安全的重要保证[1]。其中，包括通信的实时性以及威胁分析的实时性等。当网络受到外界攻击时，系统应该对相应的问题快速做出反应并处理措施。问题处理完毕后，还应将处理结果在规定的时间内反馈给系统。实时网络系统的每一个运行过程都是为了能够保证整个网络系统各项工作的协调进行。

模型驱动方法面对复杂度、集成性更高的大型系统有着安全性高、开发成本低等优势。当前的航空、航天控制系统、军事指挥自动化系统，也逐渐采用基于模型的开发方式，而这类系统对软件有着应实时性要求，反应时间要控制在几毫秒以内，而通常还要求保留一定的反应余量。因此，模型验证在网络系统的实时性验证上具有先天优势。

目前，国内外对模型的功能与正确性验证研究比较丰富，但是实时性验证研究并不广泛。因此，本文将介绍当前实时性验证所面临的问题，并重点介绍网络系统实时性验证领域的建模方法，并结合这些方法所依托的工具，分析各种方法所面临的问题，最后针对检测方法面临的挑战提出一些思路。

2 模型验证方法及面临的问题

模型检测首先要对系统建模，选用一种形式化描述方法，将待验证的系统设计转化为工具所能接受的模型，比如状态迁移图。然后，將系统所要验证的性质采用形式化的逻辑公式来描述，比如时态逻辑。它能够描述系统随着时间变化而引起的行为变化。最后是系统验证，是通过模型检测算法对系统模型的状态空间进行穷尽搜索。如果未发现违反性质描述的状态，则表明该模型满足期望的性质，否则给出一个反例路径，供设计人员参考。

模型验证方法应用初期，系统的状态和状态间的迁移都是采用显式的状态迁移图来表示。这种方法对那些进程数量较少的网络系统非常实用[2]。而当网络分量较多时，系统的全局状态空间会随着分量的增加，呈指数增长，即产生状态爆炸问题，状态爆炸问题是阻碍模型检测技术应用的瓶颈。

3 建模方法

3.1 最差情况执行时间方法

最差情况执行时间（Worst-Case Execution Time，WCET）是验证系统实时性的主要方法之一，由奥地利维也纳技术大学的Puschner和Burns提出[3]。WCET刚提出时，由于当时计算机软件需求有限，软件代码的执行时间未引起人们的重视。但是，随着软件技术的不断发展，代码执行时间的越来越复杂，WCET分析技术逐渐受到研究者的重视，目前，国内外有许多机构或大学开始加深对WCET的研究，从2001年开始，国际上每年召开一次WCET研讨会。WCET分析技术与计算方法趋于多样化，从早期的程序标注和语法制导算法发展为基于树和路径的计算方法。

WCET分析是指计算给定应用程序代码片断执行时间的上限，这里的执行时间定义为执行代码片断所花费的处理器时间。在实时系统中，如果想保证系统整体的实时性得到满足，就必须要求软件各部分在最差情况下执行的时间也能满足实时性要求，这样由部分集成到整体时，整个系统才会满足实时性的要求。

WCET分析要求安全性和精确性，安全要求不能低估最差执行时间，精确要求能够给出可以接受的高估值。我们假设程序P的WCET估算值为WCETc （P），P的实际WCET值为WCETA （P），安全性和精确性描述为：

安全性：

WCETc （P） ≥WCETA （P）

精确性：

（WCETc（P） -WCETA（P））/WCETA（P）≤δmax

其中，δmax为系统能够接受的最大相对误差。

在程序层次的验证方面，国防科技大学张曦团队利用WCET技术对嵌入式实时软件的验证进行了深入研究，提出了一种基于WCET分析的模型检验方法框架[4]，实现了对源程序的一种实时性验证方法。

该框架首先对源程序进行WCET分析，其中包括对程序的静态分析，划分出程序代码的路径集，然后利用WCET工具进行分析程序执行时间上限，分析过程如图1所示。

利用WCET分析结果对原有的实时约束进行修正，建立系统的实时性模型，同时在系统需求中提取时态逻辑作为系统的性质描述，其中时态逻辑反映了程序应该遵循的先后顺序。结合实时性模型与时态逻辑公式通过验证工具UPPAAL对模型的实时性进行验证，如果实时性验证不通过，则返回修改源程序。如图2所示。

本方法做到了对实时系统的程序层次的验证，较好地解决了状态爆炸问题，其中源程序的WCET分析是验证环节的重要一环，但是当前WCET分析能力有限，比如复杂程序运算时间估算、估值精确度、误差控制等问题。另外，对源程序的修正可能会引入新的错误，并且修正内容无法反映到生成代码的上层模型中。

3.2 时间自动机建模

为了描述实时系统的时间约束关系，Alur等人提出了时间自动机（Timed Automata，TA）[5]。时间自动机是一类带有时钟变量的有限状态自动机，其数学模型可表述为一个六元组：

Ta= （L，L0，C，A，E，I ）

其中：L是位置的有限集合；l0∈L，为初始位置；C是时钟有限集合；A是行为的有限集合；"EL×B（C）×A×2c×L是边的集合，用于描述位置之间的转移；B（C）是使能条件集合，用于描述发生转移的时间约束，2c为转移发生时的时钟集合；映射I："L→ B（C）" 用于给每个位置指定一个时钟约束。

用时间自动机网对实时系统建模，首先要对系统进行抽象和简化，子系统要简化为有限控制结构、时钟和变量构成的时间自动机，子系统之间通过通道进行通讯。然后要分析实时系统的信息处理过程，提炼重要的信息处理状态和事件进行建模。子系统的行为抽象为时间自动机，它们之间的信息交互通过通道来完成，各个时间自动机就组成网络进而描述整个实时系统的信息处理过程。

时间自动机是一种反映了时间约束的有限状态转换图，通过使用有限的真值时钟变量表示时间约束，实时系统行为可以通过时间自动机来刻画，在对实时系统建模后，可以利用时间自动机来验证系统的实时性。在实时性约束下检验状态是否可达，因此对状态可达性的研究是时间自动机的验证技术的关键。

时间自动机技术也有不足：构造时间自动机方法很复杂，如果发生错误，将导致最终验证结果的不准确。另外，时间自动机的时间无限制，会导致状态空间的无限性，随着系统的复杂程度和进程数量的增加，将无可避免的发生状态空间爆炸。状态空间爆炸也是困扰实时系统验证的最大问题。

但是，典型的时间自动机组成的平面网络作为模型不易于模拟和调试大规模的工业系统。AIexandre David和Wang Yi提出了一种层叠时间自动机（Hierarchical Timed Automata，HTA）模型，它的状态既可以是简单状态也可以是组合状态，组合状态本身就是一个时间自动机。

层叠时间自动机的允许用户在模拟时，将系统模型的内部结构隐藏或者抽象，并且更容易调试，在处理多层次复杂系统建模时有较大优势。

3.3 RTCTL模型检测方法

计算树逻辑（Computation Tree Logic，CTL）是时序逻辑的一个分支，时序逻辑非常适合于对并发系统进行验证与刻画，即使对于复杂的并发系统而言，其刻画性质依然很强。时序逻辑用于描述系统中的状态变迁序列，不显示地表示时间，而是通过语义隐式表达时间。时序逻辑定义时序运算符与逻辑连接词来表达复杂的时序性质。CTL作为时序逻辑的一个分支主要用来描述计算树的性质[8]。

CTL公式由路径量词与时序运算符组成。路径量词用于描述计算树的分支结构，有两种路径量词：A（对于所有计算路径）和E（对于某些计算路径），分别表示从某状态开始的所有路径和某些路径所具有的性质。时序运算符描述某条路径的具体性质。有5个基本运算符，意义如下：X（下一个状态）F（将来某状态）G（将来全局状态）U（直到……都满足）R（直到……才满足）。

CTL有两种公式：状态公式与路径公式。令AP为原子命题集合，状态公式语法为：

1） 如果p∈AP，则p是一个状态公式；

2） 如果f和g是状态公式，则f和f∧g，f∨g是状态公式；

3） 如果f是一个路径公式，则Ef和Af是状态公式。

路径公式的语法为：

如果f是一状态公式，则f也是一路径公式；

如果f和g是路径公式，则f，f∧g，f∨g，Xf，Ff，Gf，fUg和飞fRg是路径公式[9]。

检测实时系统的时间约束的有效方法就是扩充CTL运算符，Emerson等人将CTL逻辑扩充为RTCTL。基本的RTCTL运算符是受限的直到运算符U[a，b]这里[a，b]表示时间间隔，在此间隔内这个性质必须是真的。fU[a，b]g关于某条路径π=s0，s1…为真，仅当g在此路径上将来的某个状态s上满足，那么f在s0到s上所有状态都为真，并且s0到s的距离在间隔[a，b]之间。同样的，CTL中的其他运算符可以增加时间限制来扩展。[a，b]作为一个时间间隔，可以看做是实时性的约束。

RTCTL模型在CTL的基础上进行了扩充，继承了CTL模型的精确性，解决了状态空间爆炸问题，同时加入了时间性约束，可以高效地表达实时性要求。目前有很多工具可以完成基于CTL的模型验证，RTCTL在实时性验证中的有很好的应用前景。

通过对时间进行量化分析，可以得到系统的最大、最小时延，完成实时性验证。

4 模型验证常用工具

4.1 UPPAAL

UPPAAL是丹麦Aalborg和瑞士Uppsala大学联合开发[10]，高效实用的基于时间自动机的实时系统模型验证工具。UPPAAL特别适用于实时系统的安全性和活性的自动验证。它将每个进程都描述为有限控制结构、时钟和变量组成的时间自动机，进程之间通过管道共享数据变量进行通信，管道用于保证不同自动机中的两个转换同时执行。UPPAAL通过快速搜索机制来验证时钟约束和可达性，不仅可以有效地发现设计中出现的错误，而且可以清楚地显示导致错误的判定路径。

UPPAAL拥有图形用户界面，主要包括三个部分：编辑器（Editor）、模拟器（Simulator）和验证器（Verifier）。编辑器用于创建和编辑所要分析的系统；模拟器用于模拟系统模型执行过程可能出现的错误，以便在验证前发现潜在的错误；验证器通过快速搜索机制搜索系统的状态空间、检查时钟约束和响应限制性质。

UPPAAL体系结构如图3所示。

UPPAAL的引入，简化了实时系统验证的工作量，并且增加了验证系统的可靠性。首先，UPPAAL中时间自动机网络中每个时间自动机都是相对独立的，又是可以互相通信的，不需要构造时间自动机的积，避免了构造模型的繁杂。另外，UPPAAL中的模拟器从直观上可以看到系统的运行过程，发现存在的问题，而验证器又严格的从语义上保证了系统的安全性。UPPAAL在时间和空间上的性能显著高于其他的实时验证工具，能够处理较为复杂的系统。

4.2 NuSMV

1987年左右，卡内基梅隆大学在读博士生McMillan开发出一个符号模型验证器SMV（Symbolic Model Verifier），首次使用二叉决策图（Binary Decision Diagram，BDD）来缓解状态爆炸问题，实现了符号模型检测技术，SMV是第一个基于BDD的符号模型验证工具[11]。2001年，Carnegie Mellon University（CMU）和Istitutoperla Ricerca Scientificae Techolgica（IRST）联合开发出NuSMV（ New Symbolic Model Verifier）[12]，NuSMV支持计算树逻辑（Computation Tree Logic，CTL）和線性时序逻辑（Linear Temporal Logic，LTL）描述的所有规范，作为一款比较成熟的模型检测工具已经发展到2.6.0版，NuSMV是开源工具，其源代码和二进制文件可以在官网上获取。

作為一种通用的模型验证器，NuSMV的基本运行原理：用户使用NuSMV提供的输入语言描述待验证实时系统和约束性规范，通过NuSMV自动进行，验证确定模型在规范中是否成立，若不成立输出No，并给出反例，解析为什么规范在模型中不成立。NuSMV的运行原理如图4所示。

在功能上，NuSMV支持CTL描述规范，所以RTCTL同样可以在NuSMV上得到验证，NuSMV在实时验证领域占有一席之地。

在结构上，NuSMV定义了一个良好的软件系统架构，做到了模块化和开放性，用户可以自由定制模块。

在支持性上，NuSMV有丰富的文档和开放的源码，作为一种模型检测的通用平台，用户可以在官网和开源社区获得帮助。

NuSMV的引入，明显地简化了实时系统验证的工作量，研究者提供了更广阔的研究空间[13]。

4.3 PAT

PAT[14]是由新加坡国立大学PAT研究小组自主开发的一套模型检测工具，支持并发、网络实时系统的建模验证，能够对多种语言进行模拟验证和反例生成。PAT是一个可扩展、模块化的通用架构，其系统框架如图5所示。

框架分为四层，方便了模块的扩展，建模验证过程分为三步：编译、抽象和验证。PAT工具具有良好的扩展性，因此可以利用建模层的抽象功能对建模语言进行抽象，避免状态爆炸。扩展PAT的并行模块可以方便网络系统的实时性的建模与验证。抽象后的语言模块能够自动转化为PAT已经支持的语言，从而简化系统描述和实现过程，使得建模过程更人性化、更易使用。借助PAT工具良好的扩展性，可方便对网络系统进行实时性建模。

4 结束语

本文首先介绍了模型验证的概念与当前的问题，并总结了三种网络实时性模型的验证方法和主流的实时性验证工具，对其优缺点进行了比较，为今后的研究提供有益参考。网络安全领域的模型检测技术应用越来越广泛。保障日益复杂的网络空间的安全性，是当前研究的难题，建立在严格数学理论基础之上的模型验证必将在其中占据一席之地。

参考文献

[1] 刘权，王超.勒索软件攻击事件或将引发网络军备竞赛升级[J].网络空间安全，2018，01：1-4.

[2] 张修康，金春华，白莹.应对网络安全威胁的技术演变[J].网络空间安全，2018，01：46-50.

[3] PETER PUSCHNER and A.Burns. Guest Editorial： A Review of Worst-Case Execution-Time Analysis， Real-Tim Systems， May 2000， 18（2-3）： 115～128.

[4] 张曦.基于WCET分析技术的程序实时性模型检验方法研究[D].国防科学技术大学，2012.

[5] Alur R， Dill DL. A theory of t imed automat a[J] . Theoretical Computer Science， 1994， 126（ 2） ： 183- 235.

[6] David A ， Yi W . Hierarchical Timed Automat a for UPPAAL [ A ] .10th Nordic Workshop on Programming Theory （ NWPT） 98） [ C] .Turku Cent re f or Computer Science （T UCS） ， Finland， 1998.

[7] Michael Huth and Mark Ryan.Logic in Computer Science：Modelling and Reasoning about System，Second Edition.Cambridge University Press，2004.

[8] E.M.Clarke and E.A.Emerson.Synthesis of synchronization skeletons for branching time temporal logic.In Logic of Programs：Workshop，Yorktown，Heights NY May 1981，volume 131 of LNCS.Springer-Verlag，1981.

[9] Emerson E.A..Branching time temporal logic and the design of correct concurrent programs[Ph.D.dissertation].Harvard University，Cambridge，MA，1981

[10] Behrmann G， David A， Larsen KG. A tutorial on UPPAAL. In： Bernardo M， ed. Proc. of the Formal Methods for the Design of Real-Time Systems. Springer-Verlag， 2004. 200?236. [doi： 10.1007/978-3-540-30080-9_7]

[11] 张军林，张治国.NuSMV模型验证器实现与分析[D].中山大学，2010.

[12] CIMATTI A，CLARKE E，GIUNCHIGLIA F，et al.NuSMV： a new symbolic model verifier[C]Computer Aided Verification.Berlin： Springer，1999： 495-499.

[13] 刘博，李蜀瑜.基于NuSMV的AADL行为模型验证的探究[J].计算机技术与发展，2012，（2）.

[14] LIU Y， SUNJ， DONGJS.Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney： Springer Press， 2010：371-377.