论文部分内容阅读
对复杂时间行为协议状态进行约减对于缓解形式化验证的状态空间爆炸问题,提高验证工具系统的效率、实用性等具有重要意义。分析了实时构件组合的几种形态,对基于时间行为协议的组合理论和状态空间爆炸问题进行了讨论,给出了时间行为协议的状态空间约减算法并进行了分析,给出了示例。
时间行为协议状态空间约减算法
【摘 要】
：
对复杂时间行为协议状态进行约减对于缓解形式化验证的状态空间爆炸问题,提高验证工具系统的效率、实用性等具有重要意义。分析了实时构件组合的几种形态,对基于时间行为协议
【机 构】
：
聊城大学计算机学院,北京航空航天大学计算机学院
【出 处】
：
计算机科学
【发表日期】
：
2012年4期
【基金项目】
：
国家自然科学基金项目（90718017）, 山东省自然科学基金项目（ZR2011FL023）, 山东省软科学项目（2010RKE16007）, 聊城大学自然科学重点项目（x09032） 山东省高校智能信息处理与网络安全重点实验室（聊城大学）资助
其他文献
定位技术是无线传感器网络中的关键支撑技术之一。针对移动无线传感器网络的特点,在深入分析现有多维定标节点定位算法的基础上,提出一种改进机制,即距离自调整的多维定标节
提出了一种基于物理的流体运动模拟方法,同传统的模拟技术相比,基于物理的模拟更能表现真实感运动。选用的物理模型是完整的Navier-Stokes方程组,针对完整的Navier-Stokes方程组,利用破开算子法将模型分解成外力、对流、扩散和投影项分别进行计算。因为每一步都稳定,所以整个求解过程也稳定。因此可以用大时间步长来模拟流体运动。Navier-Stokes方程组保证了真实感,而此求解方法保证了
支持向量机是一种用途广泛的分类器,标准的支持向量机在预测每个样本点的类别时使用了训练集中所有的样本信息(即全局信息),然而这种全局化的方法并不蕴含一致性。局部支持向
云端计算可以充分聚合Internet网络服务器端和边缘终端节点的计算资源来获得更大的效益。但将计算任务部署到用户终端上执行却带来了安全隐患。分属于不同用户的海量终端节点
Web服务(Web services)已成为当前和未来网络分布式应用的主流软件开发技术。如何确保Web服务软件的质量和可靠性是当前软件工程领域关注的焦点问题。分析了Web服务测试的层
移动Adhoc网络（MANET，Mobile Adhoc Networks）正得到越来越广泛的应用，相应的网络安全问题也开始得到广泛的关注。研究MANET网络可能遭遇的攻击方式，提出基于机器学习技术的入侵检
赋时Petri网为装配序列规划提供了有效的建模方法,但其在求解最优装配序列时受到组合复杂性的严重制约。零压缩二叉决策图（ZBDD）是处理大规模组合集合和0-1稀疏向量的一种有效
隐私保护数据挖掘是在不精确访问原始数据的基础上，挖掘出准确的规则和知识。针对分布式环境下聚类挖掘算法的隐私保护问题，提出了一种基于完全同态加密的分布式聚类挖掘算法（FH