（光学工程专业论文）可验证的数字机器.pdf

福建师范大学学位论文使用授权声明 论文( 论文题目：可验证的数字机器) 是我个人在导师指导下进行的研 究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的 地方外，论文中不包含其他人已经发表或撰写过的研究成果。本人了解 福建师范大学有关保留、使用学位论文的规定，即：学校有权保留送交 的学位论文并允许论文被查阅和借阅；学校可以公布论文的全部或部分 内容；学校可以采用影印、缩印或其他复制手段保存论文。 ( 保密的论文在解密后应遵守此规定) 学位论文作者签名指导教师签名沪尹戗 福建师范大学工学硕士学位论文 摘要 随着数字时代的到来，工程师们研发系统的周期越来越短，对系统的可靠性要 求越来越高。图形建模是当今工程领域的一项重要技术。一个系统或是协议在它的 分析设计阶段，我们通过建立相应的图形化的模型，使它具有实际系统的某些性质。 模型是对系统的抽象，它较易于理解、分析和验证，对模型的验证结果可以直接作 用于实际系统，而且纠正错误的成本也相对于实际系统而言比较低。 我们构筑一个图形化的建模环境，基于状态机的原理对系统进行图形建模，并 定义其应具有的性质。然后分别对系统模型和性质进行形式化，最后通过计算机对 其验证。 论文利用状态机强大的图形化的描述能力对系统进行描述建模并定义了与之相 关的语法以及语义，文中引入了e h a 作为中间模型生成系统的l t s ，解决了状态机 对结构化的破坏问题，最后得出相应的b t l c h i 自动机。研究了如何使用l t l 公式表 达模型性质并给出l t l 公式到b t l c h i 自动机的转换方法。通过对两个自动机的乘积 进行判空，可以判断模型是否满足欲验证的性质。由于状态机本身具有并发和层次 等特征以及语义的复杂性，所以在模型验证时也面临空间爆炸问题。本文还研究了 如何缓解其所带来的空间爆炸问题。 关键词图形建模状态机验证线性时态逻辑 福建师范大学工学硕士学位论文 - _ i _ l l _ _ - _ - _ l l _ _ _ _ _ _ - _ i - - _ _ _ - _ - _ _ - - _ - - - l - _ - _ - _ 一i - - - l _ _ _ _ _ - _ _ _ - _ - _ - _ _ i _ i _ - - - - _ i i - _ l _ _ l _ _ - l _ - 一 a b s t r a c t t h em o d e ms y s t e m se n g i n e e r i n gd e m a n d sr a p i di m p l e m e n t a t i o n a n dq u a l i t y g r a p h i c a lm o d e l i n g a n ds i m u l a t i o n p r o v i d e s as o l u t i o nt o v e r i f yt h ed e s i g ng o a l s p r o a c t i v e l ya n d t or e d u c et h ec o s t i nt h i sp a p e r , w ep r e s e n tag r a p h i c a lm o d e lb a s e do nt h es t a t em a c h i n e w es e tt h e d e s i g ng o a l so fas y s t e mv i at h eg r a p h i c a lm o d e l ，a n dw ev e r i f yt h ed e s i g ng o a l si nt h e m o d e l i n gp r o c e s s w ea l s og i v ead e s c r i p t i o no ft h es y n t a xa n ds e m a n t i c so ft h es t a t e m a c h i n e w et a k et h ee x t e n d e dh i e r a r c h i c a la u t o m a t o n ( e h a ) a st h ei n t e r m e d i a t e m o d e lt oc r e a t et h el a b e l e dt r a n s i t i o ns y s t e m ( l t s ) t h i sa v o i d st h ed e s t r u c t i o no ft h e s t r u c t u r e s w ed e r i v et h ec o r r e s p o n d i n gb f i c h ia u t o m a t o n w es t u d yt h el t lf o r m u l a eo n d e s c r i b i n gt h ec h a r a c t e r i s t i c so fas y s t e ma n dw ep r e s e n ta m e t h o do fc o n v e r t i n gt h el t l f o r m u l a et ot h eb i i c h ia u t o m a t o n b ye x a m i n gt h ep r o d u c to ft h e s et w oa u t o m a t a ，w e a t ea b l et ov e d f yt h ep r o p e r t i e so ft h em o d e l e ds y s t e m b e c a u s eo ft h ep a r a l l e la n d h i e r a r c h i c a ln a t u r eo ft h es t a t em a c h i n ea n dt h ec o m p l e x i t yi n i t ss e m a n t i c s ，s t a t e e x p l o s i o ne x i s t si nt h ep r o c e s so fm o d e lv e r i f i c a t i o n w ep r e s e n tad i s c u s s i o no nt h i s i s s u ei nt h ep a p t e l k e y w o r d sg r a p h i c a lm o d e l i n g ，s t a t em a c h i n e ，v e r i f i c a t i o n ，l i n e a rt e m p o r a ll o g i c i i 福建师范大学工学硕士学位论文 、 中文文摘 数字机器( d i g i t a lm a c h i n e ) 是一种基于状态机的可视化图形化建模机，随着数 字时代的到来，工程师们研发系统的周期越来越短，对系统的可靠性要求越来越高。 图形建模是当今工程领域的一项重要技术。以往像软件和仪器系统以及协议的开发 总要等到代码测试和仪器生产出来之后才发现和排除错误，往往分析设计阶段的错 误到了测试阶段才发现，这样将造成各种资源的浪费甚至惨重的损失。而且系统的 是否可信赖是一些系统正常运转的关键因素。2 1 世纪高可信系统受到了国际上广泛 的重视，成为工程领域的研究热点，在美国，d a r p a , n s f , n a s a , n i s t 等机构都 积极参与了关于高可信系统的研究开发。由于计算机技术及其应用的飞速发展，人 们要设计的系统日益复杂化，用传统的设计方法已经不能或难以设计出符合要求的 系统。 一个系统或是协议在它的分析设计阶段，我们通过建立相应的图形化的模型， 使它具有实际系统的某些性质。模型是对系统的抽象，它较易于理解、分析和验证。 验证模型的目的是验证系统是否具有某些性质。目前的工程系统的分析设计阶段通 常只是划分接口、分配任务、描述任务、缺乏对模型的验证。建立模型到系统的可 靠转换之后，对模型的验证结果可以直接作用于实际系统，所以此时纠正错误的成 本也相对于实际系统而言比较低。因此本文提出的可验证数字机器的设计工作是很 有意义的。 我们构筑一个图形化的建模环境，基于状态机的原理对系统进行图形建模，并 定义其应具有的性质。然后分别对系统模型和性质进行形式化，最后通过计算机对 其验证。 目前建模语言规范大多是基于文法、代数理论或者数理逻辑等形式化体系，针对 的用户群体主要是系统分析人员。但是众所周知，建模语言的最终用户是领域专家， 他们熟悉领域建模的图符和模型语义，缺乏软件编程经验和计算机理论知识，因此无 法根据需求来进行建模并验证系统。本文研究的基于状态机的可视化建模机能大大 改善这种情况，利用状态机强大的图形化的描述能力对系统进行描述建模，弥补了 建模者在计算机知识上的缺失。 近年来已经出现了一些对状态机进行模型验证的研究。模型验证问题可以描述 为：对一个表示有限状态系统的k r i p k e 结构m = ( s ，r ，l ) 和一个描述系统性质的时态 福建师范大学工学硕士学位论文 逻辑公式9 ，找到所有满足9 的状态，即 s s i m ，s - 9 ，。当所有的系统初始状态在 该集合中时，系统满足妒。大多数的方法是将状态机模型转换为模型验证工具s p i n 或s m v 的输入语言进行验证。这种转换为己有并发系统模型检验工具的输入语言 后再进行验证，对状态机模型不是最自然和有效的方法，翻译之后引入较多冗余内 容，且由于语义的不同需要额外的处理。在此，我们考虑根据操作语义，用基于自 动机理论的方法针对状态机的特点直接进行模型验证。总体而言，在国内可视化图 形建模验证还处于起步阶段。 本文的主要研究工作如下： 第1 章绪论介绍了课题的研究背景和主要研究内容。简单阐述了国内外相关 的研究成果，说明了研究的意义，对图形建模及其形式化，模型验证等技术的发展 历史、主要方法和现状进行了简单的介绍。 第2 章基于状态机的图形描述及其形式化主要介绍了状态机的相关理论。阐 述了如何利用图元丰富的状态机对系统进行可视化的图形建模。介绍了状态机的图 形元素，定义了状态机的形式化语法和语义。状态机描述能力强大，并且提供了多 种图元从不同角度和应用层次刻画系统特性及其复杂的运行环境。 第3 章扩展层次自动机状态机刻画了系统中的对象在其生命周期中的行为和 状态迁移，这在系统分析和设计建模过程中占有重要地位，而对其进行正确性验证 以判断设计规范是否满足目标需求也成为一个关键问题。模型验证要求得到被验证 系统的l t s ，这就需要对状态机定义一种结构化的语义。层间迁移是体现状态机强 大、灵活功能的一个重要因素，却破坏了状态机的结构化，极大的复杂化了操作语 义。为了方便的建立状态机到l t s 之间的映射，我们用经过扩充的扩展层次自动机 结构化的表示状态机，并给出其形式操作语义和演绎规则。 第4 章基于状态机模型的验证方法介绍了b 0 c h i 自动机的定义，根据语义给 出由状态机生成b u c l f i 自动机的算法，研究了如何使用l t l 公式描述状态机的性质， 给出由l t l 公式生成b 0 c h i 自动机的算法以及根据b 0 c h i 自动机乘积进行判空来验 证其性质的方法。 第5 章验证优化与设计软件验证所面临的主要问题是空间爆炸问题，而其中 相当一部分原因可以归结为软件的规模问题。因此如何对程序进行裁剪，使所得到 的程序代码仍能反映原程序的部分特征并能够满足验证的需要是一个函待解决的研 究内容。近来模型检验方法的研究表明，针对欲验证的性质对系统的状态空间进行 福建师范大学工学硕士学位论文 缩减是解决空间爆炸问题的一种有效手段。程序切片思想按照切片准则来裁剪程序， 能够提取出程序中影响某个特定程序点变量值的语句，使人们能把注意力集中在相 关的程序代码上。程序切片开始主要应用在程序调试和理解方面，近年来已有研究 把切片方法应用在模型检验过程中以缩减状态空间。本章研究了如何对状态机进行 切片以缩减验证需要遍历的状态空间。 第6 章总结简单总结本文的研究内容，以及提出后续需要深入研究的工作。 第1 章绪论 第1 章绪论 1 1 课题背景 数字机器( d i g i t a lm a c h i n e ) 是一种基于状态机的可视化图形建模机。2 1 世纪 高可信系统受到了国际上广泛的重视，成为工程领域的研究热剧3 1 ，在美国，d a r p a , n s f , n a s a , n i s t 等机构都积极参与了关于高可信系统的研究开发。由于计算机技 术及其应用的飞速发展，人们要设计的系统日益复杂化，用传统的设计方法已经不 能或难以设计出符合要求的系统。一个系统或者软件( 包括电子的甚大规模集成电 路、通信协议等) 在它的分析设计阶段，我们通过建立相应的模型，使它具有实际 系统的某些性质【 】。验证模型的目的是验证系统是否具有某些性质。目前的工程系 统的分析设计阶段通常只是划分接口、分配任务、描述任务、缺乏对模型的验证， 模型是对系统的抽象，它较易于理解、分析和验证，对模型的验证结果可以直接作 用于实际系统【2 】，而且纠正错误的成本也相对于实际系统而言比较低。 目前建模语言规范大多是基于文法、代数理论或者数理逻辑等形式化体系，针对 的用户群体主要是系统分析人员。但是众所周知，建模语言的最终用户是领域专家， 他们熟悉领域建模的图符和模型语义，缺乏软件编程经验和计算机理论知识，因此 无法根据需求来进行建模验证系统【1 4 , 1 5 l 。本文研究的基于状态机的可视化建模机能 大大改善这种情况，利用状态机强大的图形化的描述能力对系统进行描述建模，弥 补了建模者在计算机知识上的缺失。近来己出现了一些对状态机进行模型验证的研 究。大多数的方法是将状态机模型转换为模型验证工具s p i n 5 2 j 或s m v 的输入语言 进行验证【1 l 1 2 。这种转换为已有并发系统模型检验工具的输入语言后再进行验证， 对状态机模型不是最自然和有效的方法，翻译之后引入较多冗余内容，且由于语义 的不同需要额外的处理。在此，我们考虑根据操作语义，用基于自动机理论的方法 针对状态机的特点直接进行模型验证。总体而言，在国内可视化图形建模验证还处 于起步阶段。因此以状态机为理论基础的建模验证技术是有实际研究意义的。 在数字机器中，系统模型描述可以是形式的也可以是非形式的。但是验证模型 要在形式化方法的框架中进行。我们所要设计的数字机器就是要在系统建模阶段， 通过状态机对系统模型进行图形描述( 非形式化的) ，然后再将其转化为相应的形式 化语言的表示，最后通过图形( g r a p h ) 搜索等算法对系统本身进行验证，得出结论。 结论：满足规范，或者不满足，提出反例。 验证系统大致有三种方法：模拟、演绛验证( d e d u c t i v ev e r i f i c a t i o n ) 、模型检验 福建师范大学工学硕士学位论文 ( m o d e l c h e c k i n g ) 4 5 1 。模拟是针对用户的，它是基于输入输出的考察。基于逻辑推 理的演绎验证是将系统抽象为一系列的条件和规则( i f t h e n e l s e ) ，证明所有符合 输入条件的输入根据规则演绎能得到正确的输出。模型验证( 基于穷尽搜索) 是穷 举地检查可能的状态和路径是否遵守性质规约【1 6 1 。 演绎验证( 定理证明) 用逻辑公式描述系统及其性质，通过一些公理或推理规 则证明系统具有某些性质。( 逻辑推理的主要方法有：自然推演、归结、h o a r e 逻辑 以及时序演算( m a n n a p n u e l i 命题线性时序逻辑p l t l 推理系统【4 9 】) ，优点：可验证 有穷状态系统也可以用归纳的方法处理无限状态的问题) 缺点：不能做到完全自动 化验证。对复杂的系统必须人为推理，效率低下，工业价值低【2 0 1 。 模型验证使用状态空间搜索的办法来全自动地检验一个有限状态系统是否满足 其设计规范。这类方法的优点在于它有全自动化的检测过程且验证速度快、效率高 【7 1 ，并且如果一个性质不满足，它能给出这个性质不满足的理由，据此可对系统描 述进行改进。该方法自提出以来，发展非常迅速，其理论与技术得到了工业界和学 术界的广泛关注i s 3 1 。目前，许多世界著名大公司如a t & t , f u j i t s u ，i n t e r ， i b m ，m i c r o s o f t ，l u c e n t ，m o t o r o l a ，s i e m e n s 等纷纷在其产品设计和开发过程中使用 模型检测技术，并在许多复杂的实例研究中发挥了重要的作用。模型检验只能验证 有限状态的系统，主要解决的问题是状态空间爆炸的问题。( 算法复杂性随系统状态 和所验证公式的长度增加非常迅速，与系统状态是多项式关系，与验证性质长度是 指数关系) 解决状态空间的爆炸问题的方法有：符号表示，偏序归约( p a r t i a lo r d e r r e d u c t i o n ) ，组合推理，对称，抽象，归纳。 最早模型验证由e m c l a r k e 和e a e m e r s o n l 2 4 及j e q u i e l l e 和j s i f a k i s t 2 5 1 在 1 9 8 1 年分别提出的，主要通过显式的状态搜索或隐式不动点计算来验证有穷状态并 发或实时系统。模型验证的方法是第一步指定系统应该具有的属性，第二步根据关 注的属性构造系统的形式模型。第三步运行模型检验器，检验形式模型是否具有特 定的性质，第四步分析运行结果如果出错根据给出的反例修改模型或属性，重新进 行模型检验。模型验证问题可以描述为：对一个表示有限状态系统的k r i p k e 结构 m = ( s ，r ，l ) 和一个描述系统性质的时态逻辑公式妒，找到所有满足驴的状态，即 s s l m ，s l - 9 ) 。当所有的系统初始状态在该集合中时，系统满足驴。 对系统进行形式化建模并进行分析验证包括下列步骤：1 建模：设计系统模型， 再把设计转化为模型验证工具可接受的形式系统。因为时间和空间的限制，设计建 第1 章绪论 模需要进行抽象消除无关或不重要的细节。2 规约：在验证之前需要陈述设计必须 满足的性质。规约一般以某种逻辑形式给出，我们研究的软硬件系统通常使用时态 逻辑，它能申明系统的行为怎样随时间变化。模型验证提供方法来验证一个设计模 型是否满足给定的规约，但不能确定给定的规约能覆盖系统应该满足的所有性质。 【1 5 】3 验证：理想的验证是完全自动的，然而实践中经常需要人工辅助。这里的基本 原理是给定的有限状态系统s ( 设计系统的形式化) 和给定的逻辑公式妒( 系统的 规范或者属性) ，判定s 是否满足矽。 模型验证是一种基于算法的性质验证方法。即给定一个有限状态的模型系统和 表示模型系统性质( 或规范) 的某种时序逻辑公式，看能否找到一个算法，它能够判 定该模型系统是否满足时序逻辑公式。如图1 1 所示，模型检测算法的输人包括两 部分，分别是待验证系统的模型m 和系统待检测性质1 l r ，如果模型m 满足性质v ， 则算法输出“t m e ”；否则给出反例说明m 为何不满足1 l r 。系统建模、性质描述和算法 验证是模型检测技术的三个主要步骤。 7 、 、 f得出结论) 图1 1 模型验证原理图 f i g1 1p r i n c i p l eo fm o d e lc h e c k i n g 1 2 可视化图形建模 系统的形式模型与建模方面，使用的形式工具主要包括有穷自动机理论、时态 逻辑、进程代数、p e r i 网等，并在层次上形成了并发系统、实时系统和混成系统的 抽象模型表示。i - l o g i x 公司从8 0 年代起推出和发展的建模工具s t a t e m a t e 可以 通过模块图、活动图和状态图创建一个可视化的系统规范【6 j ，它清晰、准确地反映 出指定系统预期的功能和行为。这个规范可以被执行或者进行图形化仿真，用来沟 通最终用户，确认系统规范是否符合需求。s t a t e m a t e 中的状态图可以描述系统 对激励事件的响应以及状态、行为的变化f 8 】，并通过t i m e o u t 和s c h e d u l e 等操作来描 述系统对实时特性的需求。s t e t e m a t e 已在多个关键领域进行了成功应用，如波 音飞机的储备管理系统、雷诺汽车的导向控制器、克莱斯勒汽车的定位系统等。 可视化图形建模语言是用来记录、交流系统设计思想的建模语言，它用图描述 福建师范大学工学硕士学位论文 系统模型的静态结构和动态行为【9 】o 状态机刻画了系统中的对象在其生命周期中的 行为和状态变迁，并对其进行正确验证以判断系统行为是否满足目标需求，在分析 和设计建模过程中占有重要地位。状态机是用来对单个实体行为或实体间交互建模 的图。状态机将系统动态行为离散化为格局及格局间的瞬时迁移。格局类似系统的 快照，是相对稳定，可见的；而迁移是格局之间的跳转，是瞬时的，不可见的。用 状态机建模，系统演化更抽象，易于理解和控制。状态机是h a r e l 经典状态图面向对 象的变种。h a r e l 经典状态图是基于状态的图形规约语言，它在有限自动机的基础上 增加了层次、并发和广播通信机制。而状态机在事件、冲突转换和进出入状态时执 行动作的处理上与h a r e l 状态图有所不同。验证状态机描述的不同系统元素的行为是 否满足某些性质能尽早发现设计中的错误。但状态机中的组合状态，层间转换，历 史转换等在丰富了描述手段的同时也破坏了结构的模块性，而且转换结果也与上下 文相关【1 3 】。这使得直接对状态机模型验证非常困难。为此，本文为状态机定义了形 式化语法和语义，通过e l l a ( 层次自动机) 转化成b u c h i 自动机进行验证。 1 3 形式化验证技术及其发展 ( 1 ) 时态逻辑和模型验证 时态逻辑最初是哲学家在研究自然语言中使用时间的方式而发展起来的。时态 逻辑已被证明对描述并发系统很有用，因为它们能描述事件相对于时间的顺序而不 显式的引入时间。时态逻辑通常按照时间是否被假设为一个线性或分支结构来进行 分类。有一些学者提议用时态逻辑来推理计算机程序，而p u n e l ：i 第一次用时态逻辑 推理并发系统【矧。他的方法是通过一组描述程序中单个语句行为的公理来证明程序 的性质。 c l a r k e 和e m e r s o n 在8 0 年代早期引入时态逻辑模型验证算法使这类推理能够自 动化【2 4 1 。由于验证一个模型是否满足一个公式比证明一个公式对所有模型都满足简 单的多，所以能够有效的实现该算法。他们为计算树逻辑( c o m p u t m i o n t r e el o g i c ) 提出的算法对于程序模型的大小和时态逻辑公式的长度都是多项式复杂度。他们还 给出怎样不改变算法的复杂度来处理公平性【矧，这对于验证很多依赖某类公平性假 设的并发程序的正确性很重要。同一时期q u i e l l e 和s i f a k i s 为c t l 的一个子集给出 模型验证算法【矧，但他们没有分析复杂性。后来c l a r k e 、e m e r s o n 和s i s t l a 给出一个 改进的算法【矧，它与公式长度和状态迁移图大小的乘积成线性关系。早期的模型验 证系统能验证状态数在1 0 4 到1 0 5 之间的状态迁移图。s i s t l a 和c l a r k e 为各种时态逻 第1 章绪论 辑分析了模型验证问题【4 2 , 4 3 。p n u e l i 和l i c h t e n s t e i n 重新分析了验证线性时间公式的 复杂度f 2 1 】，发现尽管复杂度对公式的长度成指数关系，但对于全局状态图的大小是 线性的。他们认为线性时间模型验证的高复杂度对于短公式仍是可接受的。同年， f u j i t a 基于l t l 公式的验证系统实现了一个t a b l e a u 方法 4 4 1 ，并描述了它在模型中的 验证。 ( 2 ) 基于自动机的形式化验证 自动机理论中的一个重要结论是时态逻辑( u 工) 公式可以转换为一个表示相 同无穷状态序列的b t l c h i 自动机【3 0 , 3 1 】。而系统也用一个b l l c h i 自动机来建模描述， 通过两个自动机的乘积所产生的自动机的判空来进行模型验证。主要步骤： 1 对于性质1 l r ，先得出它的反命题，然后建立b t l c h i 自动机a ( 妒) 2 计算系统s 中每个进程的迁移系统s i 的乘积n s i 得到系统全局行为。要验证 s 的无穷行为的性质，则把s 看作一个受限类型的b u c h i 自动机，其接收集 为整个状态集。 3 计算自动机s 和a ( 妒) 的乘积； 4 检查该乘积自动机所能接受的语言是否非空。 乘积自动机的非空问题可以通过检查是否至少存在一个从初始状态可达的环路 包含一个接收状态，这可以进一步归结为用t a r j a n 的深度优先搜索算法检查图的强 连通分支。当不存在这样一个环路时，表明s 满足性质v 。 自动机理论下最典型的模型验证工具是s p i n 4 , 5 2 。它使用l t l 公式来描述要验 证的性质，系统规范语言p r o m e l a 是一种基于交叠语义的非确定性命令语言。 s p i n 中的进程都被认为是异步的，同步需要进行显式的声明，模型验证算法采用了 o n t h e f l y ( 对系统自动机与性质自动机的乘积进行判空时，可以只在需要时生成系 统自动机的状态的策略) 【8 】和p a r t i a l o r d e r ( 通过避免对独立迁移之间不必要的交叠 进行搜索来减少模型验证的状态数和迁移数) 技术。该工具已经应用在许多通讯协 议的验证中【1 9 1 。 ( 3 ) 状态机模型验证 e m i k k 对s t a t e m a t e 中采用h a r e l 状态机的非形式化语义给出了形式化描 述，并在此基础上以扩展层次自动机e h a 作为状态机的模型，然后把e h a 转换为 s p i n 或s m v 的规范语言来进行验证。该方法给出了两种转换框架，可以分别转换 为顺序或并发代码，并指出顺序代码验证起来比并发代码更有效【3 3 1 。他们据此开发 福建师范大学工学硕士学位论文 出工具m o c e s 来验证s t a t e m a t e 中的状态机，但每次只能验证一个单独的状态 机。j l i l i u s 给出了状态机的操作语义，开发了v u m l 把状态机转换成p r o m e l a 语言【矧。v u m l 可以验证模型的死锁、可达非法状态、违背约束、向终止对象发送 事件、输入队列溢出、延迟事件队列溢出和活锁等错误，但不能验证时态逻辑公式。 d l a t e l l a 等用经过修改的e h a 来表示状态机的一个子集，并根据e h a 语义定义了 状态机的语义【1 0 l 。但是他们没有考虑历史等伪状态，把事件限制为不带参数的信号 和调用，不考虑对象创建和删除、延迟事件以及分支迁移，动作只能产生事件，不 能出现变量和数据，不考虑状态的入口和出口动作。他们把状态机的e h a 翻译成 j a c k 中的标准格式进行验证。 1 4 本文的主要内容 ( 1 ) 基于状态机的图形化表示及其形式化语法语义。 建立图形化的建模环境，利用状态机强大的图形化的描述能力对系统进行描述 建模。定义了与之相关的图形元素符号和形式化语法以及语义。引入了e h a 作为中 间模型。模型验证需要生成系统的l t s ，这里我们使用了e h a 的结构化语义，解决 了状态机对结构化的破坏问题。 ( 2 ) 研究了基于自动机形式化理论的状态机模型验证方法。 我们提出算法根据e h a 的操作语义为状态机生成模型验证所需的l t s 。研究了 用l t l 公式表达模型性质的特点，定义了描述状态机模型的l t l 公式中原子命题的 形式。给出从状态机的l t s 到b u c h i 自动机的转换方法，在为l t l 公式的否定命题 生成b t l c h i 自动机后，通过对两个自动机的乘积进行判空，可以判断模型是否满足 欲验证的性质。当性质不满足时，可以生成由状态机的状况组成的反例路径。 ( 3 ) 缓解状态机状态无限扩张的相关优化工作。 由于状态机本身具有并发和层次等特征以及语义的复杂性，所以在模型验证时 也面临空间爆炸问题。我们通过分析e h a 中存在的层次、并发和事件同步等特征定 义了一组依赖关系，并定义了由多个状态和迁移组成的切片准则。提出根据依赖关 系和切片准则计算e h a 切片的迭代算法。当按一定规则从被验证的i ：r i 。x 性质中提 取切片准则时，证明了得到的切片与原模型对该性质具有相同的满足性。该方法删 除了与被验证的性质无关的层次和并发状态，缓解了空间爆炸问题，并且有助于模 型的分析和理解。 第2 章基于状态机的图形描述及其形式化 第2 章基于状态机的图形描述及其形式化 我们这里所谈到的状态机是基于面向对象建模语言的一种状态图。它提供了丰 富的建模元素和图形表示，从不同的视角和层次支持不同的应用领域的开发。 传统的有限状态机( f s m ) 是平坦、顺序的，难以描述复杂控制系统。状态机 在f s m 的基础上增加层次、并发和通讯机制，是一种强有力的、灵活的状态迁移图。 它可以用下面式子来表达：状态机= 有限状态图+ 深度+ 正交性+ 广播通讯机制f 铝1 。 这里的状态机是经典h a r e l 状态图的一种变体，用来捕获对象的复杂动态行为。 状态机的基本元素包括状态、迁移和动作。状态是对象在一定时期内的存在条件， 迁移是对象对事件做出响应从而改变状态的方式，动作是一种原子行为，可以在状 态机中的许多地方执行，如一个事件激发了迁移、一个状态被进入或离开等。本章 对状态机图形元素及其形式化语法和语义的主要内容进行描述。 2 1 状态机的图形表示及语法 状态机是展示状态与状态迁移的图。状态机所刻画的对象状态分为三种：基本 状态、复合状态和伪状态。我们称非并发的复合状态为或状态；并发复合状态为与 状态，实现状态的层次结构和并发。伪状态又称连接子，包括初始( i n i t i a l ) 伪状态、 浅度历史( s h a l l o wh i s t o r y ) 、深度历史( d e e ph i s t o r y ) 、j o i n 、f o r k 、结合( j u n c t i o n ) 、 选择( c h o i c e ) 和终止( f i n a l ) 等伪状态。表2 1 是相关状态元素的描述与表示： 状态种类 描述表示法 没有子结构的状态 () 基本状态 被分成两个或多个并发子状态的状态，当复合状 【一一一一一 与状态 态被激活时，所有的子状态均被并发激活 包含个或多个不连接的子状态，特别是复合状 pd 或状态 态被激活时，子状态也被激活 特殊状态，表明这是进入状态机真实状态的起点 初始状态 特殊状态，进入此状态表明完成了状态机的状态 终止状态 转换历程中所有的活动 伪状态，它的激活保存了复合状态中先前被激活 的状态 历史状态 福建师范大学工学硕士学位论文 引用子机器的状态，该子机器被隐式地插入子机 ( 删晡e s ) 子机器引用状态 器引用状态的位置 表2 1 状态元素的描述与表示 t a b l e2 1d e s c r i p t i o na n dd e n o t a t i o no fs t a t e s 状态描述了一个对象生命期中的一个时间段。它可以用三种附加方式说明：在 某些方面性质相似的组对象值；一个对象等待一些事件发生时的一段时间：对象 执行持续活动时的一段时间。虽然状态通常是匿名的并仅用处于该状态时对象进行 的活动描述，但它也可以有名字。 在状态机中，一组状态由迁移相连接。虽然迁移连接着两个状态( 或多个状态， 如果图中含有分支和结合控制) ，但迁移只由迁移出发的状态处理。当对象处于某种 状态时，它对触发状态转换的触发器事件很敏感。 状态机的迁移包括如下元素：源状态、目标状态、激发事件、布尔条件和动作。 实际迁移常表示为( s l ，e v e n t c o n d i t i o n 】a c t i o n ，s 2 ) ，e v e n t c o n d i t i o n 称为触发器。 它说明当对象处于源状态s 1 ，事件e v 出现且布尔条件c o n d i t i o n 为真，则执行动作 a c t 后进入目标状态s 2 。s 2 成为活跃状态。简单迁移连接两个状态i 而复合迁移指由 伪状态j o i n ，f o r k , j u n c t i o n 或c h o i c e 连接的简单迁移簇，因此可能有多个源状态和多 个目标状态1 5 0 l 。 动作是状态机在某一点的原子行为。在状态机内，动作可以出现在迁移的执行、 进入状态或者离开状态时。活动( a c t i v i t y ) 是对象在某些状态中执行的行为，发生在 进入状态后且离开状态前。 p l m e c s t n t t m 悸 ! l 湃 雾筹。! 卜一暂l 图2 1d v d p i a y e r 系统模型 f i g 2 1m o d e lo fd v d p i a y e r _ s y s t e m ： n o m ，d j 、 b ；e i 压堆c 赢；v d 蛔s e 捌 一! i 一丽蕊l 第2 章基于状态机的图形描述及其形式化 这里我们暂时不考虑除初始和终止之外的其他伪状态( 深度历史状态、浅度历 史状态等) 、对象的创建与删除以及延迟事件，并且假定事件不带参数，由于复合迁 移均能转化为简单迁移，所以也暂时不予考虑。图2 1 的d v d 播放器例子中， d v d p i a y e r s y s t e m 和o n 是与状态，d v d p i a y e r , d v d s t a t u s ，o f f , i m a g e 和s o u n d 是或状态，其余为基本状态t l 和t 2 表示层间迁移。 这里我们为状态机定义一种形式化的语法，能够很好地用形式化语言描述状态 机。我们在经典状态机理论上加入进出状态执行动作和内部迁移等语法。 用n ，t ，兀，a 分别表示状态、迁移、事件和活动的有限集合，且a 。m 表示有限活动序列集。令r l e n ，e 1 1 ，e x ea 。 基本状态( b a s i c s t a t e ) ：萨 n ，( e n ，e x ) ，类型t y p e ( s ) = b a s i e 。1 1 为状态名，e 1 1 ，e x 分别为进出状态所执行的动作序列。 或状态( 非并发状态o r - s t a t e ) ：s = n ，( s l ，s k ) ，r , t , ( e n ，e x ) 】，类型t y p e ( s ) = o r ，s l ，s k 为s 的子状态，k 0 ，r 是处于激活状态的子状态的编号，默认值为1 。t 是所有子 状态间的变迁集合。处于激活状态的或状态，它的子状态中只有一个处于激活状态。 与状态( 并发状态a n d s t a t e ) ：s = n ，( s l ，s k ) ，a c ，e l l ，e x ，类型t y p e ( s ) = a n d ，s l ，s k 为s 的子状态，k 0 ，对于处于激活状态的与状态s ，它的多个子状态处于激活状态。 因此与状态的子状态称为并发的。 迁移( t r a n s i t i o n ) 仁( n ，i ，s r , e ，g ，a c ，t d j ，h t ) ，n 为状态名，i ，j 分别为变迁源状态、 目标状态的标号，内部层间转换由s r 和t d 来描述，s r 是受限源状态( s o u r c e r e s t r i c t i o n ) ，t d 是受限目标状态( t a r g e td e t e r m i n a t o r ) ，分别表示t 的确切源状态和目 标状态，e 是t 的触发事件，g 是t 的触发条件，a c 是转换时执行的动作序列，h t 是 t 的历史状态，它记录着进入组合状态时所激活的子状态。它有三种类型： n o n e s h a l l o w , d e e p 。n o n e 指激活默认子状态，s h a l l o w 指激活最近的活动的子状态， 如果该子状态还有内层子状态则按照默认值，d e e p 指激活最近活动的基本类型的子 状态。 状态机中的配置机制： 状态机中有多个状态处于激活状态，从状态的元组中是不能判断该状态是否处 于激活状态，必须从最外层状态出发，根据r 的值计算出处于激活状态的状态集合 【5 l 】。如果某状态处于激活状态那么从该状态开始到它的内层状态中所有被激活的状 态组成的集合称为该状态的配置，即c o n f ( s ) 。其定义：c o n f ( n ，j ) = n ) ； 福建师范大学工学硕士学位论文 c o n f ( n ，( s 1 k ) ，r t j ) = 【n ) uc o n f ( s r ) ；c o n f ( n ，( s 1 k ) ，_ 】) = n ) uu 乞1c o n f ( s i ) 。定义函数 c o n f a l l 为s 所有的可能配置的集合。相对与c o n f ，它计算出包括当前的激活的或状 态的子状态集合在内的所有可能的激活的子状态集合。其定义：c o n r a i l ( i n , _ ) = n ) 】； c o n f a l l ( n ，( s 1 d ，r ，t ，j ) = 【( n 】i uc c c o n a a l ( s j ) ，r 墨j 墨k ) u 【 n ) ) ； c o n f a l l ( n ，( ( s 1 d ，j ) = 【n ) uu 乞l c i ic 习e c o n f a l l ( s j ) u n ) 】- 。 或状态s 状态元组中的t 是s 子状态间转换的集合，因此t 中所有转换的最小 公共祖先( l e a s tc o m m o na n c e s t o r ) 都是s 。 用下面一个实例进行说明( 如图2 2 ) ： 一 、 n 1 厂 n 3、厂 n 2、 厂、 ，、 n 4、 n 5 n 6 ，t t t 5 ：d l1 1 1 18 e n t r y e t 2 ：a l t 6 ：b i 一 t 3 ：a l ， | t 1 ：a 1 1 n7 t f n 9 、 t 4 ：c l 心 力 名 图2 2 状态图的一个实例 f i g2 2a n i n s t a n c eo fs t a t em a c h i n e 此状态图中的状态项定义如下： s l m n l ，( s 2 ，s 3 ) ，( ， ) 】； s 2 = n 2 ，( s 4 ，s 5 ) ，r , t l ，t 4 ，t s ，t 6 ) ，( ， ) 】； s 3 = 【n 3 ，( s 6 ，s 7 ) ，r ， t 2 ) ，( ， ) 】； s 4 = n 4 ，( s s ，s 9 ) ，r t 3 】- ，( ， ) 】； s 5 = n 5 戈 ， ) 】； s i - h i ，( ， ) 】( 6 = i _ 9 ) ；s 1 是与状态，s 2 ，8 3 和s 4 是或状态，其余s 5 s 9 是基本状态。其 中s 4 有出e 1 动作序列，s 5 有入口动作序列。这里的或状态选用它的默认子状态作为 它的初始激活状态。 此状态图的迁移项定义如下： t l = ( n l ，4 ，彩，a ， ，囝，5 ，n o n e ) ； 第2 章基于状态机的图形描述及其形式化 t 2 = ( n 2 ，6 ，彩，如 ，j 2 j ，7 , n o n e ) ； t 3 = ( n 3 ，8 ，f 2 j ，a ，o ，9 , n o n e ) ； t 4 = ( n 4 ，4 ，o ，( 9 ，c ， ，囝，5 , n o n e ) ； t s = ( n s ，5 ，f 2 j ，d ， ，囝，4 ，s h a l l o w ) ； t o - ( n 6 ，4 ，乃，b ， ，彩，5 , n o n e ) ； t 4 是内部迁移，在t 5 中使用了历史状态。 2 2 状态机的语义 在经典状态图的基础上，引入入口和出口动作，历史状态，并且用结构化操作 语义规则( s o s ) 来定义状态机的语义，它由事件来触发，其执行的基本原理为： 一个事件队列，它保存到达的事件，一直到它们被派遣出； 一种事件派遣机制，在事件队列中选择事件并把它从队列中去掉： 一个事件处理器，处理派遣出的事件。 1 事件 事件由系统内部或环境中某些动作产生，被发送到一个或多个目标。事件在被 目标接收时放到事件队列中，当被派遣时从事件队列中取出送给状态机处理，处理 完后就不再可用。事件的接收、派遣和处理完毕之间无时间假设。事件是发生在时 间和空间上的一点的值得注意的事情。它在时间上的一点发生，没有持续时间。如 果某一事情的发生造成了影响，那么在状态机模型中它是个事件。事件可以分成 明确或隐含的几种：信号事件、调用事件、修改事件、时间事件等。表2 2 是几种 事件类型及其描述。 事件类型描述语法 调用事件接受等待应答的对象的明确形式的同步请求 o p ( a ：t ) ? 改变事件对布尔表达式