（计算机应用技术专业论文）基于petri网的嵌入式系统建模与验证研究.pdf

摘要 摘要 随着嵌入式系统在各个领域的广泛应用，嵌入式系统变得越来越复杂。在嵌入式系 统设计中采用模型的方法，有利于确保系统的正确性，缩短开发周期，降低开发费用。 本文以p e r t i 网为建模工具，对嵌入式系统的建模和分析验证进行了一些研究。 嵌入式系统具有实时性、并发性等特点，并要求高可靠性和正确性。为了设计具有 这样特点的系统，设计过程必须基于一个形式化描述，以捕获嵌入式系统的这些特点。 p e t r i 网对这类系统是一个很好的描述方法：可以表示并行和连续活动，并且很容易捕 捉不确定性行为。但传统的p e t r i 网缺乏时间概念和数据表达力，不能很好的描述嵌入 式系统的实时性要求和数据流。针对传统p e t r i 网的这些缺点，本文提出基于p r e s + 的 嵌入式系统的建模与分析验证研究。 首先，介绍嵌入式系统的一个形式化计算模型p r e s + ，可以描述嵌入式系统的一些 重要特征，其中，托肯携带数据信息，变迁执行数据的转换，时间通过与变迁相连的活 动期限来捕获。同时，引入p r e s + 模型的分层机制和组合修改操作。分层机制使模型能 够有条理的构建，由简单的单元组件构成，使得设计师在每个描述级上都可以很容易理 解；组合修改操作，通过增加或减少模块来改变其功能或状态，从而以最小的影响，实 现了网模型的修改，并有效保存了系统的性质，使系统在修改后不需要再重新验证其性 质。 其次，介绍了系统模型的分析与验证，对基于p r e s + 建模的嵌入式系统，分别提出 两种方法，对它进行分析验证。第一种为形式化验证方法，利用模型检测来验证系统的 一些性质，将其表示成时序逻辑公式。介绍了一个转换程序，把p r e s + 模型转换成时间 自动机t a ，并使用模型验证工具u p p a a l 对其进行分析验证；第二种方法，通过程序 模拟p e t r i 网中各个库所中托肯的变化情况，模拟p e t r i 网的动态行为，从而达到分析验 证的目的。最后，提出一种策略，使用正确性保留等价转换，对p r e s + 模型进行简化， 从而提高其验证效率。 关键词：嵌入式系统、p e t r i 网、p r e s + 、建模、层次、组合与修改、分析与验证、 时间自动机、等价转换 a b s t r a c t a b s t r a c t e m b e d d e ds y s t e m sb e c o m e sm o r ea n d m o r ec o m p l i c a t e dw i t hi t sw i d e s p r e a du s ei na v a r i e t yo fd o m a i n s m o d e l i n ga p p r o a c hc o u l di m p r o v et h ec o r r e c t n e s s ，s h o r t e nt h ep e r i o do f d e s i g n ，a n dr e d u c et h ec o s ti ne m b e d d e ds y s t e md e v e l o p m e n t b a s eo np e t r in e t ，w ed i ds o m e r e s e a r c ho ne m b e d d e ds y s t e mm o d e l i n ga n dv e r i f i c a t i o n e m b e d d e ds y t e m sa r ec h a r a c t e r i z e db yt h e i rd e d i c a t e df u n c t i o n ，r e a l - t i m ea n dc o n c u r r e n t b e h a v i o r , a n dh i g hr e q u i r e m e n t so nr e l i a b i l i t ya n dc o r r e c t n e s s i no r d e rt od e v i s es y s t e m sw i t h s u c hf e a t u r e s ，t h ed e s i g np r o c e s sm u s tb eb a s e du p o naf o r m a lr e p r e s e n t a t i o nt h a tc a p t u r e st h e c h a r a c t e r i s t i c so fe m b e d d e ds y s t e m s p e ：t r in e t sa r ea l lg o o dr e p r e s n e t a t i o nf o rt h i ss o r to f s y s t e m s ：i tc a l lr e p r e s e n tp a r a l l e la s w e l la s s e q u e n t i a la c t i v i t i e sa n de a s i l yc a p t u r e n o n d e t e r m i n i s t i cb e h a v i o r s h o w e v e l t h et r a d i t i o n a lp e t r in e tm o d e ll a c k st h en o t i o no ft i m e a n dd a t ae x p r e s s i o n ，i tc a nn o tr e p r e s e n tt h er e a l t i m er e q u i r e m e n ta n dd a t af l o w t om e e tt h e s e p r o b l e m s ，t h i sp a p e rp r o p o s e dt h er e s e a r c ho ne m b e d d e ds y s t e mm o d e l i n ga n da n a l y s i sb a s e o np r e s + f i r s t w ep r e s e n taf o r m a lc o m p u t a t i o nm o d e lp r e s + f o re m b e d d e ds y s t e m t h em o d e l c a n c a p t u r e s o m e i m p o r t a n t f e a t u r e so fe m b e d d e d s y t e m s ，i n w h i c ht o k e n s h o l d i n f o r m a t i o n ，t r a n s i t o n sp e r f o r mt r a n s f o r m a t i o no fd a t a ，a n dt i m i n gi sc a p t u r e db ya s s o c i a t i n g l o w e ra n du p p e rl i m i t st ot h ed u r a t i o no fa c t i v i t i e sr e l a t e dt ot r a n s i t i o n s f u r t h e r m o r e ，i n t r o d u c e t h eh i e r a r c h ym e c h a n i s ma sw e l la st h ec o m p o s i t o na n dm o d i f i c a t i o no p e r a t i o n h i e r a r c h yi sa u s e f u lt o o lt h a ta l l o w st h es y s t e mt ob ec o n s t r u c t e di nas t r u c t u r e dw a yb yc o m p o s i n ga n u m b e ro ff u l l yu n d e r s t a n d b l ee n t i t i e s ；t h ec o m p o s i t i o na n dm o d i f i c a i o no p e r a t i o nc a n c h a n g et h ef u n c t i o n so rs t a t e s a d db ya d d i n go rr e d u c i n gt h em o d u l e ，t h u s ，i tc h a n g e st h en e t m o d e li nal o w e re f f e c t ，a n dp e r s e r v e st h es y s t e mp r o p e r t i e s ，s ot h a tw en e e dn o tt ov e r i f yi t s p r o p e r t i e sa f t e rc h a n g e da g a i n s e n c o n d ，w ep r e s n e tt h ea n a l y s i sa n dv e r i f i c a t i o no ft h es y s t e mm o d e l ，p r o p o s et w o m e t h o d st oa n a l y z ea n dv e r i f yt h es y s t e m sr e p r e s e n t e di np r e s + t h ef i r s tm e t h o di st h e f o r m a lv e r i f i c a t i o n ，i nw h i c hm o d e lc h e c k i n gi su s e dt op r o v ew h e t h e rt h es y s t e mm o d e l s a t i s f i e si t sr e q u i r e dp r o p e r t i e se x p r e s s e da st e m p r o a ll o g i cf o r m u l a s i n t r o d u c eat r a n s l a t i o n p r o c e d u r et h a tt r a n s l a t et h ep r e s + m o d e lt ot i m ea u t o m a t a ，a n dt h e na n a l y z ea n dv e r i f yt h e t am o d e lu s i n gt h eu p p a a l ；t h es e c o n dm e t h o d ，t h r o u g ht h ep r o g r a mt os i m u l a t et h ec h a n g e s o ft h et o k e ni ne v e r yp l a c e s ，s i m u l a t et h ed y n a m i cb e h a v i o ro fp e t r in e tt oa c h i e v et h ea n a l y s i s a n dt e s t i n gp u r p o s e s b e s i d e s ，p r o p o s eas t r a t e g y , s i m p l i f yt h ep r e s + m o d e lt h r o u g ht h e c o r r e c t n e s s p e r s e r v a t i o ne q u i v a l e n tt r a n s l a t i o n ，i no r d e rt oi m p r o v et h ev e r i f i c a t i o ne f f i c i e n c y k e y w o r d s ：e m b e d d e ds y s t e m ，p e t r in e t ，p r e s + ，m o d e l i n g ，h i e r a r c h y , c o m p o s i t o na n d m o d i f i c a t i o n ，a n a l y s i sa n dv e r i f i c a t i o n ，t i m ea u t o m a t a ，e q u i v a l e n t - t r a n s f o r m a t i o n i i 独创性声明 本人声明所呈交的学位论文是拳人在导师指导下进行的研究工作及取 得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文 中不包含其他人已经发表或撰写过的研究成果，也不包含本人为获得江南 大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志 对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。 签名： 型直 日 期：2 1 晕f 2 ：哗 关于论文使用授权的说明 本学位论文作者完全了解江南大学有关保留、使用学位论文的规定： 江南大学有权保留并向国家有关部门或机构送交论文的复印件和磁盘，允 许论文被查阅和借阅，可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文， 并且本人电子文档的内容和纸质论文的内容相一致。 保密的学位论文在解密后也遵守此规定 签名： ! 訇盎 导师签名： 日 期： 第一章绪论 第一章绪论 1 1 研究背景 嵌入式系统是将软件和硬件集成在一起的专用计算机系统，嵌入式系统涉及的领域 有软件工程、计算机硬件、数字电子学、模拟电子学、电气工程、数据通信等。近几年 来，由于应用需求的巨大增长，嵌入式系统得到了迅猛发展。从航天飞机、智能机器人、 汽车电子、网络设备，到家用电器、手机、网络交换器，以及消费者电子产品等，都是 大量使用嵌入式系统的应用领域，嵌入式系统已普遍深入到我们的日常生活中【l 】。 随着嵌入式应用的不断增长，嵌入式系统需求的复杂性，不确定性也在不断的提高， 系统规模也在逐步扩大，而产品的研发周期又在不停的缩短，这给嵌入式系统开发带来 了新的挑战1 2 l 。 传统的嵌入式系统设计方法在设计复杂的嵌入式系统，比如分布式嵌入式系统时， 常常需要反复多次设计软硬件，不仅浪费了大量时间和金钱，而且也无法将产品及时推 向市场。因此在嵌入式系统设计中，系统建模是非常重要的。近几年来，一些学者将形 式化语言引入到嵌入式系统的设计中，并取得了许多研究成剁3 7 1 。 建立一个良好的系统模型，在系统设计的初级阶段对系统进行模拟和仿真，对系 统的有效性、稳定性和可靠性进行分析，及时对系统设计进行相应的优化并且及时发现 系统级的错误，可以避免不必要的损失。 p e t r i 网是一种使用图形方式对系统进行需求规格说明的技术，是一种可以用来定义 多进程、多任务系统的数学模型，易于描述系统的并发、竞争、同步等特征，并可用 于评价和改进系统【8 9 j 。 p e t r i 网已越来越多的用于嵌入式实时系统的建模、评估和分析。p e t r i 网允许建立嵌 入式系统的较为全面的模型，包括系统的计算部分，目标硬件以及系统环境，如传感器、 执行器等。另外大量的仿真软件可以用于模型的调试、性能评估，也可能用于某种性质 的自动分析【1 0 l 。 1 2 研究现状 近几年，关于嵌入式系统高层级设计方法的研究引起了广泛的重视和研究兴趣，欧 美等国相继开展了大量研究工作，取得了一批重要研究成果【1 1 l2 1 。但是，直到今天，尚 未确立一种公认的、统一的、成熟的设计方法。 高层级设计方法需要解决的首要问题是系统功能描述。系统功能描述的主要手段是 建立合适的模型。其模型必须能够适应嵌入式系统的特点，能够很好地描述系统的特性。 嵌入式系统的特性包括：并发性，状态迁移，层次，程序结构性，行为可完成性，可通 信性，可同步，异常处理能力，可选择性( 非定性) ，可定时性【1 3 1 。 目前，形式化的嵌入式系统建模方法主要有f s m 和p e t r i 网两种，u m l 是的半式 化模型。f s m 不能描述并发行为，u m l 不可执行，两者都有一定的局限性。相比而言， p e t r i 网是一种比较完善的形式化建模方法，其精确、形式化的数学定义，严格规范的推 江南大学硕士学位论文 导方法，较好的工具支持，特别适合描述系统的控制流、并发特性和异步为【1 4 ”】。 p e t r i ( p n ) 网t 1 6 】的概念最早是由西搏的c a p e t r i 博士于1 9 6 2 年提出来的，7 0 年 代以后，p e 仃i 网理论在欧美一些国家得到了迅速的发展，并被广泛应用于计算机科学技 术和其他许多学科领域。作为一种系统描述和分析工具的理论模型，同其他一些描述方 法相比较，p e t r i 网结拘理论更便于描述并发现现象和模拟平行系统。 p e t r i 网能够对计算机系统进行形式化描述、验证、性能评价和辅助设计，在嵌入式 系统建模领域具有优势。但是，基本p e t r i 网不具有面向对象特征和层结构，对数据流 的描述能力较弱。因此，研究适合嵌入式系统建模的p e t r i 网，成为形式化建模方法的 研究热点。 国外的研究主要有基于高级p e t r i 网的嵌入式系统的动态可塑性【1 ”、实时性【1 8 】的研 究，以及嵌入式软硬件的协同设计【1 9 】的研究等。随着嵌入式系统的广泛应用，产生了多 种扩充的p e t r i 网模型。其中，最典型的有o p n e t s ( o b j e c to r i e n t e d h i g h _ _ l e v e lp e t r in e t s ) 拉、e t p n ( e x t e n d e dt i m ep e t r in e t s ) 瞄l j 和p r e s ( p e t r in e t b a s e dr e p r e s e n t a t i o nf o r e m b e d d e ds y s t e m s ) t 2 2 1 。 近年来，国外一些实验室提出了一些使用p e t r i 网建模嵌入式系统的方法论。非商 业的系统包括c o d e s i g n ，p i 迮s + ，c a m a d ，p r t - n e tb a s e ds e a m l e s sd e s i g n 等。 国内基于p e t r i 网的嵌入式系统研究尚处于起步阶段，主要是对于嵌入式的分布性、 实时性的研究。张海涛等在对建模的实时调度，尤其是分布式实时嵌入式系统的实时调 度方面有一定的研究【2 3 , 2 4 】；另外，面向对象p e t r i 网在嵌入式系统中的应用【2 5 1 ，也有不 少的学者研究，并取得一定成果，但总体水平与国外仍有一定的差距。 因此，开展相关课题研究，有利于促进我国在该领域的研究水平。 1 3 本文的研究工作及其意义 本文主要研究基于p e t r i 网的嵌入式系统的形式化设计描述，包括系统建模，模型 扩展及修改，模型分析和验证。具体研究内容如下： 首先，定义了扩展p e t r i 网这一计算模型。p r e s + 可以在不同层次上描述系统，它 可以很容易的捕捉到顺序和并发活动，以及非确定性。托肯携带数据信息，变迁执行数 据的转换，时问通过与变迁相连的活动期限来捕获。同时，它还可以进行分层和组合操 作。分层机制使模型能够有条理的构建，由简单的单元组件构成，使得设计师在每个描 述级上都可以很容易理解；组合修改操作，通过增加或减少模块来改变其功能或状态， 从而以最小的影响，实现了网模型的修改，并有效保存了系统的性质，使系统在修改后 不需要再重新验证其性质。 对于安全性要求很高的实时系统，其正确性是一个至关重要的因素。一个错误可能 会造成很大的损失。因此，在处理这类系统时，必须证明系统的正确性。本文提出了基 于p r e s + 描述的系统的形式化验证方法。使用模型检测来证明系统的某些性质。介绍了 将p r e s + 模型转换成时间自动机的一个系统化程序，并用模型验证工具u p p a a l 对其进 行分析验证。最后，本文还提出一种提高验证效率的方法，将模型转换成初始模型，然 后简化它，但仍然保存其特定性质。这种转换方法通过使用保留正确性的转换，可以减 2 第一章绪论 少模型，降低验证成本，并提高验证效率。 1 4 本文的基本结构 本文基于p e t r i 网对嵌入式系统的建模与分析验证进行了一些针对性、探索性的研 究，全文由以下三部分组成： 第一部分：引言部分 该部分由前两章组成。第一章介绍了研究背景以及国内外的研究现状，并阐述了本 文的主要研究工作及其意义。第二章主要介绍了几种传统的嵌入式系统的模型和基于 p e t r i 网的嵌入式系统模型，并比较了它们的优缺点。 第二部分：基于p e t r i 网的嵌入式系统的建模及其分析验证 该部分是本文的重点，由第三，四章组成。第三章详细阐述了基于p r e s + 的嵌入式 系统的建模，针对嵌入式系统的自身特点，引入时间性和功能性的描述；在此基础上， 引入分层和组合修改机制，使模型能够更有条理的构建和修改。第四章则是对基于 p r e s + 描述的系统进行分析和验证。提出两种验证方法，一种为形式化验证方法，将 p r e s + 模型转换成时间自动机t a 模型，并使用现有的模型验证工具u p p a a l 对其进行模 拟分析和验证；另一种方法，通过程序模拟p e t r i 网中各个库所中托肯的变化情况，模 拟p e t r i 网的动态行为，从而达到分析验证的目的。此外，还提出一种提高验证效率的 方法，使用正确性保留等价转换，对p r e s + 模型进行简化，可以减少模型，降低验证成 本，从而提高其验证效率。 第三部分：结束语 该部分对全文进行了总结，综述了论文的研究工作，并评价了基于p e t r i 网的嵌入 式系统建模的优点与不足，最后探讨了基于p e t r i 嘲的嵌入式系统研究的进一步方向。 江南大学硕士学位论文 第二章嵌入式系统的模型概述 2 1 嵌入式系统的特点 嵌入式系统用于大量的应用，其应用领域将继续扩大。尽管应用领域的多样性，一 般嵌入式系统都有如下特点： 专用性，面向特定的任务。嵌入式系统一般面向特定的应用，即，系统执行的一 组功能都是事先定义好的，一旦系统配置好，其功能在其正常运行期间是不能修改的。 一旦任务改变，系统可能需要重新设计。 实时性。由于环境的相互影响，嵌入式系统的正确行为不仅仅取决于计算的逻辑 结构，还依赖于结果产生的时间。因此，嵌入式系统必须严格履行时间要求，系统的运 行速度，相应时间必须满足应用要求。 高可靠性。嵌入式系统对可靠性和正确性有较高的要求。在安全至关重要的应用 中，如航空电子和汽车电子，一个错误可能会造成灾难性的后果。因此，必须设计相应 的软硬件机制来确保系统操作的可靠性和正确性。 低功耗。对许多嵌入式系统，尤其是移动设备，能源消耗是一个重要的考虑因素。 对于这类设备，关键是尽可能高效率的使用能源。 异质性。嵌入式系统包括硬件和软件元素。硬件组件，如专用集成电路和现场可 编程门阵列，提供了许多应用中的速度和低功耗需求。软件组件，如可编程处理器，为 新增了功能的扩展系统增加了灵活性，并为新一代产品增添了更多的功能。 设计具有这些特点的系统是一项艰巨的任务。嵌入式系统不仅要实现预期的功能， 还必须满足不同的相互竞争的制约因素( 电力和能源消耗，性能，正确性，尺寸，成本， 灵活性，等等) 。此外，嵌入式系统日益增长的复杂性对设计师是一个巨大的挑战。 2 2 嵌入式系统的设计流程 嵌入式系统的一个通用的设计流程如图2 1 所示。 1 需求分析 在这一阶段，开发人员要和用户之间进行充分的交流，得出经用户认可、明确的系统实 现描述。因为用户给出的需求往往是不完整，表述方式是非形式化的，必须经过提炼， 形成精确的、形式化的需求描述。 嵌入式系统的需求分析一般可分为功能性需求和非功能性需求分析。非功能性分析 包括性能、价格、物理尺寸和功耗等。 分析确定需求的最有效方法是建立系统模型，通过模型可以模拟系统的功能，让用 户理解系统工作过程，以及如何与系统进行交互。常用的分析方法有流程图、数据流图、 结构图、w a m i e r 图、i o p 图、u m l 用例图等。 2 规格说明 系统的规格说明开描述了系统的功能，性能，成本，能源以及设计其他方面的限制。 4 第二章嵌入式系统的模型概述 它只声明了系统的功能，但并不给出具体的实施细节，即，它指定了系统该做什么，但 并不详细说明该如何执行。许多不同的规格说明语言都适用于嵌入式系统的设计。系统 规格说明可以考虑使用各种不同的语言，从自然语言到具有很强形式化语义的语言。但 最好使用具有精确语义的语言来指定系统，这样从设计流程的初始阶段就可以使用工具 来协助设计师。 3 系统建模 一旦给出系统的规格说明，设计者必须提出一个系统模型来捕捉规格说明的功能属 性以及非功能属性。一个健全的系统模型，设计师可以捕捉到系统的功能以及非功能限 制，验证系统的正确性，在系统合成过程中形式化的推导出完善步骤，并在整个设计流 的不同阶段使用计算机辅助设计工具。已有大量的形式化建模方法用于描述嵌入式系 统，这些计算模型包括不同的风格，特点和应用领域。 4 体系结构设计 一旦获得系统模型，必须决定系统的基本体系，即，选择组件的类型和数量以及连 接它们的方法。组件包括各种处理器内核，定制模块，通信元素如总线和缓冲，i o 接 口，以及内存。 5 划分映射 根据设计的体系结构，在划分和映射阶段，系统模型任务或进程分组并被映射到所 选的组件上。嵌入式系统的软硬件划分是指将到系统功能物理划分为定制的集成电路 ( 硬件组件) 和可编程处理器( 软件组件) 。将系统划分为硬件和软件对最终设计的成 本和性能有着巨大的影响。 6 组件设计 组件设计包括硬件组件和软件组件设计。 对于硬件设计，首先选择合适的处理器，然和要确定采用的系统总线、所需要的内 存、需要苦熬制的各种接口、电源等。 对于软件设计，首先选择是否需要操作系统，以及选择哪种操作系统，然后画出流 程图，选择合适的编程语言、合适的程序结构等。 对于分布式嵌入式系统，需要选择适当的通信硬件、通信协议，最后编写通信软件。 7 系统集成与测试 系统集成将开发好的软硬件构件集成到一个系统中测试，验证功能和指标参数。在 这一阶段通常会发现错误，即使已经调式通过的构建，在系统集成测试时也可能由于接 口连接问题或系统高负荷问题产生错误。因此，发现问题并解决问题是系统集成测试阶 段的关键。 设计流程通常需要迭代，它有时需要返回到前面的步骤，因为一些设计目标无法实 现，因此，需要寻求不同的设计方案，通过修改在之前设计阶段采取的决策。 江南大学硕士学位论文 图2 - 1 嵌入式系统设计的一般流程 f i g 2 1ag e n e r i cd e s i g nf l o wf o re m b e d d e ds y s t e m 2 3 嵌入式系统建模的常用方法 2 3 1 有限状态机 有限状态机( f s m ) 2 6 1 为描述控制系统最常用模型，由有限个状态和相互之间的转 移构成，在任何时刻系统总是处于个待定的状态。当接受到一个输入事件时，状态机 产生一个输出，同时伴随着状态的转移。系统的状态概况了对过去输入处理情况的全部 信息，系统只需要根据当前所处的状态和面临的输入就可以决定系统的行为。每当处理 了当前的输入后，系统的内部状态也就发生变化。 有限状态机是实时系统设计中的一种数学模型，是离散的输入输出系统，是一种重 要的、易于建立、应用比较广泛、以描述控制特性为主的建模方法，它可以应用从系统 分析到设计的所有阶段。其形式化表示为一个五元组胙p ，6 ，s o ，刁 其中，s = s l ，s 2 ，o oo p 勘) 是一个有限的状态集合；表示该系统能接受的所有事件 的集合；变迁函数万：s x = s ，称为状态转移函数，它描述了系统中每个状态转移到 其他状态的可能性，只要该事件发生，就会发生转换。常用定义式6 ( s ，口) 邓2 表示在状 态s ，下接受事件a 转如指定的新状态s 2 ；8 0 s 是系统的一个特殊状态，一般是系统启 用时的初始状态。z c _ s 是终结状态的集合。 通常用有向图来表示有限状态机。其节点表示状态。若在状态s ，接受到某个输入事 件口后转向状态勋，就在图中画一条从s ，到勋的带箭头的弧线，并在弧线上标记a 。 6 第二章嵌入式系统的模型概述 图2 - 2 一个有限状态机的例子 f i g 2 2a ne x a m p l eo ff s m 如图2 2 所示，显示了一个有限状态机的例子，共有四个状态s ，印，趵，趵，四个 事件a , b , c , d ，图中清晰的显示了各个状态的转换关系。 f s m 对控制占主导的系统建模具有优势，但是，它存在一些不足。一是当系统规模 变大，状态数目增加会引起“状态爆炸”；另一个是模型没有层次化结构，对于复杂系 统的建模，往往难以理解。最重要的是，任何时刻系统只能有一个状态，无法表示并发 行为，不能描述异步并发系统。 不少文献提出f s m 的扩展模型。协同设计有限状态机( c f s m s ) 是p o l i s 设计环 境中的一个基本计算模型。c f s m 是f s m 的扩展，包括控制部分和数据计算部分。每 个c f s m 同步行为从自己的观点。一个系统由若干个c f s m s 组成，相互之间通过信号 异步通信，信号以事件的形式携带信息。这种语义提供了一个g a l s 模型：全局异步( 在 系统级) 和逻辑异步( 在c f s m 级) 。c f s m s 主要应用于面向控制的系统。 为了使其跟适合于面向数据的系统，f s m 模型通过一如一组内部变量，扩展为带有 数据通道的有限状态扩展机( f s m d ) 。变迁关系不仅仅依赖于目前的状态和输入信号， 还依赖于一组内部变量。尽管引入变量到f s m d 模型，有助于减少当前状态，但它缺乏 对并发和层次的支持，因为状态爆炸的问题仍然存在。 f u n s t a t e 模型由一个网络和一个有限自动机组成。网络对应于系统的数据密集部分。 网络由存储单元，函数，以及连接存储单元和函数的弧组成。数据由存储单元中的值托 肯表示。网络中的函数的激活由状态机控制。在f u n s t a t e 模型中，任意数量的组件( 网 络和f s m ) 可以安排在等级结构中。 2 3 2 状态图表 通过f s m 的不足，得到了许多改进的f s m 模型，输入b f s m ，c f s m ，s t a t e c h a r t s 等。 其中s t a t e c h a r t s 建模能力较强，下面分别予以介绍。 a ) b f s m ( b e h a v i o rf i n i t es t a t em a c h i n e ，行为有限自动机) 一个b f s m 是输入输出按照时间排序的有限状态机，例如，在输入和输出之间增加 了线性不等式时间限制。系统可以通过b f s m 网络描述、每个b f s m 之间的通信是同 步的。只有通过网络的直接模拟，才能得到并分析b f s m 的网络行为。 b ) c f s m ( c o d e s i g n f i n i t es t a t em a c h i n e ，协调设计有限状态机) c f s m 与有限状态机非常相似，将一套输入转换成输出，并且也有内部的状态。c f s m 使用有限的非零反应时间代替f s m 中同步的事件通信。c f s m 包括输入和输出事件类 7 江南大学硕士学位论文 型集及转换关系。转换关系是一套因果关系对，每个原因和响应是一套事件名字和值。 每个转换由输入事件触发，在有限的非零事件后产生输出事件。 c f s m 是一个软硬件协同设计的形式模型，它基于f s m ，主要用于相对低的算法复 杂度、面向控制的系统。 c ) s t a t e c h a r t s z 7 】( 状态图表) 状态图表是从经典f s m 扩展得到的图形规范语言。它增加了分级、时间规范、并 行和同步。通过并行和序列操作可以实现不同的层次。在各个层次上都仍然服从f s m 的状态转换的定义，而各个状态的时间可由线性不等式确定。 图2 3 显示了一个状态图表的例子，处于较高层次的状态彳分解成三个并行的状态 bc ，d 。而状态e c d 又进一步分解成顺序的状态，比如，状态b 分解成顺序的状态s d ， s l ，印。状态彳芦d ，s 3 ，彤，是初始的状态，用一端为黑点的箭头表示。 图2 - 3 一个状态图表的例子 f i g 2 - 3a ne x a m p l eo fs t a t e c h a r t 状态图表通过等级组合和并发扩展f s m s 。一个特定的状态可以由子状态组成，即， 在高级状态被解释成其中的一个子状态。这样，s t a t e c h a r t s 通过缩减描述，避免了状态 爆炸。此外，通过线性不等式的形式指定时间。但s t a t e c h a r t s 的问题是，模型不能描述 面向数据的模型。 2 3 3 数据流图 数据流图 2 8 1f d a t af l o wg r a p h ，d f g ) i 妇结点集合和边集合构成，主要用于数据传输 系统分析。图2 4 是一个数据流模型例子。其中，方框内是数据，圆圈内是操作。 图2 4 一个数据流图的例子 8 第二章嵌入式系统的模型概述 f i g 2 - 4a ne x a m p l eo fd a t af l o wg r a p h 数据流图适合模型以数据为主的系统，如d s p 系统，也具有层次化建模能力，能 够胜任复杂系统的建模。计算密集型系统可以很方便的通过有向图来表示，节点描绘操 作，弧捕获任务间的数据依赖关系。只有当所需的操作数可用时，才会执行计算。然而， 传统的数据流图模型在时态描述和控制流描述方面有明显缺陷。 2 3 4p e t r i 网 用p e t r i 网【2 9 】来建模系统已广泛应用于许多科学领域的建模。经过多年发展p e t r i 网 已经成为一个易于理解、功能强大的建模语言，可以描述系统的并发、异步、同步等特 征。 经典p e t r i 网的结构表示如下 n = ( p 。t i 0 m o ) 其中，p = p l , p 2 ，砌) 是库所的有限集合，m 0 为库所的个数；产 t l , t 2 ，岛) 是变迁的有限集合，n 0 为变迁的个数； p p 是一组输入弧的有限集，定义了 库所到变迁间的关系流；d ：取p 一是一组输出弧的有限集，定义了变迁到库所间的 关系流；m o ：尸_ 是网初始标记，是一个向量，其第i 个元素表示第f 个位置中的 托肯数目。 在建模时，库所表示各种资源及状态，变迁表示各种事件。如图2 5 所示，显示了 一个简单经典p e t r i 网例子。这个例子显示了p e t r i 网的基本功能。在库所岛处， 由于变迁t ，和t 2 竞争库所p ：的托肯，产生了冲突。假定变迁t i 触发了，就产生了两 路并行的进程，这两路进程可以说异步，但是在变迁t 6 处达到了同步。 p 2 t 3 p j t 5 p 7 图2 - 5 一个简单的p e t r i 网 f i g 2 - 5a ns i m p l ee x a m p l eo fp e t r in e t 这种数学形式化方法已经开发多年，定义其结构和激活规则，使得p e t r i 网成为一 个易于理解的强大模型。已有大量关于p e t r i 嘲的理论成果和实用工具被开发。但在建 模嵌入式系统方面，仍然存在一些缺点： p e t r i 网的体积往往比较大，即使是模型相对较小的系统。缺乏分层和组合，如果 利用常规模型，往往很难描述和理解复杂系统。 传统的p e t r i 网模型缺乏时间的概念。然而，在嵌入式应用领域，时间是一个至 关重要的因素。 9 江南大学硕士学位论文 p e t r i 网缺乏公式计算的表达力，其托肯只是简单表示为“黑点 。 下面将介绍一些用于描述嵌入式系统的p n 形式化方法。 着色p e t r i 网【3 0 1 ，此模型中托肯可以“有色”，即托肯可以表示数据。变迁库所间的 弧上含有表达式，描述与其相连的变迁的行为。即，变迁描述行为，托肯携带数值。c p n 模型支持层次结构，并建立了强大的数学理论。但c p n 的问题是，时间并不能在模型 中定义。虽然可以将时间表示为托肯的其他类型的值，但由于不能给定激活的时间顺序， 容易发生时间的不一致性。 双变迁p e t r i 网( d t p n ) 3 1 l 是另一种计算模型，其控制流和数据流紧密相连。双变 迁p e t r i 网有两类变迁( 控制变迁和数据变迁) ，并有两类弧( 控制流和数据流弧) 。托 肯可以携带数值，并通过数据变迁的激活而改变。控制变迁可以含有基于托肯值的哨， 哨连接控制域和数据域。但d t p n 也没有明确的时间概念，而且，它不支持层次结构。 2 4 本章小结 本章简述了嵌入式系统的特点，指出了复杂的嵌入式系统设计所面临的问题。简单 介绍了嵌入式系统设计的一般流程。分析并比较了目前常用的几种设计建模方法的优缺 点和适应领域。并分析了基于p e t r i 网对嵌入式系统进行建模的优点及其不足之处。本 章内容为深入开展嵌入式系统p e t r i 网建模设计方法研究奠定了基础。 1 0 第三章基于p r e s + 的实时嵌入式系统建模 第三章基于p r e s + 的实时嵌入式系统建模 3 1 基本p e t h 网 p e t r i 网模型适用于多种类型的系统。它们可以作为一个图形和数学建模工具，广泛 的用于许多应用领域。一个p e t r i 网可以看成一个有向二分图( 由两种节点组成，即库 所和变迁) ，初始状态初由始标识表示。经典p e t f i 网的定义如下： 定义3 1 ：p e t r i 网( p e t r in e t ) p e t r i 网- 俨，t ，i ，0 ，m o ) ，其中 p = p l ，p 2 ，p m 是库所的有限集合 仁 t t ，t 2 一，岛) 是变迁的有限集合 i c _ p t 是一组输入弧的有限集，定义了库所到变迁间的关系流 o c _ t p 是一组输出弧的有限集，定义了变迁到库所间的关系流 m o ：p n o 是网初始标记 图3 - l 显示了p e t r i 网的一个列子，p = 溉，mp c ，肌 ，丁= ，t 2 ，= ，r 戊p 6 ，f ，) ， 锄，功) ，0 = ( ，p c ) ，( t e ，p d ) ) 。库所用圆表示，变迁用方框表示，弧用箭头表示。 图3 - 1 一个p e t r i 网 f i g3 - 1 a p e t r i n e t 在经典p e t r i 网模型中，一个标识m 分配每个库所一个非负整数m 例，表示库所p 中的托肯数目。在图3 1 中的模型中，m o ( p 9 = 2 ，m o ( p b ) = 1 ，m o ( p j = 例= 0 。 定义3 2 ：前集与后集 变迁，t 的前集仁仞尸ip ，力，) 为，的输入库所集，类似的，变迁t e t 的后 集t o = 仞pi ( t ，力0 ) 为r 的输出库所集。同样，库所p p 的前集o p 和后集p d 分别 由梦 t e t l ( t 0 ) 和p 喧 f t i 0 ， 给出。 p e t r i 网的动态行为通过改变标识来表示，它必须遵循下面的激活规则。 定义3 3 ：使能变迁的激活 若v p 口t ，m p ) o ，则变迁，处于使能状态。使能变迁的激活( 将标识m 变成m ) ， 从，的每个输入库所中移除一个托肯( v p d f ，m 例= m 例一j ) ，并为t 的每个输出库所 增加一个托肯( v p 尸，m 例= m 纠+ ) 江南大学硕士学位论文 下面介绍的经典p e t r i 网的定义同样也适用于我们的设计描述模型p r e s + 。 定义3 - 4 立即可达标识 如果存在变迁 t 的激活使标识m 变成m ，则标识m 是m 的立即可达标识。 定义3 5 ：所有可达标识 网一组可达集尺仰是m o 的所有可达标识，定义如下： i ) m o e r ( n ) i i ) 若m r 肿，m 是m 的立即可达标识，则m e r ( n ) 定义3 - 6 ：冲突变迁 若o t n o t ，1 2 i ，则变迁，和，相冲突 定义3 - 7 ：无冲突网 若v t , t t ，有f 一n 锄，则网为无冲突网。 定义3 - 8 ：自由选择网 若对任意两个冲突变迁t 和r ，有= l i = 1 ，则网为自由选择网。 定义3 - 9 ：扩展自由选择网 若对任意两个冲突变迁t 和t ，有o r = o r ，则网为扩展自由选择网。 定义3 - 1 0 ：安全网 对任何可达标识，若每个库所中的托肯数目l ，则网是安全的。 定义3 - 1 1 ：活性网 定义3 1 1 如果对每个可达标识m e r ( t v ) 署i 每个变迁f r ，存在一个m 的可达标识 m ，使f 处于使能状态，则网为活的。 3 2 基本p r e s 碳型