【摘 要】
：
控制器综合从较高的抽象层次开始，使用硬件描述语言，采用综合优化工具进行，因此验证综合过程的正确性至关重要。本文采用图同构的方法对控制器综合前的完全确定有限状态机STG_org和从综合后结构实现逆向提取的完全确定有限状态机STG_ext进行等价性证明，从而验证综合过程的正确性；为进一步降低算法时间复杂度，利用综合过程状态化简的信息，提出带综合信息指导的验证算法，将时间复杂度从O(B2/A·t1(n)
【机 构】
：
安徽大学计算机科学与技术学院,安徽合肥 230039;安徽大学计算智能与信号处理教育部重点实验室,安徽合肥 230039
【出 处】
：
全国第19届计算机技术与应用学术会议(CACIS·2008)
论文部分内容阅读
控制器综合从较高的抽象层次开始，使用硬件描述语言，采用综合优化工具进行，因此验证综合过程的正确性至关重要。本文采用图同构的方法对控制器综合前的完全确定有限状态机STG_org和从综合后结构实现逆向提取的完全确定有限状态机STG_ext进行等价性证明，从而验证综合过程的正确性；为进一步降低算法时间复杂度，利用综合过程状态化简的信息，提出带综合信息指导的验证算法，将时间复杂度从O(B2/A·t1(n)+A·t2(m,n))降低到D(B·t1(n)+A·t2(m，n))，理论上证明了算法的高效性。
其他文献
提出基于虚拟现实(VR)技术的三维虚拟现实实验室(VPL)的设计架构.对架构各模块分门别类作了介绍,并对数据库的使用与连接、虚拟现实实验(VRE)图形图像的实现等关键技术作了专门阐述.针对Cult3D与Java在VRE图形图像表现、数据管理的特点,进行了分析比较.
本文简要介绍了一种新的三维地学空间构模方法-似三棱柱(STP法).用它作为基本体元来实现三维地质体的可视化,该方法首先将原始钻孔数据经过预处理形成各个地层上下对应的三角网格高程数据,然后连接相邻地层上下对应的网格形成似三棱柱.在此体元上对三维地质体漫游技术中大量使用到的直线、平面与似三棱柱体元,切剖面的求交算法做了一定的研究,最终借鉴OpenGL的功能,实现了三维地质体的几种可视化操作.
模型化处理是航天器测控工程的重要技术之一.本文以单体航天器的在轨姿态运动为研究对象,采用动力学分析的方法,建立了航天器姿态运动的动态-测量系统模型,并简要指出上述模型在航天器姿态估计、姿态预报、故障诊断、动力系统仿真和控制工程等方面的应用.
本文讨论了基于集对分析SPA的联系数的可拓SPE和基于集对联系值的模糊系统SPF,并提出联合应用SP(A+B+C+D+E+F)框图。
本文研究了嵌入式技术在以单片机为控制核心的多功能小车的应用,小车的功能有循线,避障,语音及液晶显示等.在凌阳16位单片机SPCE061A的基础上,自制的红外传感器实现循线,利用微动开关实现避障,单片机较完备的语音处理功能及外接功放电路实现语音功能.小车的驱动采用普通直流电机,利用驱动芯片L298方便地实现小车的变速及转弯.
本文提出了在噪声干扰情况下准确提取BPM时间信号的模型.此模型在对时间信号的特征和噪声干扰的综合影响充分分析的基础上,合理利用多种滤波和误差补偿及修正方法等实现了信号的提取,实验证明误差小于100us.
为在天基网络中进行应用级开发与研究,需要对背景业务流量进行建模并实时生成.本文提出了一种基于分形散粒噪声的卫星网络流级聚合流量生成算法,该算法根据星间链路的差错特性、星上路由器随机丢弃策略、星间路由往返时延抖动特性、拥塞控制策略,对单个流的速率波动进行建模,进而使用分形散粒噪声过程对天基组网中的聚合业务流量进行模拟生成。
在无线网络下行链路的资源调度的过程中，无线信道的时变特点对整个网络的吞吐量和用户之间的公平性有很大的影响。本文为了在保证用户公平性的前提下，提高整个系统的吞吐量，提出了一种基于信道状态监测的改进PF调度算法。该算法通过对每个用户调度时刻之前的信道监测，来衡量每个用户信道的特点，并以此为依据对传统的PF算法做出改进。仿真结果表明在保证用户公平的前提下，改算法能有效的提高整个系统的吞吐量。
为了实现高效率、自适应的Internet动态路由策略，在本体论基础上，提出Internet动态路由的本体建模思想。使用本体开发工具Protégé描述Internet动态路由的概念本体和任务本体。根据该模型建立Internet动态路由实现框架，并在实验仿真环境中进行验证。结果表明基于本体的Internet动态路由实现框架可以提供稳定性和适应性，对解决Internet动态路由问题很有意义。
战地网络极易受到各种攻击和破坏，有效的密钥管理方案是实现安全通信的关键。多层移动Ad hoe网络是比较适合战地环境的一种网络组织机构，本文给出了一种基于身份的密钥管理方案并给出了详细的操作步骤，本方案不需要公钥证书的存在，用户以其身份标识作为公钥，明显降低了网络负载并且对节点计算能力和存储能力没有特殊的要求。从而更好的适应了战地网络环境。