BACnet应用层状态机在线测试研究

计算机科学２００６Ｖｏ１．３３№．６　ＢＡＣｎｅｔ应用层状态机在线测试研究　许毅平朱振华周曼丽　（华中科技大学电子与信息工程系　武汉４３００７４）　摘要随着ＢＡＣｎｅｔ网络技术的应用发展，对ＢＡＣｎｅｔ网络设备协议一致性测试的要求也越来越强烈，本文在比较　现有的协议一致性测试方法的基础上，给出了基于在线测试的ＢＡＣｎｅｔ协议测试方法，研究了ＢＡＣｎｅｔ应用层状态机　的运行模式，并采用有限状态机模型对ＢＡＣｎｅｔ应用层状态机进行了分析，给出了相应的状态机状态判定方法和在线　测试的软件结构。　关键词有限状态机，协议一致性测试，状态判定，ＢＡＣｎｅｔ　Ｔｈｅ　Ｓｔｕｄｙ　ｏｆ　Ｏｎ－ｌｉｎｅ　Ｔｅｓｔｉｎｇ　ｆｏｒ　ＢＡＣｎｅｔ　Ａｐｐｌｉｃａｔｉｏｎ　Ｌａｙｅｒ　ＴＳＭ　ＸＵ　Ｙｉ—Ｐｉｎｇ　ＺＨＯＵ　Ｍａｎ－Ｌｉ　（Ｅｌｅｃｔｒｏｎｉｃｓ＆Ｉｎｆｏｒｍａｔｉｏｎ　Ｅｎｇｉｎｅｅｒｉｎｇ　Ｄｅｐａｒｔｍｅｎｔ，Ｈｕａｚｈｏｎｇ　Ｕｎｉｖｅｒｓｉｔｙ　ｏｆ　Ｓｅｉ．＆．Ｔｅｃｈ．，Ｗｕｈａｎ　４３００７４）　Ａｂｓｔｒａｃｔ　Ｗｉｔｈ　ｔｈｅ　ｄｅｖｅｌｏｐｍｅｎｔ　ｏｆ　ＢＡＣｎｅｔ　ｔｅｃｈｎｏｌｏｇｙ，ｔｈｅ　ｒｅｑｕｉｒｅｍｅｎｔｓ　ｏｆ　ｐｒｏｔｏｃｏｌ　ｉｍｐｌｅｍｅｎｔ　ｃｏｎｆｏｆｉｎａｎｃｅ　ｔｅｓｔｉｎｇ　ｂｅｃｏｍｅ　ｍｏｒｅ　ａｎｄ　ｍｏｒｅ　ｉｎｔｅｎｓｅ．Ａｆｔｅｒ　ｃｏｍｐａｒｉｎｇ　ｔｈｅ　ｍｅｔｈｏｄｓ　ｏｆ　ｐｒｏｔｏｃｏｌ　ｉｍｐｌｅｍｅｎｔ　ｃｏｎｆｏｒｍａｎｅｅ　ｔｅｓｔｉｎｇ　ｉｎ　ｅｘｉｓｔｅｎｃｅ，　ｔｈｅ　ｐａｐｅｒ　ｐｒｅｓｅｎｔｓ　ａ　ＢＡＣｎｅｔ　ｐｒｏｔｏｃｏｌ　ｔｅｓｔ　ｍｅｔｈｏｄ　ｂａｓｅｄ　ｏｎ－ｌｉｎｅ．Ａｎｄ　ｔｈｅｎ，ｔｈｅ　ｐａｐｅｒ　ｓｔｕｄｉｅｓ　ｔｈｅ　ｒｕｎｎｉｎｇ　ｍｏｄｅ１　ｏｆ　ＢＡＣｎｅｔ　ａｐｐｌｉｃａｔｉｏｎ　ｌａｙｅｒ　ＴＳＭ，ａｎｄ　ａｎａｌｙｓｅｓ　ｔｈｅ　ＴＳＭ　ｕｓｉｎｇ　ｆｉｎｉｔｅ　ｓｔａｔｅ　ｍａｃｈｉｎｅ　ｍｏｄｅ１．Ｆｉｎａｌｌｙ，ｔｈｉｓ　ｐａｐｅｒ　ｐｒｅｓｅｎｔｓ　ａｎ　ａｌｇｏｒｉｔｈｍ　ｔｏ　ｉｄｅｎｔｉｆｙ　ｔｈｅ　ｓｔａｔｅ　ｏｆ　ＴＳＭ，ａｎｄ　ｄｅｓｃｒｉｂｅｓ　ｔｈｅ　ｓｏｆｔｗａｒｅ　ｆｒａｍｅｗｏｒｋ　ｏｆ　Ｏｎ－ｌｉｎｅ　ｔｅｓｔｉｎｇ．　Ｋｅｙｗｏｒｄｓ　ＦＳＭ，Ｐｒｏｔｏｃｏｌｉｍｐｌｅｍｅｎｔ　ｃｏｎｆｏｒｍａｎｃｅ　ｔｅｓｔｉｎｇ，Ｓｔａｔｅ　ｄｅｔｅｒｍｉｎａｔｉｏｎ。ＢＡＣｎｅｔ　１　引言　在当今网络的时代，网络协议对网络技术和网络产品的　普及和发展发挥了决定性的作用。由于网络协议通常采用非　形式化的、基于自然语言的文本方式描述，这种方式可能使协　议实现的不同开发者对协议标准的理解产生差异，从而使协　议实现偏离协议标准，这种偏离会影响协议实现间的互操作　由美国供热、制冷与空调工程师学会（ＡＳＨＡＲＥ）组织制定的　用于楼宇设备自动化和控制的网络通信协议。该协议是美国　国家标准，欧洲标准草案，并且于２００３年１月２Ｏ日被ＩＳＯ正　式采纳为国际标准（ＩＳ（）１６４８４—５）。随着ＢＡＣｎｅｔ被接纳为　ＩＳ（）国际标准，市场对ＢＡＣｎｅｔ设备的需求也将空前增长。　ＢＡＣｎｅｔ作为一种网络协议，它的协议实现同样面临着协议实　现一致性的问题。　性　因此，协议实现正确性的检测成为关注的焦点，协议一致　性测试就是用来检验协议实现的正确性的有效手段，协议一　致性测试方法一般分为两种；主动测试和被动测试＿】］。　文本通过分析ＢＡＣｎｅｔ应用层协议，提出了一个ＢＡＣｎｅｔ　应用层协议一致性测试方案，实现对ＢＡＣｎｅｔ协议实现的在　线测试。　主动测试一般用于在协议实现出产或认证前进行，采用　主动测试时，测试器（Ｔｅｓｔｅｒ）根据预先设置好的测试集主动　地向被测协议实现（ＩＵＴ）发送测试报文，测试器通过观察　２　ＢＡＣｎｅｔ应用层协议　ＢＡＣｎｅｔ是一种开放性协议，它采用ＯＳＩ模型的分层通　ＩＵＴ对测试报文的响应给出判据。被动测试也叫在线测试，　一信体系结构，同时鉴于楼宇控制系统的实际需要和实现成本　等多方面因素，ＢＡＣｎｅｔ并没有完全参照ＯＳＩ采用七层　般用于协议实现的在线运行测试，采用在线测试时，测试器　并不主动向ＩＵＴ发送测试报文，它主要通过观察和分析ＩＵＴ　实际运行过程中接收和发送的报文序列，推断ＩＵＴ内部状态　的变化是否符合协议的规定，以此来对ＩＵＴ进行检测。主动　测试的关键在于测试集，测试集决定了测试的覆盖范围，也决　结构，而是采用了一个由物理层、数据链路层、网络层和应用　层组成的折叠式结构。在这四层结构中，ＢＡＣｎｅｔ应用层是　ＢＡＣｎｅｔ协议中地位最重要、内容最丰富的一层。ＢＡＣｎｅｔ应　用层定义了两大类服务：无证实应用层服务和有证实应用层　服务　。　定了测试的时问费用，而产生一个高效、全面的测试集往往是　很困难的，而在线测试并不需要测试集，并且在线测试具有测　试环境简单，可长时间进行测试，以及在实际的工作环境下进　行测试等优势，在线测试可以作为主动测试手段的有力补充，　因此研究在线测试具有很现实的意义。　ＢＡＣｎｅｔ协议是Ａ　Ｄａｔａ　Ｃｏｍｍｕｎｉｃａｔｉｏｎ　Ｐｒｏｔｏｃｏｌ　ｆｏｒ　Ｂｕｉｌｄｉｎｇ　Ａｕｔｏｍａｔｉｏｎ　ａｎｄ　Ｃｏｎｔｒｏｌ　Ｎｅｔｗｏｒｋｓ的缩写＿２］。它是　无证实应用层服务是一种不受保证的报文通信机制，主　要用于信息广播和信息探询，发送报文的一方不要求确知发　送的报文是否被期望的接收方收到，也不期待一定收到接收　方的响应，因此在发送方和接收方之间不需要维持状态同步　关系。　＊）美国＆　ｎｅｔ制造商协会（ＢＭＡ）及ＢＡＣｎｅｔ测试实验室（ＢＴＬ）资助。许毅平・　博士。　７６　－　维普资讯 http://www.cqvip.com

服务器状态圈　客户机状志圈　事件ｔｌ：发送无证实请求　　２：发送无证实响应　３　发送不分段有证实请求　４：发送分段有证实请求（第一分段）　５：收到分段有证实请求（第～分段）　６；啦到不分段育｛芷实请求　ｔ嶂到简蔓确认　８　收到分段确认ｕ：收到分段堡杂确认（第一分段）（非最后分段）　９。收到最后分段确认　ｌＯ；收到不分段复杂确认　１４ｔ峨到中止报ｌ文　ｌ５：发送简单确认　　ｌ２：收到分段鬈杂确认（中问分段）ｌ６ｔ发送不分段复杂确认　　１３．ｌ８ｔ发送分段复杂确认（中间分段）　１９ｔ发送分段复杂确认（最后分段）ｌ７ｔ麓送分段复杂确认（第ｒ＿分段）－峥到分段复杂确认（最后分段）　　２０，收到分段有证实请求（中问分段）　　图１　ＢＡＣｎｅｔ应用层状态机　有证实应用层服务是一种受保证的通信机制，采用客户／　的关系，通过分析状态变迁规则，采用推理技术来判断ＩＵＴ　服务器通信模式，发起请求报文的一端为客户端（称为ＢＡＣ—　的状态机变迁是否正确。　ｎｅｔ　Ｃｌｉｅｎｔ），对请求报文进行响应的一端为服务端（称为　ＢＡＣｎｅｔ　Ｓｅｒｖｅｒ），在这种模式下，客户端和服务端采用一问一　表１客户状态机事件及状态变迁规则表　答的会话方式，客户端每发送一个有证实请求报文都要判断　起始事件类型　起始事　起始　变迁　变迁　该报文是否被服务器端收到，以及服务器端对该请求的处理　件编号　状态　状态　事件　结果，在整个会话过程中，客户端和服务端之间需要进行同　发无证实请求　１　０　０　｜　步，以使会话能够正常进行，为了使状态保持同步，ＢＡＣｎｅｔ协　收无证实响应　２　０　０　｜　议规定客户端在发送请求报文时应创建客户状态机（Ｃｌｉｅｎｔ　发不分段有证实请求　３　Ｏ　２　｜　发分段有证实请求（第一分段）　４　０　ｌ　ｆ　ＴＳＭ），服务端在收到有证实请求报文时应创建服务器状态　发分段有证实请求（其他分段）　５　１　１　｜　机（Ｓｅｒ＃ｅｒ　ＴｓＭ），客户状态机和服务状态机分别依据一定的　收简单确认　６　１　０　｜　规则改变各自的会话状态，共同管理双方的会话，使通信的双　２　０　｜　方能够顺利地完成对话。ＢＡＣｎｅｔ规定一个协议实现可以同　收分段确认　７　１　１　５　时建立多个会话，在每个会话中协议实现充当不同的角色，即　收最后分段确认　８　１　２　ｆ　协议实现在一个会话中可以充当客户端，在另一个会话中充　收不分段复杂确认　９　１　０　｜　当服务端，协议实现为每一个会话创建一个状态机。因此，在　２　０　ｉ　某一时刻，一个协议实现可能同时存在若干个客户状态机和　收分段复杂确认（第一分段）　１０　１　２　３　３　１３　１３　服务器状态机。ＢＡＣｎｅｔ应用层状态机如图ｌ所示，由图可　收分段复杂确认　１１　３　３　１３　知，一个客户状态机有空闲、等待证实、分段请求和分段证实　（其他分段）　４种状态，一个服务器状态机有空闲、分段请求、分段响应和　收分段复杂确认　１２　３　０　１４　等待响应４种状态。　（最后分段）　发分段确认　１３　３　３　｜　３　ＢＡＣｎｅｔ应用层状态机变迁规则　采用在线测试主要通过分析ＩＵＴ接收和发送的报文序　ＢＡＣｎｅｔ协议应用层状态机可以用有限状态机模型来进　列，推断ＩＵＴ状态机是否按协议的规定进行运行。任何一个　行描述，有限状态机模型是一种由若干状态、一个起始状态、　事件都有它发生的条件，这个条件就是状态机的当前状态。　一个终止状态、一组输入输出符号和状态变换函数组成的计　因此，当一个ＩＵＴ产生一个事件（发送一个报文），该ＩＵＴ内　算模型，有限状态机可以用来抽象表示一个进程的运行　部的状态机的状态肯定属于某个状态子集，该子集所包含的　状态Ｉ４　］。标准有限状态机可以表示为ＴＳＭ＝（Ｓ，Ｘ，ｙ，　，　状态个数大于等于１；当一个ＩＵＴ接收到一个事件（接收到一　，Ｑ，Ｆ），其中，Ｓ表示所有状态的集合；Ｘ表示所有输入符　个报文），该ＩＵＴ内部的状态机的状态同样肯定属于某个状　号的集合；ｙ表示所有输出符号的集合；　为状态迁移函数；Ａ　态子集。　为输出函数；Ｑ为起始状态集；Ｆ为终止状态集。　由于一个事件可能在多个状态下均可能发生，因此在线　ＢＡＣｎｅｔ应用层有客户状态机和服务器状态机两种，这两　测试器不能明确地确定ＩＵＴ状态机的状态，然而，一个与某　个状态机的运行是的，采用有限状态机模型可分别定义　一状态机相关的连续的事件序列可以确定一个唯一的状态机　为：　状态序列，因此，当在线测试器检测足够长的事件序列时，就　客户状态机模型：Ｃｌｉｅｎｔ—ＴＳＭ＝（Ｓ，Ｘ，Ｙ，　，．：【，Ｑ，Ｆ），　可以确定ＩＵＴ状态机的状态，从而可以判断该ＩＵＴ的状态　其中Ｓ　｛空闲，分段请求，等待证实，分段证实｝，Ｑ　｛空　机是否正确。　闲｝，Ｆ＝｛空闲｝，Ｘ一｛系统外部输入（所有可能接收到的报　为了能够实现该目的，需要分析事件和状态机可能状态　文类型），系统内部输入｝，Ｙ＝｛系统外部输出（所有可能发　・　７７　・　维普资讯 http://www.cqvip.com

送的报文类型），系统内部输出），状态迁移函数　为变迁状态　与输入ｘ和当前状态的映射关系，状态的变迁由输入ｘ和当　前状态共同决定，输出函数　为输出与输入和当前状态的映　射关系，输出由输入ｘ和当前状态共同决定。　服务器状态机模型：Ｓｅｒｖｅｒ－ＴＳＭ－－（Ｓ，Ｘ，Ｙ，　，　，Ｑ，　应的，增加一个事件层同时也会增加一个状态关联层。　Ｆ），其中Ｓ一｛空闲，分段请求，等待响应，分段响应｝；Ｑ一　｛空闲｝，Ｆ－－｛空闲｝，Ｘ一｛所有可能接收到的报文类型｝，系　统内部输入｝，Ｙ一｛系统外部输出（所有可能发送的报文类　型），系统内部输出｝，状态迁移函数　为变迁状态与输入ｘ　和当前状态的映射关系，状态的变迁由输入Ｘ和当前状态共　同决定，输出函数　为输出与输入和当前状态的映射关系，输　出由输入Ｘ和当前状态共同决定。　由于客户机状态机和服务器状态机的测试方法是相同　的，这里以客户状态机的例来分析事件和状态机状态间的关　联，一个事件可由５个部分来描述：时间、发送者、接收者报文　以及状态机标识，标记为Ｅ一｛Ｔｉｍｅ，Ｓｅｎｄｅｒ，Ｒｅｃｅｉｖｅｒ，ＰＤＵ，　ＴＳＭＩＤ）。一个事件通常与起始状态、变迁状态以及变迁事　件相关联，我们称这种关联为状态变迁规则　起始状态表示　发生某事件的可能的条件状态，也就是一个事件一定是当状　态机处于一定状态时才可能发生；变迁状态表示在起始状态　下发生该事件后，状态机发生变迁后的状态，事件发生后，状　态机的状态可能不变也可能变为其他状态；变迁事件表示发　生变迁时状态机产生的事件（即向外发送报文），事件发生后。　状态机可能产生变迁事件，也可能不产生　由于在线测试时，　在线测试器所能观察到的事件是网络上的报文，引起状态机　改变的其他内部事件（如超时、上层应用软件的操作等）是没　法获取的，因此，需要将客户状态机的事件和状态进行重新整　理和编号。客户状态机有四种状态｛空闲，分段请求，等待证　实，分段证实｝，分别记为｛０，１，２，３｝。客户状态机事件可以归　纳为１５种事件，同种事件具有相同的状态变迁规则，不同类　型的事件可能具有不同的状态变迁规则。表１给出了各种事　件的状态变迁规则。当发生某事件时，只要查找该事件对应　的变迁规则，就可以得到事件的起始状态，变迁状态和变迁事　件，同一个事件可能有多条变迁规则。　４　ＢＡＣｎｅｔ应用层状态机状态判定　在线测试的根本方法就是通过根据前面描述的状态机模　型和状态变迁规则来推断ＩＵＴ同步的状态变迁，由于每个　ＩｕＴ可能同时存在有多个状态机，我们采用孩子兄弟树来管　理ＴＳＭ的状态变迁推理（如图２所示）。图中有四种节点，　Ｒｏｏｔ为根节点，用于索引状态机节点。ＴＳＭ为状态机节点，　每个服务器状态机和客户状态机对应一个唯一的ＴＳＭ节　点，每个ＴＳＭ节点都有一颗状态变迁推理子树，推理子树由　事件层和状态关联层交替组成，事件层包含事件节点（即Ｅ　节点），每个状态变迁推理子树的事件层只包含一个事件节　点，事件节点包含一个事件信息。状态关联层由状态变迁节　点Ｓ组成，ｓ节点描述上一层事件层事件的状态变迁规则，包　括事件的起始状态、变迁状态和变迁事件，由于一个事件可能　有多个状态变迁规则，因此，状态关联层可能包含多个状态变　迁节点Ｓ，状态变迁节点作为上层Ｅ节点的子节点，同层的ｓ　节点互为兄弟。状态关联层下层的事件层包含一个事件节　点，该事件节点Ｅ作为上层的某个状态变迁节点的子节点，　条件是该事件的起始状态为上层Ｓ节点的变迁状态，同时生　成该事件的状态关联层节点。事件层和状态关联层是一一对　・　７８・　图２　ＴＳＭ状态判定管理图　当每次事件到达时，查找ＴＳＭ状态管理树。找到相应　ＴＳＭ（￣Ｉ是第一次，创建新节点），进行ＴＳＭ推理运算，如果　推理成功，则等待下一事件；如果错误返回，则将ＴＳＭ节点　从Ｒｏｏｔ中取下，放入到错误ＴＳＭ链表中，进行相应处理。关　键的状态变迁判定算法描述如下：　算法：ＴＳＭ推理运算　Ｉｎｐｕｔ：事件Ｅｖｅｎｔ　Ｏｕｔｐｕｔ：返回成功；返回错误　Ｆｕｎｃｔｉｏｎ：　ＭａｔｃｈＣｏｕｎｔ　Ｏ（初始化，表明此次查找匹配规则数目）　在Ｒｏｏｔ中查找对应ＴＳＭ节点　Ｉｆ没找到　Ｔｈｅｎ创建新的ＴＳＭ节点添加到Ｒｏｏｔ，深度Ｄｅｐｔｈ一０。Ｍａｔｃｈ　Ｃｏｕｎｔ＝０　Ｅｌｓｅ找到相应的ＴＳＭ，在当前ＴＳＭ节点下查找深度为ｄｅｐｔｈ的　状态关联层节点（广度遍历）　Ｆｏｒ该层每一个状态变迁节点　Ｆｏｒ事件的每个变迁规则　Ｉｆ规则匹配　Ｔｈｅｎ　｛　将事件节点添加当前状态变迁节点的子节点。同　时增加该事件节点的子节点（关联层子节点）。ＭａｔｃｈＣｋｍｎｔ＋＋，Ｄｅｐｔｈ＋＋。　　｝　Ｉｆ　ＭａｔｃｈＣｏｕｎｔ为０　Ｔｈｅｎ返回错误（所有规则不匹配）　Ｅｌｓｅ返回成功　５　ＢＡＣｎｅｔ协议在线测试系统软件结构　图３为系统的软件结构图，各模块的主要功能如下。　包捕捉模块：包捕捉模块根据包过滤器的设置对网络上　传输的报文进行监听，涛符合包过滤器规则的报文上传给包　处理模块，同时也将包传递给数据存储模块　包处理模块：包处理模块的主要目的是提取事件信息，事　件信息包括时间、发送考、接受者、报文类型以及状态机标识，　这些信息需要根据报文内的信息加工获得。因此，包处理模　块需要对报文进行解码，为了正确解码，包处理模块需要调用　编解码模块的解码处理函数。如果解码正确，则包处理模块　将事件信息传递给事件匹配模块，如果解码失败，则将错误信　息传递给异常处理模块处理。　编解码模块：该模块是ＢＡＣｎｅｔ编解码函数接口模块，提　供了ＢＡＣｎｅｔ协议定义的报文、数据的编解码宴现。　事件匹配模块：该模块根据包处理模块提供的事件信息　查询状态变迁规则库，查找出与该事件相关的状态变迁规则，　并将事件及其状态变迁规则传给状态树管理模块。　（下转第８２页）　维普资讯 http://www.cqvip.com

对型的访问权限；访问描述在整个访问控制框架中用到　的关系，例如对访问时间的。　＃Ｄｏｍａｉｎ　Ｄｅｆｉｎｉｔｉｏｎｓ　＃Ａｃｃｅｓｓ　Ｃｏｎｔｒｏｌ　Ｍａｔｅｒｉｘ　对主体提出的动态客体预留请求进行裁决并对系统预留资源　进行管理。通过预留资源的实施，系统避免了关键应用与其　它程序之问产生的资源使用冲突。在访问控制框架中。我们　／ｂｉｎ／ｐｈｏｎｅ＝ｔｒｕｓｔｅｄ＿ｄ　（ｔｒｕｓｔｅｄ　ｄ，ｓｙｓｔｅｍ　Ｉ，ａｌ１）　／ｕｓｒ／ｂｉｎ／ｍｐｌａｙｅｒ＝ｅｅｒｔｉｆｉｅｄ＿ｄ（ｃｅｒｔｉｆｉｅｄ＿ｄ，ｓｅｎｓｉｔｉｖｅ—ｔ，ｒｗ）　使用一种扩充ＤＴＥ策略的描述性语言来定义访问控制策略。　＃Ｔｙｐｅ　Ｄｅｆｉｎｉｔｉｏｎｓ　＃Ｃｏｎｓｔｒａｉｎｔｓ　／ｅｃｔ／ｎｅｔｗｏｒｋ＝ｓｙｓｔｅｍ＿ｔ　（ｃｅｒｔｉｆｉｅｄ＿ｄ，ｓｅｎｓｉｔｉｖｉｅ＿ｔ，　方便用户的配置和管理．　／ｕｓｒ／ｌｏｃａｌ／ａｂｅ．ｍｐｅ—ｓｅｎｓｉｔｉｖｅ＿ｔ　Ｔｉｍｅｉｎｔｅｒｖａｌ　１　９：００　１　２２：００）　＃Ｒｅｓｅｒｖａｔｉｏｎ　Ｄｅｆｉｎｉｔｉｏｎｓ　参考文献　ＣＰＵ＿Ｐ１＝２０ｍｓ，　Ｍｅｍｏｒｙ１　Ｔｒｕｓｔｅｄ　Ｃｏｍｐｕｔｉｎｇ　Ｇｒｏｕｐ．ＴＣＧ　Ｓｐｅｃｉｆｉｃａｔｉｏｎ　Ａｒｃｈｉｔｅｃｔｕｒｅ　Ｏｖｅｒ—　—Ｐ１＝３Ｏ　Ｐｏｗｅｒ　Ｐｌ＝ｓｔｒｉｃｔ　Ｓｅｔ１＝｛ＣＰＵ＿Ｐ１．Ｍｅｍｏｒｙ—ＰＩ，｝　ｖｉｅｗ．Ｖ１．２，Ａｐｒ．２００４．ｈｔｔｐｓ：／／ｗｗ　ｔｒｕｓｔｅｄｃｏｍｐｕｔｉｎｇｇｒｏｕｐ．　Ｓｅｔ２一｛Ｐｏｗｅｒ＿Ｐ１）　ｏｒｇ／　／ｂｉｎ／ｐｈｏｎｅ　９０　２　Ｔｒｕｓｔｅｄ　Ｍｏｂｉｌｅ　Ｐｌａｔｆｏｒｍ．Ｓｏｆｔｗａｒｅ　Ａｒｃｈｉｔｅｃｔｕｒｅ　Ｄｅｓｃｒｉｐｔｉｏｎ。　图３策略语言示例　２００４．ｈｔｔｐ：／／ｗｗｗ．ｔｒｕｓｔｅｄ—ｍｏｂｉｌｅ．ｏｒｇ／　３　Ｃｏｎｓｕｍｅｒ　Ｅｌｅｃｔｒｏｎｉｃｓ　Ｌｉｎｕｘ　Ｆｏｒｕｍ．ＣＥＬＦ　Ｓｐｅｃｉｆｉｃａｔｉｏｎ　ｖ１．０，Ｊｕｎ　进一步的工作和结论在预留执行中，系统对主体使用　２００４．ｈｔｔｐ：／／ｗｗｗ．ｃｅｌｉｎｕｘｆｏｒｕｎ￣ｏｒｇ／　超过预留资源的情况进行了处理。另一方面，用户对主体运　４　Ｂａｄｇｅｒ　Ｌ，Ｓｔｅｒｎｅ　Ｄ　Ｆ，Ｓｈｅｒｍａｎ　Ｄ　Ｌ，ｅｔ　ａ１．Ｐｒａｅｔｉｃａ１　Ｄｏｍａｉｎ　ａｎｄ　行所需要的资源无法准确判断，定义的预留资源可能大于实　Ｔｙｐｅ　Ｅｎｆｏｒｃｅｍｅｎｔ　ｆｏｒ　ＵＮＩＸ．Ｉｎ：ＩＥＥＥ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ　Ｓｅｃｕｒｉｔｙ　际用到的资源，造成系统资源浪费。降低系统性能。对于这种　ａｎｄ　Ｐｒｉｖａｃｙ。Ｏａｋｌａｎｄ，Ｃａｌｉｆｏｒｎｉａ，Ｍａｙ　１９９５．６６～７７　情况，需要进一步改进资源预留模型，以便用户可以根据资源　５　Ｒａｊｋｕｍａｒ　Ｒ，Ｊｕｖｖａ　Ｋ，Ｍｏｌａｎｏ　Ａ，ｅｔ　ａ１．Ｒｅｓｏｕｒｃｅ　Ｋｅｒｎｅｌｓ：Ａ　Ｒｅ—　的实际使用情况进行调整。另外，在系统运行过程中，一些非　ｓｏｕｒｃｅ－Ｃｅｎｔｒｉｃ　Ａｐｐｒｏａｃｈ　ｔＯ　Ｒｅａｌ　Ｔｉｍｅ　ａｎｄ　Ｍｕｌｔｉｍｅｄｉａ　Ｓｙｓｔｅｍｓ．　周期性进程需要动态修改其预留资源，需要在模型定义以及　Ｉｎ：Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ：ＳＨＥ／ＡＣＭ　Ｃｏｎｆｅｒｅｎｃｅ　ｏｎ　Ｍｕｌｔｉｍｅｄｉａ　Ｃｏｍｐｕｔｉｎｇ　ａｎｄ　Ｎｅｔ’￣ｍｒｋｉｎｇ，Ｊａｎｕａｒｙ　ｌ９９８　框架方面做进一步的改进。　６　Ｍｅｒｃｅｒ　Ｃ　Ｗ．Ｏｐｅｒａｔｉｎｇ　Ｓｙ　ｓｔｅｍ　Ｒｅｓｏｕｒｃｅ　Ｒｅｓｅｒｖａｔｉｏｎ　ｆｏｒ　Ｒｅａｌ—　本文设计了一种应用于移动终端系统的访问控制框架，　Ｔｉｍｅ　ａｎｄ　Ｍｕｌｔｉｍｅｄｉａ　Ａｐｐｌｉｃａｔｉｏｎｓ．Ｃａｒｎｅｇｉｅ　Ｍｅｌｌｏｎ　Ｕｎｉｖｅｒｓｉｔｙ，　不但能够保证数据的机密性和完整性要求，而且满足系统对　１９９７　关键应用及时响应的要求，提高移动终端的可用性　在该访　７　Ｓｃｏｒｄｉｎｏ　Ｃ．Ｌｉｐａｒｉ　Ｃ　．Ｕｓｉｎｇ　Ｒｅｓｏｕｒｃｅ　Ｒｅｓｅｒｖａｔｉｏｎ　Ｔｅｃｈｎｉｑｕｅｓ　ｆｏｒ　问控制框架中，移动终端客体被分为两类：静态客体和动态客　Ｐｏｗｅｒ￣Ａｗａｒｅ　Ｓｃｈｅｄｕｌｉｎｇ，Ｉｎ：Ｐｒｏｅ．ｏｆ　ｔｈｅ　４ｔｈ　ＡＣＭ　Ｉｎｔ１．Ｃｏｎｆ．ｏｎ　体。主体提出的访问请求通过访问代理转交给访问监控器和　Ｅｍｂｅｄｄｅｄ　Ｓｏｆｔｗａｒｅ，Ｐｉｓａ，Ｉｔａｌｙ，Ｓｅｐｔ，２００４　预留监控器，前者负责对静态客体的访问进行控制，后者负责　（上接第７８页）　总结通信协议一致性测试是一个十分活跃的研究领　状态变迁规则库：用于存放事件和事件状态变迁规则。　域，在线测试作为一种怫议一致性测试方法具有其独特的优　每个状态变迁规则包括事件类型、起始状态、变迁状态和变迁　势，由于这种测试本身不对被测系统的正常运行带来干扰，因　事件，一种事件可能具有多条状态变迁规则　此可以实现对被测系统长时间的测试。本文对在线测试在　状态树管理模块：该模块主要根据事件匹配模块匹配的　ＢＡＣｎｅｔ通信协议的应用进行了讨论，给出了基于有限状态机　结果对状态树进行管理。该模块对每二个事务状态机维持一　模型的ＢＡｃｎｅｔ协议：伏态机测试方法和软件框架。　个ＴＳＭ节点，每个ＴＳＭ节点下有一个对应的状态变迁树。　每次事件到达时。以事件的状态机标识信息为索引找到相应　参考文献　的状态变迁树。然后。根据变迁规则，通过推理，使状态树向　１　吴建平，尹霞．基于形式化方法的协议测试理论ＥＪ］．清华大学学　每一个可能的方向进行生长。当状态变迁树不能生长时，通　报（自然科学版），２００１．４１（４／５）　知异常处理模块进行异常判断，并对已无生长可能的分支进　２　ＡＳＨＲＡＥ　ＢＡＣｎｅｔ：Ａ　Ｄａｔａ　Ｃｏｍｍｕｎｉｃａｔｉｏｎ　Ｐｒｏｔｏｃｏｌ　ｆｏｒ　Ｂｕｉｌｄ－　行剪枝处理。　ｉｎｇ　Ａｕｔｏｍａｔｉｏｎ　ａｎｄ　Ｃｏｎｔｒｏｌ　Ｎｅｔｗｏｒｋｓ　１３５—２００１　异常处理模块：对包处理模块、状态树管理模块中产生的　３　Ｓｐｉｔｓｙｎａ　Ｎ，Ｔｒｅｎｋａｅｖ　Ｖ．ＦＳＭ　Ｂａｓｅｄ　Ｉｎｔｅｒｏｐｅｒａｂｉｌｉｔｙ　Ｔｅｓｔｉｎｇ　ｏｆ　ｏＣｍｍｕｎｉｃａｔｉｏｎ　Ｐｒｕｔｏｃｏｌｓ．Ｃｏｎｔｒｏｌ　ａｎｄ　Ｃｏｍｍｕｎｉｃａｔｉｏｎｓ，ｔｈｅ　异常信息进行格式化处理。并且能对出错原因进行一定的推　２００３　ＩＥＥＥ—Ｓｉｂｅｒｉａｎ　Ｃｏｎｆｅｒｅｎｃｅ　ｏｎ，２００３．２０～２３　理分析，然后将分析结果发送给数据存储模块。　４　Ｚｈａｏ　Ｙｉｘｉｎ。Ｙｉｎ　Ｘｉａ，Ｈａｎ　１３ｏ，ｅｔ　ａ１．Ｏｎｌｉｎｅ　Ｔｅｓｔ　Ｓｙｓｔｅｍ　Ａｐ—　数据存储模块；对收到的报文信息、正在维护的ＴＳＭ树　ｐｌｉｅｄ　ｉｎ　Ｒｏｕｔｉｎｇ　Ｐｒｏｔｏｃｏ１　Ｔｅｓｔ　Ｍｏｄｅｌｉｎｇ．Ａｎａｌｙｓｉｓ　ａｎｄ　Ｓｉｍｕｌａｔｉｏｎ　信息以及异常信息进行存储管理，以便用户查看。　ｏｆ　Ｃｏｍｐｕｔｅｒ　ａｎｄ　Ｔｅｌｅｃｏｍｍｕｎｉｃａｔｉｏｎ　Ｓｙｓｔｅｍｓ．Ｉｎ：Ｐｒｏｅｅｅｄｉｎｇｓ　ｏｆ　状志变迁规则库　．－　事件匹配模块　—＇　状寿树管珊模块　Ｎｉｎｔｈ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ，Ａｕｇ．２００１．３３１～３３８　５　赵邑新，吴建平．应　用于在线测试的状态判定算法．电子学报，　２０００，２８（１１）：８３～８７　编．翠码模块　＿－　包处理模块　—１　异常处理模块　包捕捉模块　——－－一　数据存储模块　图３软件结构图　・８２・