（计算机科学与技术专业论文）基于lsc的模型检验研究与实现.pdf

国防科学技术大学研究生院学位论文 摘要 随着软件工程学科的发展，形式化方法越来越多地用于软件开发周期的各个 阶段。在需求分析阶段，利用场景对系统进行建模和分析已成为一门重要技术。 l s c ( l i v es e q u e n c ec h a r t ) 语言以场景为描述手段，以顺序图的形式直观而精 确地刻画系统行为。基于l s c 的模型检验不仅易于理解，而且可以尽早发现设 计错误。 论文主要研究了一种对l s c 模型进行模型检验的方法，并实现了一个相关 验证工具。文章深入分析了l s c 语言。l s c 语言不仅具有直观可视的图形描述， 而且还有精确定义的语法语义，其表达能力很强。为了满足模型检验的需要，本 文在研究l s c 语法语义的基础上提出了一种生成与l s c 等价的状态迁移模型的 方法。该方法以所有实例的当前情境为状态，沿着系统运行的路径描述迁移，并 将l s c 特，囊显式地表达在迁移中，实现了从l s c 刽状态模型的转换，本文还分 析了l s c 待验证性质的特点，采用c t l 时j 卜逻辑公式作为待验征性质的输入。 壁于l s c 等价的：状态迁移模型，论文研究了对l s c 进行模型检验的方法。 最后，我们实现了一个l s c 模型检验工具，剥以x m l 文件输入的l s c 模 型和c t l 公式输入的待验证性质进行模型检验，从而实现对设计模型的确认和 验证。 关键词：l s c ，场景，顺序图，状态模型，模型检验，时序逻辑 国防科学技术大学研究生院学位论文 f o r m a lm e t h o d sa r eg a i n i n gw i d ea c c e p t a n c ei ne v e r yp h a s eo ft h es o f t w a r el i f e c y c l e w i t ht h e d e v e l o p m e n t o fs o f t w a r ee n g i n e e r i n g t e c h n o l o g i e s b e i n gr a n i m p o r t a n tt e c h n o l o g y t o c a p t u r e t h es o f t w a r e r e q u i r e m e n t s ，s c e n a r i o b a s e d a p p r o a c h e sa r ew i d e l yu s e da n dm a n ys c e n a r i od e s c r i p t i o nm e t h o d s ，s u c ha sm e s s a g e s e q u e c ec h a r t ( m s 6 3 ，a l ed e v e l o p e d w h i l et h el i v es e q u e n c ec h a r t ( is c ) i sa n e x p r e s s i v ea n dr i g o r o u sl a n g u a g ef o rt h es c e n a r i od e s c r i p t i o n ，t h em o d e lc h e c k i n go f l s cs p e c i f i c a t i o n si sp o s s i b l ew h i c hh e l p sf i n ds o m ee r r o re a r l i e r i nt h i st h e s i sw ep r e s e n tam e t h o d ，w h i c hf a c i l i t a t e st h em o d e lc h e c k i n go ft h e l s cs p e c i f i c a t i o n so ft h er e a c t i v es y s t e m s ，a n dw eh a v ea l s oi m p l e m e n t e dat o o lt o a u t o m a t et h em e t h o d w ef i r s ta n a l y z et h el s cl a n g u a g e ，w h i c hi sa ne x p r e s s i v e v i s u a lb e h a v i o u r a ls p e c i f i c a t i o nl a n g u a g ea n dh a sr i g o r o u ss y n t a xa n ds e m a n t i c s m o d e lc h e c k i n gu t i l i z e st h es t a t em o d e lo fs y s t e m s ，t h u s ，w ep r e s e n tam e t h o dt h a t g e n e r a t e st h es t a t em o d e l sf r o ml s cm o d e l sb a s e do i lt h el s cs e m a n t i c s w h e nt h e s t a t em o d e l so ft h es y s t e m sa r eg e n e r a t e d ，w ec a nd om o d e lc h e c k i n gb a s e do nt h e s t a t em o d e l s ，t h ep r o p e r t yg e n e r a t i o nf o rl s ci sa l s oa n a l y z e di nt h et h e s i s h a v i n g d i s c u s s e dt h es t a t em o d e lg e n e r a t i o na n dt h ep r o p e r t yg e n e r a t i o n ，w es t u d i e dt h e m o d e lc h e c k i n gm e t h o d so fl s cs p e c i f i c a t i o n s a tl a s t ，w ed e s i g na n di m p l e m e n ta v e r i f i c a t i o nt o o l ，w h i c hg e n e r a t e ss t a t et r a n s i t i o nm o d e l sf r o mt h ex m lf i l e so fl s c s p e c i f i c a t i o n s ，a c c e p t st h ei n p u tp r o p e r t y ，a n dt h e nb e g i n sm o d e lc h e c k i n g t h em o d e l c h e c k i n gm e t h o da n d t h es u p p o r t i n gt o o le n a b l eu st ov a l i d a t ea n dv e r i f yt h es o f t w a r e r e q u i r e m e n t sa ta ne a r l ys t a g e k e yw o r d s ：l s c ，s c e n a r i o ，s e q u e n c ec h a r t s ，s t a t em o d e l ，m o d e lc h e c k i n g ，t e m p o r a l 1 0 9 i c i i 国防科学技术大学研究生院学位论文 第四章l s c 模型检验3 0 4 1 模型检验技术简述3 0 4 2l s c 性质描述3 5 4 3 基于状态搜索的模型检验3 5 4 3 1 c t l 公式的分解。3 6 。 4 3 2 验证算法3 6 4 4 基于s m v 的验证3 7 4 4 1 s m v 语言3 7 4 4 2 映射规则3 8 4 5 本章小结3 8 第五章验证工具的设计与实现4 0 5 1 验证工具及其体系结构4 0 5 1 1 体系结构4 0 5 ，i2t 具功能4 1 5 1 3 具体实现4 2 5 2 一个应用实例分析4 2 5 3 本章小结，4 5 第六章结束语 6 1 主要成果 6 2 未来工作展望 致谢 攻硕期间发表的文章 参考文献 图1 _ 1 图2 1 图2 2 图2 3 图2 4 图2 5 图2 6 图3 1 图目录 ，4 6 ，4 6 4 6 4 8 4 9 5 0 软件开发中的模型检验3 可见事件示例9 u n i v e r s a l 图示例1 1 e x i s t e n t i a l 图示例1 1 l s c 图例1 2 p e r c h a r t 和c o l dl o c a t i o n s 示例1 3 基本l s c 语义模型框架自动机 l s c 运行路径示例 1 7 2 1 国防科学技术大学研究生院学位论文 图3 2 多个运行路径示例2 2 图3 3l s c 模型与其状态模型2 8 图4 1 计算树3 2 图4 2 部分c t l 公式语义3 4 图5 1 验证工具的体系结构4 0 图5 2 验证工具交互界面。4 1 图5 3 列车离站场景。4 3 图5 4 验证结果。4 4 表目录 表3 1列车控制系统中的事件 表3 2l s c 中支持的强制性和可能r # 概念 表4 1 从l s c 状态迁移模型到s m v 表5 1 验证结果显示 8 1 4 3 8 4 4 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：基王竖塑搓型拴堕塑童量塞理 学位论文作者签名：曼蟹 日期： o 帕侔j f 月| ) 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阆；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可阻采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书。) 学位论文题目：基b i ! 曲搓型揸坠婴童皇塞理 学位论文作者签名 作者指导教师签名 墨宏 是k 乞。乞 日期：捌牛年 f 月l 日 日期：如铲i t 月1 日 国防科学技术大学研究生院学位论文 第一章绪论 1 1 课题背景 当前，许多领域对计算机软件的正确性和可靠性提出了很高要求，例如交通 控制、飞行控制、汽车设备和航空设备等等。特别是在安全攸关领域，如果软件 出现错误，造成的损失将非常巨大。因此，研究如何提高安全攸关软件和系统盼 正确性和可靠性非常重要。 1 1 1 高可信软件与形式化方法 人们提出各种方法和技术来开发高可信软件，例如形式化方法、软件测试等。 形式化方法以，一密的数学为基础，使人们能够以精确的方法来表示概念，证哪川虬 范和设计的性质，并且在丌发出软件产品之i i 就能对产品的行为进行推理。经过 多年的计算机科学研究和工程实践，人们已经、谚 到形式化方法在丌发安仑收关 j 监用中的重要作h 俐。自2 0 世纪9 0 l - t b t ，期以来，高可信软件和系统受到了 国际上广泛的重视，成为计算机科学技术的重要热点。在美国，d a r p a 、n s f 、 n a s a ( 国家航空和宇宙航行局) 、n i s t 等机构都积极参与了关于高可信软件和 系统的研究开发；n a s a 先后发布了形式化方法规范和验证指南( f o r m a l m e t h o d ss p e c i f i c a t i o na n dv e r i f i c a t i o ng u i d e b o o k ) 第一卷和第二卷。事实卜- ，许 多标准已明确要求或推荐在安全攸关的高可信应用开发中使用形式化规范和验 证技术。 形式化方法中，模型检验【3 9 】( m o d e lc h e c k i n g ) 是一种很重要的自动分析和 验证技术，其实质是利用计算机的强大计算能力，通过穷举被检验系统的有穷状 态空间中的每一个状态来验证该系统是否满足特定的形式规约。相对于传统的形 式化证明方法而言，模型检验方法具有快速、全自动、对使用人员的数学背景相 对要求不高的特点。很多情况下，可以把模型检验和各种抽象与归纳原则结合起 来验证非有穷状态系统( 如实时系统) 。模型检验已经在硬件电路、通信协议、 软件系统规范中得到成功的应用，例如i e e e 标准的验证、各种协议验证、大型 通讯软件验证等。 1 1 2 反应式系统与场景 安全攸关领域的计算机系统多为反应式系统，因而对反应式系统的研究非常 重要【1 0 】。简单地讲，反应式系统的特征是不断地与环境进行交互，它们通常执 第1 页 国防科学技术大学研究生院学位论文 行一些行为动作，对外界的激励做出响应。这种连续的交互特性与转换式程序不 同，它没有固定的输入输出。另外，反应式系统通常又是并发执行的，而并发系 统往往存在不确定性。所以，对反应式系统的行为描述是一件困难的事情。 近年来，利用场景来规约反应式系统行为的技术得到了很大发展 3 , 1 3 , 1 4 】。针 对一个系统的行为描述，设计人员可以将它分解成若干场景，这也是一种分而治 之的思想。一个场景指“一种可能发生在几个对象间有目的的交互行为”【研。它 由一个或者多个动作组成，每个动作表示一个对象和另一个对象之间的一次交 互。在一个场景中一系列动作的组合描述了一条运行路径。场景可以用不同的符 号( 语言) 表示，可以是非形式化语言、半形式化语言以及形式化语言【1 2 l 。本 文所说的l s c ( l i v es e q u e n c ec h a r t ) 语言【1 】即为一种可视形式化规约语言，它 可以精确描述场景中的行为。 1 2 立题意义 我们以广泛使用的u m l 为例说明软件的”发过程1 1 1 , 4 1 l 。丌发人员首先进行 需求分析。用户给出系统用例，用例实例化的结果即为场景，场景描述了系统中 对象间的行为交互，u m l 利用顺序图来描述场景。在进一步的系统设计和实现 中，u m l 从各种不同角度，采用各种手段为系统建模，一般利用状态机描述对 象内的行为变化。顺序图的表达能力较弱，只能帮助设计人员理解系统的行为过 程，不能对系统中行为给予精确描述。因此，当前对系统进行模型检验，往往需 等到系统设计的后期1 2 9 】，等到系统的状态机模型建立，主要基于状态机模型进 行模型检验。 可见，模型检验欲得到更广泛地应用，需克服两个主要障碍：错误的发现需 等到系统设计的后期；只有具有较深的专业知识才能给出待验证性质，并进行验 证。 顺序图用于系统设计早期，它描述了系统中对象间的行为交互( 即场景) 。 顺序图是直观的、易于理解的。因此，虽然基于顺序图做模型检验将可以较好地 克服上述两个障碍，使得模型检验在软件开发能得到更广泛的运用。事实上，近 年来基于顺序图的形式化分析验证得到了很大发展【2 0 , 2 7 1 。典型的顺序图如：盯u 的消息序列图【2 1 , 2 z l ( m e s s a g es e q u e n c ec h a r t s ，m s c ) 以及它在u m l 中的变种 u m l 顺序图。但是这些顺序图的语义却很弱，无法精确描述系统行为。为了解 决这个问题，同时保留可视化的优点，h a r e l 等人提出了一种对m s c 进行扩展的 语言l i v es e q u e n c ec h a r t s ( l s c ) 1 1 l 。l s c 能够很好的描述系统的场景，精 确地描述系统中的行为，是一种表达能力很强的可视化规约语言。 第2 页 国防科学技术大学研究生院学位论文 直观的可视化的l s c 语言可以精确描述系统中的行为，而基于l s c 的模型 检验能够尽早验证用户需求是否满足系统性质( 如时序逻辑给出的性质) ，本文 从这个角度出发展开研究。 这样，我们在软件开发过程增加了基于l s c 的模型检验。图1 1 中显示了 软件开发过程中各种模型检验的关系。特别的，我们观察l s c 模型和状态枕模 型，l s c 模型的建立比状态机模型要早，所以基于l s c 的模型检验可以尽早发 现错误；图中也说明从l s c 的对象问行为描述是可以向状态机的对象内行为描 述进行转换。 图1 1 软件开发中的模型检验 值得注意的是，基于l s c 进行模型检验也可以很好地解决软件开发中的两 个问题： 确认“我们开发的是我们所需要的软件吗? ”，这是说软件是否符合用 户需求；由于l s c 是一种形式化的顺序图。因此它很适合描述系统交互行为， 进行需求获取。 验证“我们开发的软件正确吗? ”，这是说软件是否f 确、可靠。我们 可以通过l s c 模型检验发现设计错误。 第3 页 国防科学技术大学研究生院学位论文 1 3 论文的主要研究内容 l 、深入研究了l s c 语言 l s c 有两种模式的图：u n i v e r s a l 图和e x i s t e n t i a l 图。u n i v e r s a l 图用于表示强 制性场景，即系统中一定发生的场景：e x i s t e n t i a l 图用于表示可能发生的场景。 系统中的消息、实例变量的条件、实例运行( 1 0 c a t i o n ) 均带有强制性或可能性 的属性。形式化的顺序图必须关联变量，l s c 对消息、条件、实例均有严格的定 义。形式化的顺序图不仅精确描述了对象间的交互行为，还揭示了对象内部的行 为变化。例如：消息的时间顺序和因果顺序得到区分；事件的强制性和可能性得 到区分；对象实例的运行过程也得到表示。 l s c 同m s c ( 或u m l 顺序图) 比较：增加了强制性与可能性概念，语义更 加丰富严格，表达能力大大增强。 l s c 同状态图比较：能够从l s c 模型转换到状态图，他们的表达能力本质 | j | 是一致的。 l s c 同时序逻辑比较：l s c 模型可以由时序逻辑c t l 表达，c t l + 的表达能 力强于l s c 语言；但没有必要将l s c 语言的表达能力进一步加强。 2 、提出了从l s c 到状态迁移模型的转换方法 l s c 基于场景为系统建模。系统场景包含一系列实例与事件。任何时刻，关 于实例变量一组命题集合构成系统的一个状态，而命题构成用户关心的性质。当 系统运行在某个状态时，这时所有实例的命题有些为真，有些为假；当实例局部 计算或事件改变了变量的值，使得实例命题的值发生了变化，系统状态改变。可 见，系统当前状态是所有实例当前位置的一个映射。系统的状态可以用c u t 来表 示，c u t 是系统所有实例的当前位置的集合，它关联了所有实例命题的当前值。 场景揭示了系统的一个或多个运行路径，我们沿着系统运行路径，用c u t 表 示系统状态，将所有系统状态的变化迁移关系表达出来，即形成了系统的一个状 态模型。迁移关系是系统运行路径的体现，具体由系统的事件和实例运行决定。 论文增加了一个终止状态，若迁移运行到终止状态，表示这是一条被系统接收的 运行路径。 因此，生成l s c 状态迁移模型的核心思想：根据系统的运行路径进行转换， 以系统运行中所有实例的c u t 为状态，以实例运行过程结合发生的事件为迁移顺 序，并把l s c 图中强制性和可能性概念表现在迁移中，完成u s c 模型到状态模 型的转换。系统的实例变量决定了系统的状态，系统的事件决定了状态的迁移。 因此，l s c 状态迁移模型与原l s c 模型的一致化约束为：l s c 状态迁移模型中 的变量和事件与l s c 模型中变量和事件一一对应。 第4 页 国防科学技术大学研究生院学位论文 3 、研究了基于l s c 的模型检验方法 对于一个从l s c 模型生成的等价的状态迁移模型，用户或设计人员结合系统 场景和模型给出验证性质，对此状态迁移模型( 即k r i p k e 结构) 进行模型检验， 论文研究了下列两种途径。 一种为直接搜索状态空间，看待验证的性质是否满足，其主要思想为：对于 一个r i p k e 结构m 和一个c t l 公式表达的验证性质甲，从印的最初级子公式( 原 子命题) 开始，标识令该子公式为真的m 中的状态。子公式逐步扩展，所标识的 状态也随之变化，直到最后子公式变为牛；此时看m 是否标识了印，若标识了则 验证性质成立，反之则不成立且为一个反例。 另一种途径是利用现有模型检验工具s m v 3 0 3 l 】，将生成的状态迁移模型转 换为s m v 输入语言，利用s m v 进行验证。根据一定的条件，主要将模型状态 和事件、变量映射为输入语言的状态和布尔变量，迁移映射为c a s e 语句，输入 的待验证性质映射为断言，从而生成s m v 输入语言。 4 、开发了l s c 模型验证工具 基于状态搜索的方法，丌发了l s c 验证工具。验证工具一方面从l s c 模型 的x m l 文件读入图形信息：实例、事件、l o c a t i o n s 及其相关变量，生成l s c 模 型的等价的状态迁移模型m ；另一方面，由用户输入性质，通过搜索l s c 等价 的状态迁移模型进行模型检验。 由于原子命题和实践相关，我们在课题中只验证事件之间的时序逻辑性质。 我们定义了一个函数h ( e v e n t ) ，表示事件发生，将之作为原子命题在状态中标出， 可以验证消息、条件的时序顺序。 1 i4 论文的组织结构 论文内容共分6 章，各章内容简要描述如下： 第一章“绪论”，交代论文的研究背景，确定论文的研究角度和意义，并概 要的介绍了论文的主要研究内容，给出了本文的组织结构。 第二章“l s c 语言”，介绍了l s c 语言，分析其语法语义，并将它的表达能 力和现有行为规约语言进行比较。 第三章“从l s c 模型到状态迁移模型”，研究从顺序图形式的l s c 模型到 其等价的状态迁移模型转换的方法和算法。 第四章“l s c 模型检验”，介绍了模型检验和时序逻辑，分析用计算树逻辑 笕5 页 国防科学技术大学研究生院学位论文 c t l 表示待验证性质的特点，研究了两种模型检验的途径和具体方法。 第五章r 验证工具的设计与实现”，介绍了验证工具的体系结构、具体实现 和功能，并就一个具体实例利用工具进行分析。 第六章“结束语”，在总结论文的基础上，提出了下一步的研究内容。 笫6 页 国防科学技术大学研究生院学位论文 i 第二章l s c 语言 2 1l s c 的应甩背豪 消息顺序图( m s c ，m e s s a g es e q u e n c ec h a r t ) 2 1 , 2 2 被广泛用于描述系统 场景，获取系统中对象问典型的行为交互，理解系统的执行过程。这种直观可视 的描述方法在系统开发的早期特别有用，因此r r u ( 国际电信联盟) 对m s c 进 行了标准化，并不断对其进行修改以适应实际需要。r r u 的m s c 标准f 2 l ，2 2 】给出 了一定程度的语法语义描述；除此之外，其它若干文献【12 j 也提出了m s c 语法和 语义定义：同时，为了支持基于m s c 的分析，许多机构也开发了与m s c 相关 的分析工具【2 4 , 2 7 。 尽管m s c 得到了广泛应用，但是m s c 本身存在一些不足。如：一个m s c 规约是否描述了系统所有的行为? 或者只是描述了一个系统的一些阡本行为? 通常，m s c 只是用柬捕捉相应用例的一些样本场景。随着系统模型的精化和对 用例理解的深入，已有的系统描述手段必须解决个需求描述问题：u j 能性 ( e x i s t e n t i a l ) 视点和强制性( u n i v e r s a l ) 视点之阿的转换。前者说明当某个条件 为真，则此场景可能发生；而后者指出，如果刻画该场景的条件为真，系统则必 须执行图中描述的这个场景。因此，我们希望能够规范场景的活性( 1 j v e n e s s ) ， 即强制性的行为。 实际上，一个基本m s c 图本身也存在可能性和必然性之间的混淆：m s c 的 消息序列没有说明描述的是时间偏序约束，还是消息间的因果联系。标准 2 1 ，2 2 】 中仅仅把m s c 的语义视为按时间顺序排列的事件的一种约束，而设计者则希望 根据设计的深入和细化，进一步对消息发收的必然性和可能性作出强制规定。 i t u 标准中没有考虑对条件多样性的支持，从而无法区分可能性和必然性，表达 能力比时序逻辑或者其他形式化语言要弱得多【2 3 】。因此，需要扩展m s c 语言， 使之具备清晰的语法和完全的形式化语义。 因此，d a m m 和h a r e l 等提出了一种新的称为l i v es e q u e n c ec h a r t s ( l s c ) 1 的语言。l s c 是对m s c 的扩展，区分了系统中可能发生( e x i s t e n t i a l ) 和必须发 生( u n i v e r s a l ) 的场景，而且也规范了可以接收到( c o l d ) 和必须接收到( h o t ) 的 消息。对图中其它元素也规定了其强制性和可能性，一个条件可以是c o l d 或者 h o t ，前者意味着它可以为真( 否则不执行当前的图) ，后者则说明它必须为真( 否 则系统中断) ：实例的运行可以定义为h o t 温度和c o l d 温度，h o t 温度迫使实例继 续向前执行，到达实例线的下一点，c o l d 温度要求实例可以停留在它当前的运行 位置上。强制性行为描述要求行为必须发生，可以表达出系统的活性属性：对强 第7 页 国防科学技术大学研究生院学位论文 制性条件设置f l a s e 条件，可以表示禁止出现的行为，表达出系统的安全性属性。 自提出以来，l s c 以其卓越的表达能力而得n t 许多很好的应用【3 , 1 7 0 1 9 】。在软件 的需求阶段，设计人员利用l s c 语言可以对系统进行更好的分析【1 5 , 1 6 1 我们作 基于l s c 的模型检验研究也属于此范畴。 2 2 席l s c 描述系统行为 本节我们以列车系统f 2 l 为例说明如何利用l s c 描述系统的行为。该案例可 简述为：一个环形铁路中有六个站点，每两个相邻站点间有两条线路；若干列车 在这个环形路线上运行，运送旅客。在此系统中，我们抽象出一些对象： 夺c a r h a n d l e r ：车站中负责与列车通讯并调度列车的管理中心； 夺d e s t p a n e l ：车站中接受乘客要求，将消息返回给乘客的装置； 夺c a r ：列乍； 夺p f o x i m i t y s e n s o r ：列车上测试列车与前方h t 标距离的感应器； 夺c r ul s e r ：列车的操纵者。 夺p a s s e n g e r ：乘客。 对象c a r 可以发送事件s t a r t ，s t o p ，e n g a g e 和d i s e n g a g e 给c r u i s e r ，发送 d e p a r t r e q 和a r r i v r e q 给c a r h a n d l e r 。对象c a r 也可以从p r o x s e n s o r 处接收a l e r t l 0 0 和a l e r t s t o p 事件，从c a r h a n d l e r 处接收d e p a r t a c k 和a r r i v a c k 事件，从c r u i s e r 处接收s t a r t e d 消息。 消息m s g i d 从实例i 异步发送到实例j 消息m s g i d 从实例i 同步发送到实例j 实例i 收到来自实例j 的消息m s g i d 消息m s g i d 从实例i 异步发送到外部环境 消息m s g i d 从实例i 同步发送到外部环境 实例i 收到来自外部环境的消息m s g i d 表3 1 列车控制系统中的事件 对于一个反应式系统，我们用v a r ( i ) 表示实例i 的变量，用e v e n t ( i ) 表示它的 事件。变量可以是局部变量，也可以是全局变量；要求v a t ( i ) 包括实例i 所有已 知的变量。l s c 作为一种形式化的顺序图，必须关联变量和事件才能精确的描述 系统的行为。表3 1 给出了消息事件的形式与含义。 系统s 的个快照s 显示了某个时刻所有可能的事件及所有的变量所赋的 第8 页 国防科学技术大学研究生院学位论文 值。如果条件c 中涉及到了e v e n t ( s ) ( 系统的实例的事件集合) 中的事件或者v a r ( s ) ( 其实例中的变量) 中的变量，那么，s l _ c 表示快照s 满足条件c 。假定执行语 言有线性时间的语义。对系统s 来讲，s 的一次运行是一个无限的快照序列。通 常用r 表示一次运行，i ) 表示它的第i 个快照，用r i 表达从r 中截取前i - 1 个前缀 时获得的无穷序列。r u n s ( s ) 表示s 的所有运行的集合。 令m 是l s c 的集合。m 中的每个元素m 中的事件和变量是可见的，并分别 用v i s _ e v e n t s ( m ) 和v i s _ v a r ( m ) 表示m 的可见事件集合和变量集合。如果m 中所 有m 满足v i s _ e v e n t s ( m ) ce v e n t ( s ) 并且v i s _ v a r ( m ) 量v a r ( s ) 。则称m 与s 是一 致的，记作c o m ( m ，s ) 。 图2 1 可见事件示例 图2 1 中可以看到的事件有： ， ， ， ， ， ， ， ， 。 v i s _ e v e n t s ( m ) t 9 有些内容没有在图2 1 中表示，如 ， ， 第9 页 国防科学技术大学研究生院学位论文 ， 。 如果该图是u n i v e r s a l 图，则v i s _ e v e n t s ( m ) e o 的事件均不得在图中的事件之间 出现。这样就保证了a r r i v r e q 和a r r i v a c k 消息不能在车离开终端站的时候出现， 因为这两个消息只与列车到达有关。 如果单个图m 表示了s 的一次运行f ，则表示为r 卜n l 。在图中不可见事件 和变量不受图的约束。但是可视事件及变量则受图的限制。此外，如果r 卜m ， 在r 中插入任意个m 中不可见并且没有受到m 限制的事件得到r - j i t t e r ，则r - j i t t e r 卜m 。与此类似，插入任意或者有限数量的局部变量( 这些变量没有出现在 v i s) ，也不会影响 的正确性。_ v a r ( m ) q 6 r r l i t u 标准没有对m s c 和独立的系统描述之间的相互关系做出规定。但是必 须解决系统行为不同视点( 如对象问和对象内部的表示) 的表示和验证。在开发 过程中般按如下过程使用l s c ： 在设计过程的j i 期阶段，通常用l s c 来描述系统可能的使用：设计者舰定系 统需要显示在蚓中的行为。系统至少有一次运行满足幽。 在设计的后续阶段，对系统的使用方式有了充分的了解后，就要保证，无论 系统如何运行，都要保证图中所规范的行为的执行。 在l s c 中，每个图都有其特定的模式： m o d ( m ) e e x i s t e n t i a l ，u n i v e r s a l 因此，系统s 的一个l s c 规约表示为四元组： l s = 其中m 是与s 一致的l s c 的集合，a c ( m ) 和p c h ( m ) 为每个m e m 提 供了激活条件或p r e c h a r t 。 一个图m e m 满足一次运行r e r u n s ( s ) ( 记作r 卜m ) 当且仅当： 若1 1 3 是u n i v e r s a l 的，则v i ，( r ( i ) _ - a c ( m ) jr ih ) ； 若n l 是e x i s t e n t i a l 的，则了i ，( r ( i ) b c ( m ) 八r i 卜m ) 。 系统s 满足规约l s ( 表示为s 卜l s ) 当且仅当： 对所有的e x i s t e n t i a l 图m e m ，jr er u n s ( s ) r 卜m ； 对所有的u n i v e r s a l 图m m ，v r er u n s ( s ) rh n 。 一般来说，一个e x i s t e n t i a l 图的p r e c h a r t 的激活条件比较弱，可能退化为真， 而且p r e c h a r t 本身很小甚至为空，因为通过e x i s t e n t i a l 图只能部分了解这个系统 开发阶段的需求。相反对u n i v e r s a l 图来说，系统的一次运行不需要匹配这个激 活条件，因此，个u n i v e r s a l 图的主体部分可以为空，此时对系统没有任何限 制。l s c 的支持工具应该提供对u n i v e r s a l 图的正确性( h e a l t h i n e s s ) 检查，确保 第1 0 页 国防科学技术大学研究生院学位论文 至少有一次运行能达到这样一个点，能够满足p r e - c h a r t 和激活条件。 图2 2u n i v e r s a l 图示例 图2 2 用一个u n i v e r s a l 阿描述了一辆车离丌站点的场景。参与这个场景的对 象有c r u i s e r 、c a r 和c a r h a n d l e r 。在这里用一个激活消息简单地表示激活条件。 用一个从图外面来的虚线的c o l d 消息箭头标出这个激活消息。只要c a r 收到 s e t d e s t 这个消息，图中的消息序列就开始执行：c a r 向c a r h a n d l e r 发出离丌清求 d e p a r t r e q ，c a r h a n d l e r 返回一个确认离开的d e p a r t a c k 消息。为了启动c a r 的引 擎，c a r 向c r u s i e r 发出s t a r t 消息，后者回应一个s t a r t e d 消息给c a r 。最后c a r 发一个e n g a g e 消息给c r u s i e r 。这时c a r 可以离丌终点站。每一个发送事件都跟 着一个相应的接受事件。 广一一一一一一一一一一一一一一一一一一一一一一一一一一一 ：p r o x s e n s o jc r u s i e rc a rc a r h a r i d e r ； a r r i v e r e q 。 一a r r i v e a c k a l e r t s t o p d i s e n g a g e 1 j s t o p 图2 3e x i s t e n t i a l 图示例 第1 1 页 国防科学技术大学研究生院学位论文 图2 3 则描述了个e x i s t e n t i a l 图的例子，用虚线框标出。这个图描述了c a r 停在车站的的情境。作为一个e x i s t e n t i a l 图，它不需要满足所有的运行；但要求 至少有一次运行满足它。 2 3l s c 语法语义 对于一个反应式系统，我们用l s c 对其行为进行描述，利用u n i v e r s a l 图规约强制性场景，利用e x i s t e n t i a l 图规约可能性场景，从而形成了一个 l s ，l s = 宏观地描述了一个系统，这一节我们将深入到 l s c 内部，研究其语法语义。 2 3 1l s c 语法 1 图形符号及其含义： l s c 扩展了i t u 的m s c ，主要区分了系统的强制性行为和可能性行为，增加 了活性( l i v e n e s s ) 成分。l s c 圈中标记着强制性或者可能性符号，称这种关f 内部图元素的差异为这个元素的温度( t e m p e r a t u r e ) ；强制性元素的温度是高 ( h o t ) ，而暂时性元素的为低( c o l d ) 。下面我们结合图2 4 介绍l s c 图中元素得含 义及其强制性和可能性概念。 图2 4l s c 图例 l s c 图中包含一组系统实例，如图1 中1 1 1 4 。实例的概念取决于l s c 描述 的内容，可以为进程、对象、组件或环境等等。实例上垂直向下的线表示其生命 第1 2 页 国防科学技术大学研究生院学位论文 线。在实例线上，发生了事件点称之为l o c a t i o n s ，为了便于表达，我们在图中用 数字标出l o c a t i o n s ，分别用 、 、 表示。 l o c a t i o n s 将实例线分成几个部分，例如1 1 被分为三个部分，从上至下依次为： 满足1 1 的初始条件，发送m l ，发送m 3 ；实线表示实例一定要通过此l o c a t i o n 到达下一个l o c a t i o n ，虚线表示实例可能会停在此l o c a t i o n 。 在一个l o c a t i o n 处，实例可以发送或接收消息。消息可用实线和虚线箭头表 示，实线表示消息必然被接收，虚线表示消息可能被接收。消息分为异步消息和 同步消息，异步消息的接收一定在消息的发送之后发生；同步消息的接收和发送 同时发生。 在一个l o c a t i o n 处，实例可以检验条件是否满足。条件可以只关联一个实例， 如c o n d 2 ，也可以关联多个实例，如c o n d l 。关联多个实例的条件称为共享条件， 共享条件的实例需要同步，即同时发生。条件可用实线框和虚线框表示，实线框 表示条件一定要被满足，否则系统中断，虚线框表示条件可能会不满足，若不满 足，系统退出当前习。 图2 5 拙述了火1 二进站的情境。图的顶音1 ；是p r e c h a r t 并用一个虚线榧乜 着，这意味这只有p m c h a r t 成功完成以后这个场景才能实现。在下而的c a r 和 c a r h a n d l e r 实体部分卅现的虚线段规范了消息a r r i v e a c k 可能不发送。这种情况 可能发生在站台关闭或所有的站台都满了的时候。 p r o )s e n s o r c a l c a r h md l e r d e p a rt a c k a l e r t l o o a r r i v r e q 。 a r r i r a c k 图2 5 p e r - c h a r t 和c o l dl o c a t i o n s 示例 l s c 图有两种模式，分别为u n i v e r s a l # l l e x i s t e n t i a l ，l s c 用u n i v e r s a l 来 表示强制性场景，用实线框表示，即系统中一定发生的场景，用e x i s t e n t i a l 图表 第1 3 页 国防科学技术大学研究生院学位论文 示可能发生的场景，用虚线框表示。如图2 4 即为一个u n i v e r s a l 图。