Z规格说明自动生成器

来源 :计算机系统应用 | 被引量 : 0次 | 上传用户:gao1980623
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
形式化Z语言采用严格的数学理论可以有效提高软件的可靠性和鲁棒性,但是由于其包含的数学理论使得只有少数人能够熟练应用Z语言进行形式化规格说明书的编写.目前,多数对于Z语言的研究集中在理论阶段,还没有相应的工具支持Z规格说明的自动生成.本文中对于Z规格说明自动生成器的研究有助于降低Z规格说明书的编写难度,降低了形式化开发的难度及成本,对于形式化Z语言的推广具有重要的意义.
其他文献
针对传统身份识别技术存在的密码记忆难、隐私易泄露、信息易伪造等问题,提出并实现了基于安卓平台的混合特征在线手写笔迹识别算法.本算法通过迁移传统笔迹采集平台、采用文本相关与文本无关相结合的方式分别对静态纹理特征和动态矢量特征进行提取,弥补了当前笔迹采集困难、信息易伪造、准确性差等缺陷,实现了用户在移动设备上更加快捷安全的进行身份识别和鉴定.通过实验得出:该笔迹识别算法具有良好的稳定性、高可重复性、优
给出一种嵌入式平台QR码译码程序的移植方法.选用UP-NETARM2410-S嵌入式平台作为硬件开发平台,首先介绍了系统的硬件平台的组成,然后,对使用Qt-Creator进行QR码译码程序的开
近年来,随着移动互联网的快速发展,通信行业也进入了移动时代,企业的通信业务可以借助移动互联网结合融合通信拓展到移动领域.企业通讯录作为企业通信的入口起着至关重要的作
对ARM平台电机矢量控制模型进行了分析及性能评估,弥补了当前伺服控制系统中该评估工作的空白.分析了电机矢量控制模型和能实现该模型ARM平台的软硬件环境,给ARM平台电机矢量
针对多维敏感属性数据发布面临的一般泄露、交叉泄露、相似性泄露、多维独立泄露的威胁,本文提出了敏感属性敏感等级和敏感属性值敏感等级的概念,基于单维l-diversity模型,对
为了实现利用视频车辆检测器数据计算和预测路段行程时间,将排队长度数据应用到路段行程时间的计算中,采用改进粒子群的BP神经网络算法和时间序列分析对路段进行实证研究.将
针对移动云计算中资源发现能耗高的问题,提出了一种自适应、自动切换资源发现模式的高能效资源发现算法.首先,为两种主流移动资源发现模式分别建立能耗-资源质量模型;然后,利
随着无缝连接技术的发展,以多媒体应用服务为核心的无线电技术必须满足用户网络服务质量的要求. 对于异构无线网络,可能发生不同技术和管理域之间的切换,切换判决不再基于某一参
研究了面向服务的Web报表设计器,通过提供服务的方式保障系统功能需求.设计器作为一个粗粒度的服务,由多个细粒度的子服务构成,通过转换接口的方式为不同业务系统提供模板设
储层评价是油田有利区筛选及预测的重要基础和依据,针对传统AHP方法主观性强、判断矩阵不一致等问题,对AHP算法进行改进,提出一种基于改进AHP的储层综合评价方法.该方法采用