【摘 要】
:
针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换
【机 构】
:
西安电子科技大学计算理论与技术研究所,西安电子科技大学ISN国家重点实验室,武汉大学软件工程国家重点实验室
论文部分内容阅读
针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效
其他文献
运用复杂系统通用设计方法IDEF0对整个系统进行规划和设计,将CAD,CAPP与MRPⅡ集成WTUMRP系统,使系统具有良好结构性和模块性,介绍了系统工作原理琢其用户界面特色。
根据相似理论放大的模型,采用热色液晶瞬态测量技术研究带有60°肋和单排溢流孔的内流通道的换热特性,分析主流雷诺数和出流比对壁面对流换热的影响规律.矩形内流通道进
在能量异构传感器网络中,由于节点能量在一定范围内随机分布,平衡能量消耗和延长网络寿命成为此类算法的一个重要挑战.针对该问题,提出了一种基于蚁群算法的异构传感器网络路由算
为了避免薯蓣皂甙元-3β-乙酸酯溴加成反应中C-23溴代副产物的产生,系统考察了有机碱和环氧化合物对它溴加成反应的影响.由于有机碱和环氧化合物均可消除反应体系中存在的酸,
为加深对狭缝通道内水沸腾换热机理的探索,对宽度为2mm、长度为300mm的竖直狭缝通道内水沸腾气泡动力学展开研究,通过数值模拟的方法探索气泡生成、长大和脱离的过程,分析了壁面
提出一种新的气液两相流体等干度分配方法——分相分配法.该方法的特点在于,基于单相流体较容易实现均匀分配的特征,首先通过强化两相流体在分配单元内的相分离,将气液混合物
市场竞争是否必然带来社会道德的沦丧 ?在市场经济中如何寻求法治与道德的契合点 ?本文在分析了市场经济下的道德现状 ,以及法律对道德的积极作用后 ,从健全权力约束机制、完