基于活性顺序图的形式化验证方法及工具研究

张　坤，叶俊民，王　嫱，赵丽娴，陈　曙

（华中师范大学　　计算机学院，武汉　430079）

基于活性顺序图的形式化验证方法及工具研究

张坤，叶俊民，王嫱，赵丽娴，陈曙

（华中师范大学计算机学院，武汉430079）

近年来，形式化验证方法在软件开发过程的作用越来越大；如何充分利用形式化验证方法提高软件系统的可靠性已成为软件开发者及使用者主要关注的问题；总结了近年来基于活性顺序图的形式化验证方法的研究进展，首先介绍活性顺序图的语言及其表达能力与复杂性，然后深入分析现有的基于活性顺序图的形式化验证的关键技术及其典型应用，最后实现一种基于活性顺序图的运行时验证工具，实验证明使用本验证工具进行形式化验证的可行性。

活性顺序图；形式化验证；软件开发过程

0　引言

随着计算机技术的发展，软件系统已经渗透到人们的生活之中，软件系统关系着人民的信息安全、财产安全乃至生命安全。形式化验证方法在软件开发过程中的作用越来越受到软件开发者的重视，确保软件系统在任何时候都与需求规约一致，已经成为软件开发者及使用者关注的重要问题，利用场景对系统进行建模和分析已成为软件开发过程中形式化验证的重要技术和方法［1］。目前形式化验证方法主要包括模型验证［2］与运行时验证［3］等。

基于场景的形式化验证经常使用顺序图对系统进行建模和分析，顺序图是一种基于场景的语言，能够图形化地表示系统实例间交互的时序关系。顺序图包括消息顺序图（Message Sequence Chart，简称MSC）［4］、.0顺序图（UML2.0 Sequence Diagram，简称UML-SD）［5］、活性顺序图（Live Sequence Chart，简称LSC）［6］及其它变种。MSC由ITU提出并在业界得到广泛应用，但MSC表达能力很有限，只能表示可能发生的场景，不能表示系统必须满足的场景。虽然UML-SD增加了一些新的操作符，增强了其表达能力，但UML-SD的非形式化语义也限制了其应用。LSC对MSC进行扩展，LSC使用universal和existential两种模式区分强制场景和可能场景，且LSC具有形式化语义。因此，软件开发过程中形式化验证经常使用LSC描述系统场景中事件交互的时态关系。此外，LSC可以用来建模实际系统，也可以用于描述场景需求，基于LSC的形式化验证方法不仅使系统需求的行为语义易于理解，而且还能尽早地发现软件设计错误。利用LSC对系统进行建模和分析已成为需求分析阶段的重要技术和方法。

LSC在MSC的基础上增加了活性（liveness）的概念，活性表示需求的场景一定会发生［7］。LSC分为universal和existential两种模式，universal图表示系统一定发生的场景，用实线矩形框表示，existential图表示系统可能发生的场景，用虚线矩形框表示。universal图包含一个前置图（prechart）和一个主图（main chart），前置图表示触发场景，用虚线六边形表示，主图表示响应场景，用实线矩形表示，universal图表示的意思是，如果前置图表示的触发场景成功执行了，主图就必须执行。existential图则只含有主图，不包含前置图，existential图只要求前置图与主图的一个事件实例，不强制要求主图要在每一次前置图执行后执行。

图1　universal模式LSC图

为了描述系统的强制性行为和可能性行为，LSC对图中所有的位置、消息和条件等元素分配了温度属性，若元素的温度是Hot，则该元素一定会发生，若元素的温度值是Cold，则该元素可能会发生。在LSC图中，Hot用实线表示，描述系统满足强制行为；Cold用虚线表示，描述系统可能满足的行为。如果实例线上某个位置是Hot位置，可以直接从当前位置移动到下一个Hot位置；如果这个位置是Cold位置，实例运行可能通过该位置。如果某个消息温度值是Hot，则该消息一定会被发送与接收；如果消息的温度值是Cold，表示该消息一定会被发送，但是消息可能被接收，也可能不被接收。

1　LSC语言定义

下面基于文献［8］形式化定义LSC语言，首先定义LSC语法，由于基于LSC的形式化验证过程一般基于程序执行轨迹，这里给出LSC基于轨迹的语义。文献［9］论述LSC具有很强的表达能力，为了充分使用LSC进行形式化验证，有必要对LSC的复杂性进行论述。

1.1LSC语法

令inst（c）表示LSC图c的实例线集合，dom（c，i）表示实例线i上的位置集合，dom（c）表示LSC图c上位置集合。

定义1（LSC）：LSC定义为一个7元组L=＜I，dom，ML，SR，Pre，Mode，quant＞，其中：

1）I是实例线的结合；

2）Dom是图c上的位置集合；

3）ML是图c的消息集合；

4）SR是图c的同步发生区域；

5）Pre是图c的前置图，可为空。

6）Mode∈｛initial，invariant，iterative｝，Mode决定LSC的执行频率。

7）quant∈｛universal，existential｝，quant决定LSC的模式。

1.2LSC基于轨迹的语义

由于定义LSC基于轨迹的语义时要使用LSC的cut，这里首先定义LSC的cut。

定义2（cut［8］）一个cut指图中每个实例到其位置的一个映射，cut⊆dom（c，i0）×...×dom（c，in），其中inst（c）=｛i0，...，in｝。

使用cut，下面定义LSC的执行轨迹。

定义3（执行轨迹）：令cuts序列c=c0，c1，...，ck为LSC图c的一次执行，执行轨迹w=trace（c），则w=w0w1，...，wk。其中c0，wi表示图c中事件的集合。

一个LSC的轨迹语言是LSC图c执行所产生的所有执行轨迹的集合。Lc=｛w|∃（c0，c1，...ck）∈R uns（c）｝，使得w =trace（c0，c1，...，ck），其中Runs（c）表示LSC所有执行轨迹的集合。

1.3LSC语言的表达能力与复杂性论述

在一定限制条件下，可以将LSC转换为等价的时序逻辑语言或者自动机语言［9］，这表明LSC语言具有很强的表达能力。Bontemps等人［10］主要讨论了LSC语言的复杂性，表明LSC语言复杂性主要包括两个方面：1）LSC语义依赖于偏序关系；2）LSC的规约是非结构化的。前者引起的复杂性可以在实际应用中避免，因为实际应用场景一般是线性时序场景。后者引起的复杂性问题可以通过额外的信息生成高效的算法来解决。研究表明，LSC转换为时序逻辑语言或自动机语言的复杂度相对较小，因此LSC经常用于形式化验证。

2　基于LSC的形式化验证方法

在形式化验证过程中，主要有建模系统和描述需求规约两类需求。由于LSC可以用来建模系统行为，也可以用于描述场景需求［8］。因此，基于LSC的形式化验证方法关键技术主要从以下两个方面进行论述。

2.1使用LSC建模系统行为

形式化验证需要建模系统行为，MSC可以直观的描述系统中对象间的交互情景，MSC可以解决基于状态图作为系统行为模型的局限性问题，但是在捕获系统行为需求时，MSC也存在一些不足［11］，LSC也可以建模众多系统，且LSC语言可以补充MSC的不足，因此，使用LSC建模系统行为的研究逐渐展开。使用LSC建模系统行为即从基于场景规约的LSC构建可执行的系统。目前主要有两种方法［12］，第一种是自动合成系统的方法。给定LSC模型，确定是否存在一个系统满足该LSC模型，如果存在这样的系统，则根据LSC模型中实例间的交互确定实例的有限状态机或状态图，有限状态机或状态图集合构成确定满足该LSC的系统，但是合成的系统要满足两个需求：1）合成的系统需要监听系统中发生的事件；2）合成的系统必须满足LSC模型，自动合成系统的方法已在文献［11］实现。第二种方法是从LSC规约中场景实例间的交互建模可执行的系统［13］，该方法不是为每个实例产生实例的内部规约，而是按照算法直接执行场景，在LSC的场景描述中定义可执行的系统及系统运行产生的状态。这种方法有一个研究成果，即Play-out机制［13］，Play-out机制允许工程师与其它相关人员更好地了解场景实例交互所产生的行为。

这两种常见的方法各有特点，两种方法的比较见表1所列。

2.2使用LSC获取待验证的系统性质

形式化验证经常使用时序逻辑语言或自动机语言等描述系统的待验证性质。但在工程应用中，尤其是在基于场景的软件工程中使用时序逻辑并不实际。由于LSC语言具有直观性和形式化的特点，因此在形式化验证中，LSC经常作为系统开发过程中需求规约描述语言，然后将LSC转换为待验证的性质，这些性质然后用时序逻辑语言或自动机语言进行描述。关于从LSC获取待验证的系统性质，下面分LSC转换为时序逻辑和LSC转换为自动机两种类型进行论述。

表1　使用LSC建模系统的两种方法比较

2.2.1LSC转换为时序逻辑

Bontemps等人［14］对于只含LSC核心语法的LSC规约，证明任何LSC规约都可以转换为时序逻辑公式。Kugler等人［15］设计算法将LSC转换为LTL公式，其它相关的研究很多基于该转换算法，文献［15］主要产生两种性质：图中消息的偏序性质（φ性质），图中消息的唯一性性质（χ性质）。对于一个universal图，对应的LTL公式φc形式如下。

该转换等式从上到下分为三部分，顶部的φ性质保证了前置图与主图中的消息都是偏序关系，中部保证了只有前置图的消息都发生后，主图中的消息才并且一定发生，底部保证了图中的消息只发生一次。文献［15］中的转换方法为LSC图每一个可能的执行入口都生成LTL公式，转换后的LTL公式的规模是LSC中事件规模的平方复杂度。Kumar等人［16］从化简偏序性性质和化简唯一性性质两个方面，利用LSC规约中性质的实现文献［15］中转换的优化，优化后所产生时序逻辑的规模是主图中最大消息规模的平方复杂度，该优化在大多数情况下可以缩小转换所产生的LTL公式的规模。

此外，LSC转换为时序逻辑这些方法有一定的限制，这些方法的研究一般只针对LSC核心语法所表示的需求规约，缺少将完整LSC语法转换为时序逻辑的算法。

2.2.2LSC转换为自动机

文献［17］实现了LSC转换为自动机，他们将符号化自动机结构形式的LSC图作为输入的自动机结构，然后通过增加接受状态和增加/更新迁移将符号化自动机结构转换为可以检测安全与活性错误的否定自动机。该转换过程关注于创建自动机结构，并使用得出的自动机实现形式化验证，如果需求规约用时间扩展的LSC表示，则可将LSC转换为时间自动机。一般的转换过程关注于创建自动机结构，Kumar等人［18］则直接研究了适用于发现系统错误的LSC到自动机的转换过程，他们的LSC转换为自动机的转换过程使得性能与可扩展性均显著提升。

将LSC规约转换为自动机语言，然后使用基于自动机语言进行形式化验证，这种方法可以支持LSC的更大语法子集，且支持更大规模的LSC规约［17］。

3　基于LSC的形式化验证典型应用

基于LSC的形式化验证应用已有很多，从形式化验证方法分类来看，目前基于LSC的形式化验证主要应用有模型验证领域与运行时验证领域等。下面就基于LSC的形式化验证在模型验证领域与运行时验证领域的应用进展加以论述。

3.1基于LSC形式化方法的模型检测

LSC可以作为系统需求规约描述语言，通过将LSC转换为时序逻辑语言或自动机语言的方法可以从LSC获取系统待验证的性质［17］。此外，LSC又可以建模系统行为，因此，LSC也是系统的高级编程语言。模型检测即需要建模系统也需要时序逻辑或自动机语言等表示的需求规约，而LSC正好具有上述两种表述能力。因此，很多模型检验应用研究都基于LSC，基于LSC形式化方法的模型检验应用研究可以分为三类：

1）LSC只转化为系统行为模型，待验证的系统性质规约由用户定义［17］；

2）系统行为模型由其它模型产生，待验证系统性质规约从LSC中获取［19］；

3）系统行为模型由LSC转换形成，待验证系统性质规约也从LSC中获取［8］。

其中，情形3）的基于LSC形式化方法的模型检测过程如图2所示。

图2　基于LSC形式化方法的模型检测过程

3.2基于LSC形式化方法的运行时验证

LSC可以转换为时序逻辑语言或者自动机语言来获取系统需求规约，将转换的时序逻辑语言或者自动机语言表示的需求规约作为监控器［3］，使用运行时验证的相关技术［20］就可以实现基于LSC形式化方法的运行时验证。基于LSC形式化方法的运行时验证过程如图3所示。

图3　基于LSC形式化方法的运行时验证过程

基于LSC的形式化方法应用于运行时验证领域已经有相关研究，Chai等人［21］提出中标准LSC语言在其研究的嵌入式实时系统中表示特定场景的正确性性质还不够充分，因此引入充分前置图的概念，提出扩展的活性顺序图 （extension of live sequence charts，简称eLSC），并分为有迭代eLSC和无迭代eLSC两种场景，有迭代eLSC场景直接使用文献［15］中的方法转换成为LTL公式，并使用公式重写的方法使用Maude工具引擎［22］进行运行时验证，无迭代eLSC场景则设置专门的算法进行运行时验证。并研究了欧洲列车控制系统（ETCS）中RBC/RBC切换场景，实现基于LSC形式化方法用于运行时验证。

4　基于LSC的验证工具实现

本文实现的基于LSC的验证工具的设计思路是：首先，插装获取系统执行轨迹，导入目标系统程序，使用Spring AOP进行代码插装获取其执行轨迹；然后，输入使用从LSC转换所得的LTL公式；最后，自动生成被验证的项目文件，再调用Maude工具引擎实现运行时验证。

4.1工具架构

本文设计的基于LSC的验证工具架构如图4所示。

图4　运行时验证工具框架

1）插装获取系统执行轨迹：

在此模块中，用户可以导入要验证的目标系统源程序，并且可以在工具中查找已导入的目标系统程序代码。在目标系统程序运行时，根据配置的插装点通过Spring AOP插装获取目标系统的执行轨迹序列，并将执行轨迹序列存贮在本地，便于后续的运行时验证。

2）导入需求规约：

在此模块中，根据LSC描述的需求规约场景，用户可以导入从LSC转换所得的LTL公式，导入的LTL公式作为需求规约将存贮在本地，便于后续的运行时验证。

3）运行时验证：

在此模块中，工具根据公式重写算法自动生成相应的重写规则，Maude工具引擎根据重写规则文件运行产生监控器，监控器分别根据（1）和（2）获取的系统执行轨迹和需求规约进行重写逻辑的运行时验证，并显示验证结果。

4.2工具实现

4.2.1插装获取系统执行轨迹模块实现

该模块的作用是通过Spring AOP插装获取目标系统的执行轨迹。在该模块中，GetSystem Trace类调用目标系统运行，RBC2RBCAspect类根据配置的插装点进行代码插装，当目标系统运行完成后，RBC2RBCAspect类的通知代码获取系统的执行轨迹序列。然后由GetSystem Trace类生成原子命题声明文件与执行轨迹序列日志文件。如图5所示是本模块的静态结构图。

图5　插装获取系统执行轨迹模块静态结构图

4.2.2需求规约导入模块实现

该模块的作用是导入从LSC转换所得的LTL公式，同时生成相应的需求规约文件并将其存储在本地，生成的需求规约文件将作为需求规约输入到Maude工具引擎中。如图6所示是本模块的静态结构图。

图6　需求规约导入模块静态结构图

4.2.3运行时验证模块实现

该模块的作用是调用Maude工具引擎进行运行时验证。该模块中，RunDemo类生成相应的重写规则，Maude工具引擎根据重写规则文件进行运行时验证，并显示运行时验证结果。如图7所示是本模块的静态结构图。

图7　运行时验证模块的静态结构图

4.2.4验证过程

第一，插装获取系统执行轨迹。首先，工具将导入并运行目标系统，当目标系统运行结束后，工具就获取了执行轨迹序列。第二，导入待验证的需求规约，输入从LSC转换所得的LTL公式形式的需求规约。最后，进行运行时验证。工具首先生成重写规则文件，然后调用Maude工具引擎，Maude工具引擎根据重写规则产生预测监控器，进行运行时验证，并显示验证结果。本次实验结果如图8所示。

本次实验结果为“maybe”，由于从LSC转换所得的LTL公式含有时序逻辑运算符G，验证工具分析目前的执行轨迹没有发生需求违约，但对以后的执行情况还无法确定，判定结果为可能为真，因此验证结果为maybe，这也体现出LTL三值语义实现了对LTL二值语义的自然覆盖。然后进行另一组实验，本次插装获取另一条轨迹t=HOVCond，pre，req，ack，rri，使用工具进行运行时验证，该执行轨迹的实验结果为“false”，如图9所示。

图8　运行时验证

图9　执行轨迹违反规约的验证结果

5　结语

基于LSC的形式化验证方法已成为软件开发过程中一种重要的验证方法，基于LSC的形式化验证已经成功应用到多个领域。本文对基于LSC的形式化验证方法进行研究，论述LSC的理论基础，对比分析了基于LSC的形式化验证领域的关键技术与应用进展，并实现一种基于活性顺序图的验证工具，实验证明使用本验证工具进行运行时验证的可行性。随着软件规模不断扩大系统集成度不断提高，基于LSC的形式化验证方法必将在软件开发过程中发挥其应有的价值。

［1］Li X S，Liu Z M，He J F.A formal semantics of UML sequence diagram［A］.Proceedings of the 2004 Australian Software Engineering Conference［C］.2004：168-177.

［2］Clarke E M，Grumberg O，Peled D A.Model Checking［M］.MIT press，1999.

［3］Leucker M，Schallhart C.A brief account of runtime verification［J］.The Journal of Logic and Algebraic Programming，2009，78（5）：293-303.

［4］ITU-T.Recommendation Z.120：Message Sequence Charts［Z］. Geneva：ITU-T，1999.

［5］Object Management Group （OMG）.UML［Z］：Superstructure Version 2.2.2009.

［6］Damm W，Harel D.LSCs：Breathing Life into Message Sequence Charts［J］.Formal Methods in System Design，2001，19（1）：45-80.

［7］李雯睿，王志坚，张鹏程.模态顺序图u MSD的形式化语义［J］.软件学报，2011，22（4）：659-675.

［8］Larsen KG，Li S.Scenario-based analysis and synthesis of real-time systems using Uppaal［A］.Proc13th Conference on Design，Automation，and Test in Europe［C］.2010：447-452.

［9］Harel D，Maoz S，Segall I.Some Results on the Expressive Power and Complexity of LSCs［J］.In Pillars of computer science，2008，351-366.

［10］Bontemps Y，Schobbens P.The Complexity of Live Sequence Charts［J］.Institut d'Informatique，University of Namurrue Grandgagnage，21B5000-Namur（Belgium），2005，15.

［11］Harel D，Segall I.Synthesis from scenario-based specifications［J］.Journal of Computer and System Sciences，2012：78（3），970-980.

［12］Harel D，Kantor A，Maoz S.On the Power of Play-Out for Scenario-Based Programs.［J］.Lecture Notes in Computer Science，2010：207-220.

［13］Brenner C，Greenyer J，Panzica V et al.The ScenarioTools Play-Out of Modal Sequence Diagram Specifications with Environment Assumptions［A］.In Proc.12th Int Workshop on Graph Transformation and Visual Modeling Techniques.Volume 58，EASST ［C］.2013.

［14］Bontemps Y，Schobbens P.The Computational Complexity of Scenario-based Agent Verification and Design［J］.Journal of Applied Logic，2007，5（2）：252-276.

［15］Kugler H，Harel D，Pnueli A et al.Temporal logic for scenariobased specifications［A］.Proc.of the 11th Int.Conf.on Tools and Algorithms for the Construction and Analysis of Systems（TACAS05）［C］.2005：3440，445-460.

［16］Kumar R，Mercer E，Bunker A.Improving translation of live sequence charts to temporal logic［A］.Proc.of the 7th Int.Conf. on Automated Verification of Critical Systems（AVoCS07）［C］. 2007，183-197.

［17］Kumar R，Eric G Mercer.Verifying Communication Protocols U-sing Live Sequence Chart Specifications［J］.Electronic Notes in Theoretical Computer Science，2009，250（2）：33-48.

［18］Kumar R，Mercer EG.Improved live sequence chart to automata translation for verification［J］.Electronic Communications of the EASST，Volume 10，2008.

［19］Li SH，Balaguer S，David A，G.Larsen K，Nielsen B，Pusinskas S.Scenario-based verification of real-time systems using UPPAAL［C］.Form Methods System Design，2010，37：200-264.

［20］张硕，贺飞.运行时验证技术的研究进展［J］.计算机科学，2014，41（11A）：359-363.

［21］Chai M，Schlingloff B.Monitoring Systems with Extended Live Sequence Charts［J］.Springer International Publishing Switzerland，RV 2014，LNCS 8734，48-63.

［22］Clavel，Duran，Marti-Oliet，Meseguer，Talcott et al.Maude Manual［M］ （version 2.6）.University of Illinois，Urbana-Champaign，2011.

Research on Formal Verification Method and Verification Tool Based on Live Sequence Chart

Zhang Kun，Ye Junmin，Wang Qiang，Zhao Lixian，Chen Shu
（School of Computer Science，Central China Normal University，Wuhan430079，China）

In recent years，the role of formal verification technology in the software development process is growing more and more important.How to use formal verification technology to improve the reliability of software systems is a major concerned problem of software developers and users.This paper summarizes the progress of formal verification method based on Live Sequence Chart recently.In this paper，the language of live sequence chart，its expressive power and complexity are first introduced.Then the existing key technologies and their application of formal verification method based on live sequence chart are analyzed.Finally，the runtime verification tool based on live sequence chart is implemented，experiments show the feasibility of using this verification tool to formal verification.

live sequence chart；formal verification；software development process

1671-4598（2016）05-0274-05

10.16526/j.cnki.11-4762/tp.2016.05.076

TP393

A

2015-11-14；

2015-12-15。

国家科技支撑计划项目（2015BAK33B00）；教育部规划基金项目（15YJA880095）；中央高校基本科研业务费专项资金科研项目（CCNU15GF003）。

张坤（1992-），湖北武汉人，硕士研究生，主要从事软件分析与验证方向的研究。