基于LOTOS的PIM-SM协议形式化分析

来源 :2006北京地区高校研究生学术交流会 | 被引量 : 0次 | 上传用户:lijincai0122
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
PIM-SM协议是目前应用最为广泛的域内组播路由协议,但它的标准化进程仍处在实验阶段,协议本身需要不断发展完善,有必要使用形式化方法对其进行研究.本文基于协议工程学理论和LOTOS形式化技术,提出PIM-SM组播系统的抽象模型,重点给出协议实体的部分形式化描述,最后使用CADP工具集对其进行验证.
其他文献
火电厂大型机组具有控制对象复杂、滞后大,模型难以建立等特点,用传统的控制方法很难得到最佳的运行效果,而多变量广义预测控制策略,具有适用范围广、鲁棒性强等优点,可有效弥补上述不足.本文提出了一种约束优化的算法,此算法不但适合实际工业中物理量不能无限取值的要求,而且利用了矩阵分解技术,使在线运算量大为减少.
本文应用状态反馈预测控制(SFPC)算法,对带有耦合、不确定性的油田联合站油水分离控制过程进行分解分析,给出了基于状态反馈的电脱水系统的多变量适应式SFPC算法.基于Lyapunov稳定性理论,对时滞过程进行分解分析,推出了多变量线性时滞系统的时滞独立稳定充分条件方程式,并在此基础上给出了几个判定线性时滞系统独立稳定的简单判据,讨论了时滞系统的指数稳定性,给出了系统具有任意指定收敛速度指数稳定的充
轧机驱动电机与轧辊间采用长轴连接,连接轴刚度有限,因此在带材高速轧制时,常规电流、转速双闭环控制易产生机电振动和断带现象.为克服该缺陷,本文针对具有参数摄动、负载扰动和电枢反应引起的非线性不确定性的直流驱动轧机主传动系统控制问题,基于H∞控制理论设计了轧机主传动系统的鲁棒状态反馈控制器,并利用两自由度控制方法设计了主传动系统的前馈补偿控制器.仿真研究结果表明,该方法不仅有效抑制了轧机主传动系统的机
针对单自由度磁悬浮模型无法解决转子高速旋转时的各向耦合和陀螺效应的问题,采用了径向四自由度和轴向单自由度的整体建模方法,得到了五自由度磁悬浮轴承模型.因径向与轴向不存在运动耦合,所以只针对径向四自由度进行了分析设计.通过对干扰抑制指标的H∞综合设计,得到H∞最优动态补偿器.仿真结果表明,该方法设计的控制器有较好的鲁棒稳定性和较强的干扰抑制性能.
提出一种基于规则的资源动态协调方法.通过高斯函数动态计算流程使用资源的优先级,并使用规则约束流程间的资源竞争,达到对资源的重新分配和优化的目的.该方法能将流程和资源的相关信息实时反映到流程对资源的调度上,解决了资源分配模式单一和缺乏实时性等问题,使得系统更加合理地分配资源,提高系统的性能.
在基于Vega的视景仿真中,传统的鼠标加键盘的操作方式难以满足复杂操作的需要.本文提出了将SpaceBall运用于Vega仿真视景中的一种操作方法,并对其实现的关键技术进行了探讨.将此方法应用于某型导弹虚拟挂弹系统开发中,取得了良好的效果.
Web服务的商业流程执行语言(简称BPEL或BPEL4WS)是由IBM/BEA/Microsoft等几家厂商联合提出的一种基于XML的工作流定义语言,可以作为企业工作流建模的基础.但是目前能够图形化自动生成符合BPEL4WS规范的流程设计器并不多,基于这种现状,本文在现有的工作流的研究基础上,提出一种符合BPEL4WS规范的工作流平台.本文首先介绍了工作流和BPEL的基本概念,然后给出了该流程设计
提出了一种基于底层网络消息传递机制的分布式对象模型:远端应用服务对象(RASO-Remote Application Server Object).模型以异步回调和有限状态机概念为基础,构建了一种松耦合、可扩展性强的分布式系统.模型能根据用户服务需求灵活定制,并以较小的开销完成消息交换,克服了传统分布式中间件操作复杂、使用效率低的缺点.文章最后对一个RASO数据库实例作了性能分析.
本文根据维修作业任务调度的复杂性,以及当前存在的问题.提出了基于Multi-Agent技术的维修作业任务调度系统,建立了基于管理Agent、任务Agent和资源Agent的系统模型,引入了面向任务领域的协商机制,并且讨论了单调让步协议和Zeuthen策略.
针对xml格式的特点,首先利用结构图把xml文档集转换成属性数据集,把xml文档的聚类转换成属性数据的聚类.然后对现有属性数据聚类算法k-modes从3个方面加以改进,最后给出了聚类的全部流程.实验结果充分说明了这种算法的可行性和有效性.