【摘 要】
：
XYZ/E语言是一个可执行的时序逻辑语言,可以用来描述有穷状态反应系统.为了构造一个以XYZ/E语言作为系统描述语言的模型检查工具,可以在已有的成熟模型检查工具的基础上,实现
论文部分内容阅读
XYZ/E语言是一个可执行的时序逻辑语言,可以用来描述有穷状态反应系统.为了构造一个以XYZ/E语言作为系统描述语言的模型检查工具,可以在已有的成熟模型检查工具的基础上,实现一个语言转换工具,把对反应系统的XYZ/E语言描述转换成该模型检查工具可接受的描述,然后利用该工具进行模型检查.SPIN是一个得到广泛应用的线性时序逻辑模型检查工具,能够验证由若干个进程异步组合而成的有穷状态系统,它使用进程元语言Promela来描述反应系统.我们实现了一个语言转换工具,可以把满足一定限制的XYZ/E程序转换成Promela程序,从而可以利用SPIN来对用XYZ/E语言描述的有究状态反应系统进行模型检查,达到了能够对用XYZ/E语言描述的有穷状态系统进行模型检查的目的.
其他文献
该文首先分析了互联网对信息检索技术提出的挑战,分析了传统搜索引擎的优缺点,并介绍了传统搜索引擎采用的基于Web内容分析方法的几种基本技术.基于Web结构分析的方法从Web的
随着信息化的深入发展，智能小区应运而生。智能小区的最典型的两个信息 化增值服务是卫星数字电视的接入和视频点播。数字电视比起传统的采用模拟信
软件漏洞使系统容易受到攻击,影响系统的可用性。软件漏洞中,复杂数据类型相关的漏洞占了较大的比例。在可执行程序中实现对此类漏洞有效检测,复杂数据类型的识别是关键。由
随着计算机应用的不断发展,软件作为信息系统的实现载体,已广泛应用在现代社会的各个领域,软件中的任何安全漏洞都可能导致非常严重的后果。软件测试是保证软件正确性、完整
随着计算机系统的互联，特别是通过Internet将各种计算机进行互联，大大拓展了信息资源共享空间和时间，提高了其利用率，同时也给计算机网络系统的安全性带来了前所未有的挑战。要实
该文基于构件技术设计了PnPMIS框架,支持集成管理信息系统的快速开发和集成,利用简单的接口实现模块的即插即用,在系统结构上提供可扩展、抗修改、可重用等支持,在用户界面上
该文在第一章主要针对目前视频点播技术的研究与发展现状作了分析;第二章介绍了半流式视频点播技术的定义和设计思想,并介绍了中大软件所开发的台山城域网VOD/COD系统;第三章
过去20多年来定理机器证明所获进展主要限于等式型定理的证明,而对不等式型定理机器证明的研究却举步维艰.1994年,周咸青、高小山等将"柱形代数剖分"原有算法和吴方法相结合,
微内核技术是对操作系统结构的一种革新.如何设计微内核的结构,在学术界有一些争论.在对微内核的两种基本结构进行了研究之后,该文采用了一种适用于嵌入式系统应用的微内核操
论文参考理想的绿噪声模型,着重分析和讨论了三种现有的绿噪声半色调技术:R.Levein提出的依赖输出反馈的误差扩散算法、Ostromoukhov的随机簇点抖动技术以及Leo Lau提出的bip