基于B/S架构的实时系统建模验证工具

石 安 张卓若 代立云

(西南大学 重庆 400715)

0 引 言

近年来，科学技术迅猛发展，对嵌入式实时系统应用的需求不断增加，实时系统(Real-time System)在核研究、航空航天、军事和民用领域都有着广泛的作用，如核反应冷却系统、过程控制系统、交通控制系统、轨道信号系统等。实时系统计算结果的正确性是指在规定时间内做出正确的程序逻辑响应。即系统须及时响应外部条件的要求，控制所有实时设备和实时任务在指定或确定的时间内协调一致地运行，完成系统功能。因此，实时系统需要在预定义的时间内对事件进行相应的处理与反馈。若该实时系统无法满足在“可执行时间”“任务周期”“通信延时”等方面的特定时间约束，可能会引发重大错误和安全隐患。如何有效地保证设计实时系统的安全性和可靠性，并保证各子系统的正常交互和各子任务的协调一致，一直是设计开发人员所关注的重点和难点。为了满足开发人员对实时系统的开发需求，基于现有建模与验证工具UPPAAL的优缺点，在继承其高可靠性与实时性优点的同时，克服其下载安装慢、拖拽控件不灵活且不支持多用户进行项目团队管理的缺点，本文设计实现了基于B/S架构的实时系统建模与验证工具。

1 相关背景

近年来，实时系统复杂性不断提高，硬件、软件规模不断增大。同时，实时系统具备的外部环境和系统内部的交互性、多种类型任务的混合性及对时间约束的严格性等，更增加了对其分析和验证的难度。从实时系统领域中应用的形式化方法来看，在计算机系统上层规范到最终实现的过程中，使用形式化语言对系统需求进行描述，并选择适当的形式化工具进行系统辅助设计和安全性验证，能够在较大程度上减少由系统开发人员引起的设计失误，从而提高系统的安全性[1-2]。

1.1 形式化方法

通俗地讲，形式化方法即通过数学逻辑的手段设计并开发一个高可靠性的系统。与传统的软件开发方法不同，形式化方法更加偏向于理论。国内外研究机构和学者根据各自不同的背景和研究基础，提出了众多形式化模型和验证方法。其中，模型检验(Model Checking)[3-4]是一种常用的实时系统形式化验证方法，在工业领域得到了较为广泛的应用。模型检验方法最早由Clarke等[5]及Quielle等[6]分别提出，使用状态空间搜索的方法遍历根据系统规范而设计的实现模型，系统的规范(Specification)由一种形式语言描述，从而进一步检验该计算模型是否满足某条由时态逻辑(Temporal Logic)公式所表示的特定性质。该方法可将验证过程自动化，即容易采用计算机进行辅助验证，应用起来比较简便，对工程技术人员的理论要求不高；同时，模型检验技术可对设计模型中的错误进行定位，当系统性质未被满足时可给出反例，帮助用户发现错误，增加了系统安全设计的可用性。但鉴于实时系统中时间变量的无界性，系统复杂性的提高易导致模型验证过程中出现状态爆炸问题。

1.2 同类系统研究应用与现状

近年来，国内外在实时系统的建模验证工作上取得了较大的进展，并推出了相应的算法和工具，包括改进的SMV[7]、AT&T的基于自动机理论的典型模型检验工具SPIN[8-9]、UPPAAL[10]等。其中，UPPAAL由于其可靠性和实时性高，是目前使用最为广泛的实时系统建模验证工具。UPPAAL是一个集成的工具环境，将时态逻辑模型检测理论及时间自动机理论相互结合，目前已大量应用于对实时控制器和通信协议的描述和验证[11]。UPPAAL使用快速验证技术和限制技术等模型验证技术，从而有效地保证了实时系统的安全性和正确性，同时还解决状态空间爆炸问题。UPPAAL主要包含系统编辑器(System Editor)、验证器(Verifier)、模拟器(Simulator)三部分。尽管功能已较为成熟，UPPAAL同样存在一些弊端。作为一款桌面应用程序，其需要从官网上填写个人信息后下载安装，等待时间较长；此后如有版本的更新，用户亦需另行下载新版软件。且局限于其JAR文件格式，用户需要配置Java运行环境和较高版本的JDK。同时，UPPAAL的用户界面设定有所欠缺，一些控件的点击、拖拽并不十分灵活，使得其在效率、有效性和用户体验等方面降低了性能。此外，UPPAAL的单用户设计不适合项目团队管理。更为重要的是，UPPAAL作为20世纪90年代诞生的一款工具软件，其后续所有版本的设计思想还停留在单机应用程序的构建思路上，早已落后于当前应用软件形态逐渐向网络化、服务化、云化发展的未来趋势，需要对其从系统架构上实施全面的改造和重新开发。

基于对实时系统建模验证工具的需求，同时结合现有相关工具存在的问题，本次系统在同样保证实时系统检验的安全性和正确性的前提下，采用B/S架构使得验证工具具有更简洁美观的用户界面且可以免安装直接在浏览器打开链接后使用，更快捷的同时，减少软件对电脑硬盘容量的占用和运行时对内存的消耗。而且B/S架构也能更便捷地扩展到项目的团队上。在保证程序升级方便，维护成本低的同时，能够在兼容性、可理解性、可用性等方面带给用户更友好的体验。这不仅对于这类工具本身的生长演化极具意义，更有利于向从事基于时间自动机的实时系统分析与验证领域研究的学者提供一款具备高可用性、高效率、轻量级、低成本的工具。

2 系统设置

本次系统开发前端使用mxGraph框架，通过JS实现网页界面和相关数据的显示，后端使用Java进行相关验证性任务的实现，前后端之间使用Ajax进行数据的传输。整个系统主要实现在线编辑时间自动机模型并对其相关性质进行验证，并且对于验证的结果会有反馈信息的显示。满足实时系统开发过程中，对于时间自动机模型的验证需求。在保证响应速度的同时，提供准确的验证结果。

2.1 架构设计

为实现上述功能，基于B/S架构进行设计与开发。用户通过浏览器进入操作界面，将大部分的事务逻辑留在后端实现。将Web浏览器作为核心应用软件，后端负责实现功能的关键部分，这样既利于开发又便于后期维护和用户使用。系统整体架构设计如图1所示。

2.2 整体功能设计

系统前端需要实现相关时间自动机模型的建模，包括图模型的导入导出，编辑和相关数据的处理与展示。在完成一个完整的时间自动机模型的生成之后，可以验证其相关性质并在前端返回验证结果，验证等相关功能的实现集中于后端。前后端之间的数据传输，采用Ajax技术，保证数据传输的效率，从而提高整个系统在验证过程中的响应速度。系统整体的功能流程如图2所示。

2.3 具体功能实现

mxGraph框架将图表元素的属性和图元间关联关系的描述以XML的格式保存和进行数据交换，能够将用户所编辑图形的数据存储成XML文件；此后，可快捷方便地通过Ajax传递到后端Servlet，将mxGraph生成的XML文件转换成UPPAAL格式的XML文件，然后通过命令行的方式连接到调用Verifyta验证器进行检验。检验的结果又通过Ajax返回到前端进行显示。

2.3.1前端mxGraph的使用

前端使用JS编写，结合mxGraph框架并生成XML文件。mxGraph是一个开源的JavaScript绘图组件，其前身为2000年推出的JGraph[12]。mxGraph主要提供快速生成可视化的图表、对图表进行自动化的布局、排列和分析，并提供相应的用户交互等功能[12]。在开发实现网页编辑显示Workflow/BPM流程图、网络拓扑图和普通图形等的Web应用程序过程中常涉及mxGraph框架相关技术。该框架具备架构简单、兼容性高、有效灵活的图像可视化等优点，可以很好地满足本次系统开发在前端对于图形高效编辑的需求。利用mxGraph中内置的文件字符解码器，可以方便地将格式内容精简且易于解析的XML格式文档转换为用户所需的数据格式文件。所支持的文件格式的存储包括GIF、JPG、PDF、SVG等，用户可根据实际需要灵活进行文件格式的选取。

2.3.2Ajax的使用

Ajax(Asynchronous JavaScript and XML)，即异步的JavaScript和XML，能够与服务器进行数据交换，并具有能够在不需要重新更新整个页面的情况下，只更新发生了数据改变的部分网页的功能。使用Ajax技术进行前端和后端的数据传输，实现导出XML文件、保存图片等，以及进行条件的验证等，同时将结果返回给用户。同时，在异步调用时通过设置请求超时处理，当数据请求失败时在页面提示用户检查网络或者数据库连接情况，提供了操作友好的人机交互[14]。如此使得Web应用程序更为迅捷地响应用户交互，实现了网页与网页间的平滑过渡，缩短用户等待时间，提升了用户体验。此外，Ajax采用异步方法与服务器通信，在不打断用户操作的前提下，通过降低网络数据流量且提高数据传输效率，优化了浏览器和服务器之间的沟通。

2.3.3后端Servlet的使用

后端使用Servlet可接收Ajax传来的请求，并实现将前端用户编辑并显示的图形导出PDF、JPG、PNG、XML等格式文件输出；将mxGraph格式的XML文件转化成UPPAAL格式的XML文件；连接verifyta进行某条件的形式化检验等功能。此外，可通过Servlet实现包括数据压缩、Web和URL访问、图像处理、JDBC、多线程等功能。

2.3.4Verifyta的使用

后端Servlet通过相关命令行语句的调用，连接到Verifyta，实现对程序可达性、安全性、活性等性质的验证。

UPPAAL的Verifyta验证器可由命令行调用，进行验证条件(Property)的形式化检验，输出结果(Satsified、Unsatisfied、Error)并在条件不满足时生成反例轨迹(Counter-example)到xtr文件(UPPAAL的历史执行轨迹文件)。

3 系统实现

3.1 系统编辑器的原理和构成

单击并展开左侧边栏中“Timed Automata”选项，可将长方形表示的模版和圆形表示的位置拖入右侧画面。系统最右侧显示图的相关属性，除常规的图的相关属性设置之外，还包括时间自动机的相关参数设置、函数声明等。

双击模版，即可进行模版的定义。模版(Templates)具有唯一确定的名称(Name)、模版声明(Declaration)和模版参数(Parameter)。其中，模版声明的变量为仅可供该模版使用的局部变量和时钟变量；模版参数可以是int、chan、const等类型的符号变量或常量(Symbolic variables and Constants)，进程声明(Process Declaration)时被赋值。由于系统通常具有多个相似的进程(Process)，通过定义模版(Templates)并在实例化时更改相应参数等，即可同时生成多个进程。系统主界面如图3所示。

点击右侧边栏“Edit Declaration”按钮，弹出框分别包含“Declaration”“Property”“Instantiation”选项。其中：“Declaration”中进行全局的时钟、整型、通道等类型变量的声明，在此中声明的变量在所有Template中有效共享；“Property”中，用户编辑、增删验证条件，并以此检验系统的行为和性质；“Instantiation”中对模版进行实例化，生成相应进程。点击图的顶点和边也可以进行相关属性的设置，顶点和边所包含的各自属性及其含义如表1所示。

表1 顶点和边相关属性含义表

3.2 验证器的原理和构成

由于该程序的验证部分使用了UPPAAL的verifyta验证器，因此具体实现主要参照的UPPAAL中的运行方式。

TCTL支持A[]φ、E<>φ、A<>φ、E[]φ、φ→ψ等表达方式(φ和ψ表示状态谓词)，其路径含义表如表2所示。

表2 路径含义图

查询规范语言包括路径公式(Path Formula)和状态公式(Path Formula)。状态公式是一个描述单个状态的表达式，可表示某特定进程是否处于某个位置(Location)，如P1.cs and x<3，其中P1表示进程，cs表示位置；也可在不考虑模型行为的情况下对状态进行评估，如x<3。

路径公式量化模型的路径或轨迹包括安全性(Saf-ety)、活性(Liveness)和可达性(Reachability)[17]，图4描述了所支持的不同路径公式。

可达性表示某给定公式φ是否能由某个可达到的状态(Reachable State)满足，即从初始状态起，是否存在一条路径可以最终达到某状态，该状态满足公φ，表示为E[]φ。可达性可以验证模型的一些基本行为，但不能保证模型的正确性。

安全性即“某坏事永远也不会发生”，指系统的正确性、互斥性和无死锁性。在UPPAAL中，通过以A[]φ表示“某好事始终为真”，来验证模型的安全性。活性即“某事最终一定会发生”，指系统的终止性、保证服务性和响应性，可表示为A<>φ。考虑到前置条件时表示为φ→ψ，即一旦φ发生，ψ定会发生。

死锁即证明系统在一般运行时不存在一个能够循环执行的路径环。通过对每个状态分别进行前向及后向搜索，如果都仅存在一条路径能够回到原来状态，即认为存在该可循环执行的路径环。UPPAAL中使用公式A[] not deadlock表示全局是否存在死锁状态。

同时，对TCTL等实时时态逻辑公式进行模型检验时，须对状态迁移的时间约束进行处理。在验证系统响应的实时性时，判断某条件能否实现须搜索该响应所有的可能路径如可实现，则须继续验证时间约束能否被满足，具体算法为把路径上所有迁移的时间约束进行累加，计算所有路径耗时的最大值，然后将该最大值和公式中的时间约束进行比较，从而判断该系统响应是否满足实时性要求。

4 系统测试与实例分析

在完成了系统的开发之后，测试实例至关重要。此次测试采用了实时系统中常见的时间自动机模型实例，通过完整的建模与验证流程来测试系统各个部分功能的实现情况。

4.1 Train-Gate实例简介

Train-Gate被定义为由若干列火车和一个控制器组成的铁路控制系统，描述列火车过桥的过程。该桥为一个共享的关键资源(Shared Critical Resource)，一次只可被其中一列火车访问。火车停下和重新启动都需要时间。当火车靠近桥时，发出“appr！”信号，并在10 s内监听控制器发来的停止信号“stop！”。如没有接收到，则不停车，并在3～5 s内通过，同时发送给控制器离开信号“leave！”；如接收到，表示前面有其他火车正在通过该桥，则该列车停车。控制器接收到“leave？”信号，得知前一列火车离开桥后，会发出“go！”信号，通知正等待的火车中最前面的一列继续行驶。该车收到信号后，有7～15 s的启动时间，然后同样在3～5 s内通过该桥并发送“leave！”信号。

4.2 过程演示

声明全局变量。常量N表示火车数量。定义长度为N的typedef类型数组id_t作为模版train的参数。同时，分别定义长度为N的通道数组appr、stop、leave和紧急通道(Urgent Channel)。紧急通道表示启动该转换时，必须没有延迟地同步执行消息的传递。同时，模版声明和全局声明时，使用JavaScript的正则表达式，在前端进行语法检验，同时与用户交互，进行相应错误的提醒。即保证声明的变量数据类型合法，为常量、整形、布尔型、通道类型、时钟类型、typedef类型等；且各声明语句之间由“；”隔开，从而更加确保生成相应XML文件的正确性。全局变量声明界面图如图5所示。

定义模版Train和Gate。将自动机中的顶点和边的连接好后，进行相关属性设置，完成建模。模板Train的自动机形式图如图6所示。

初始位置为Safe，可在任意时间到达Appr位置，此时通过appr[id]！通道，发送消息给Gate进程，并更新enqueue队列的值，在其末尾添加此火车id号，表示该辆火车即将到达。

Appr位置具有不变量限制x≤20及两种转换选择。其一，将转向Stop位置，其保护条件为x≤10，并有名为stop[id]？的同步通道，表示在10 s内某个不确定(Non-deterministic)时间，因接收到Gate进程通过Stop通道传递来的消息，跳转到Stop位置。其二，将转向Cross位置，其转换条件为x≥10，更新公式为x=0，表示因一直未接收到Stop消息，在10 s到20 s内的某个不确定时间，将跳转到Cross位置，并将时钟值重置为0。

Cross位置具有x≤5的不变量限制和x≥3，和通道leave[id]！，表示将在3～5 s某个时间，发送消息给Gate进程，并跳转回初始位置Safe。如Gate进程处于Free位置，且满足长度len>0，将跳转到Occ位置；如处于Occ位置，将跳转到Free位置，并将队列中第一个元素弹出，表示第一列等待的火车。

Stop位置具有通道go[id]？和更新公式x=0，表示当收到Gate传来的go消息后，将转换到Start位置，并重置时钟值为0。

Start位置具有不变量限制x≤15和x≥7，表示在7 s到15 s内某时间到达Cross状态。模板Gate的自动机形式图如图7所示。

Gate进程负责与train进程进行消息通信从而保证正在通过桥的火车只有一列。当Gate处于初始Free位置时，如队列的长度len=0，表示此时没有火车，则跳转到Occ位置；如Gate处于Occ位置，则跳转到下一紧急(Urgent)位置后，通过通道stop(tail())！，发送消息返回给该Train进程。

实例中Train模板和Gate模板的局部变量声明和参数定义如图8所示。

在图8中，定义Train模版的局部时钟变量x，并设置其参数id，值在0～5范围。定义Gate模版的局部数组list，长度为N+1。同时定义局部函数enqueue()和dequeue()，分别表示在队列list的在末尾加入指定元素，或弹出其首部元素。

实例化Train和Gate模版为系统中的进程。在定义完成之后，必须进行声明，完成实例化。即声明了分别代表六列火车的六个Train类型的进程Train(0)-Train(5)，和一个Gate类型的进程。

在完成实例化以后，最终要检验该系统是否满足相关性质。四条消息分别从有无死锁、可达性、安全性、活性等方面检验系统的正确性。性质检验界面如图9所示。

本例中具体检验条件内容如下：

-A[] not deadlock 不存在死锁。

-Train(0).Appr-->Train(0).Stop 每列靠近的火车，都会在通过桥之前先停止。此为故意设置的错误条件，用以检验系统对错误项的检查和提示。

-A[]Train(0).Cross+Train(1).Cross+Train(2).Cross+Train(3).Cross+Train(4).Cross+Train(5).Cross<=1. 表明通过桥的一次只允许一列火车。(安全性)

-Train(0).Appr-->Train(0).Cross: 每列靠近桥的火车都会最终穿过该桥。保证最终所有火车都会顺利通过该桥。(可达性)

在Property List中添加上述四个条件，并且在最后一行添加一个错误格式的条件，此处为人为故意设置的错误格式的验证条件，从而检验系统能准确识别用户输入的是否是符合规范的检验性质内容。当条件满足时，返回“Formula is Satisfied”；条件不满足时返回“Formula is Not Satisfied”并提醒用户在首页面Tools-Trace中查看轨迹；此外，当输入内容错误时，会提示用户“Input is Wrong”，以便提醒用户在检查所输入的验证性质条件后重新输入。测试结果显示如图10所示。

此案例中，在上文的检验条件具体内容中可以看到，第二条性质是故意设置为错误的性质，故结果理应是不满足的。通过系统检验，得到了预期的正确结果，系统显示第二条性质不满足，并且提示在Tools-Trace中显示出反例轨迹。反例轨迹图如图11所示。

5 结 语

本文根据现实中科研人员在对于实时系统开发过程中，所遇到的时间自动机模型验证的需求，设计并实现了一个基于B/S架构的实时系统的建模与验证工具，并通过测试一个经典的Train和Gate时间自动机模型，实现其建模与性质验证，最终得到了预期的正确结果。

选择基于B/S架构更加符合当今网络化、云化发展的趋势。尽管本文基本达到了预期效果，但由于实时系统的验证修正涉及到的领域广泛且理论性强，在实际应用中，为了达到更好的用户体验，需要对该验证系统做进一步完善，通过建立用户权限设定、限制文档只读可写属性、资源自定义加载和文档本地自动保存及副本储存与服务端上传修改相结合等方式，可实现不同用户对系统资源的访问与修改，在不影响系统运行的安全性和可靠性的同时，实现资源的共享并提高工作效率。同时进一步提高验证器的工作效率，改进相关验证算法，满足实时系统的建模和检验过程中更多需求，例如在图11中还有两处留出的更多信息展示的空间，在后续的开发中将实现模型的可视化显示。通过交互式地运行系统，并将各进程的自动机图形当前所处的位置和转换标红，更直观形象地描述实时系统可能的动态行为及多并发进程之间的交互，从而开发出一个更加稳定且高效的实时系统建模与验证系统。