微机仿真系统中形式化方法的应用

Z语言是一种广泛应用的形式化语言，适合于仿真实时软件系统的需求规格说明．通过微机系统仿真软件的Z规格说明，讨论了Z语言在实时系统开发中使用的一些方法、对典型问题的处理原则以及操作同时序关系的描述．     

多视点实时形式化方法的应用模式

RT-Z结合了Z的状态描述能力和Timed CSP对并发实时进程的描述能力,成为一种有效的实时并发软件的开发手段。RT-Z不但是一种规格说明语言,也可以用于建模．多视点的软件开发方法的研究从不同的视点观察系统,分离各自的关注点。简化了系统的设计．本文在形式化方法RT-Z的基础上扩充语法框架,以支持多视点工程的思想,充分利用形式化方法的精化推理机制,同时具有对实时约束的描述能力,可作为并发实时系统开发中的基本模式．     

基于C++STL的Z规格说明数据类型的表示

介绍了Z规格说明的数据类型和它们的分类,从定义出发,阐述了这些数据类型派生的派生与继承关系．以Z规格说明向可执行代码的自动转换为目的,结合C 语言中STL模板库对数据结构和通用算法的强大支持功能,提出了用STL中的容器表示Z规格说明数据类型的方法。     

基于Z语言的互联网登陆系统的形式化规格与验证

Z语言是一种基于集合和一阶谓词逻辑的模式规约语言,可产生精确地需求规格说明.本文用形式化语言Z对互联网登陆系统的主要操作模式进行规格说明,接着通过形式化验证,证明设计的规格说明能够满足用户的需求,提高了系统的可靠性和稳定性.     

基于ＯＯＺＳ的ＵＭＬ类图形式化描述及其应用

统一建模语言UML是一种面向对象分析和设计过程中重要的建模工具。但由于UML缺乏精确的形式化语义,不利于对其所描述的需求进行进一步分析和验证。这一点上,形式化方法可与之互补。基于此,本文采用一种面向对象的、基于Z的扩展语言OOZS———结构化面向对象形式规格说明语言,对UML的类图进行了形式化描述,寻求一种在软件设计与系统建模过程中UML到OOZS的映射与转换机制,最后给出一个基于OOZS的UML类图的形式化描述实例,结果表明本文的研究工作在实践中是可行的。     

需求分析的 Z 语言形式化方法

非形式化的需求规格说明容易产生歧义,导致所开发的软件系统不能满足用户的功能要求.Z语言是一种基于集合和一阶谓词逻辑的模式规约语言,可用于产生精确的需求规格说明.介绍了需求分析的Z语言形式化方法,并给出了一个通用堆栈的Z语言描述实例,同时指出这种形式化方法有待进一步研究的地方.     

传感器数据流实时语义注释方法研究

为了对微环境监测平台上的传感器所捕获的异构、大量、连续的数据流进行语义注释,从而及时地根据语义上下文推理出新的或隐含的知识,以实现微环境监测平台的实时监测,对SASML映射语言和SDRM算法进行了研究和改进,设计了S-SASML映射语言和SDS2R算法,用于将传感器原始数据流转换为符合SOSA/SSN本体的RDF数据流;并利用线程池技术实现方法的高并发处理,提高了方法的实时性能。改进后的映射语言和算法实现了微环境监测平台对连续、大量的数据流的实时语义注释,不仅解决了动态传感器数据流语义注释的问题,而且避免了高频数据流导致的系统过载现象,具有稳定高效的处理能力,基本满足了微环境监测平台的需求,具有一定的应用价值。     

基于前后断言的多线程形式功能规格说明语言

探索用基于公理语义的前后断言方法来刻划多线程程序的功能，设计了一个功能规格说明语言ＪＡＶＡＳＰＥＣ，用来形式地表达程序的功能规格说明，为支持多线程的Ｊａｖａ程序自动生成奠定了基础     

WSDL→Radl-WS生成方法及自动转换系统

精确地描述Web服务语义对Web服务的发现、执行、动态组合和交互至关重要.在Radl语言基础上,扩展Radl为Radl-WS,提出一种新型的基于Radl-WS代数规范的Web服务建模语言.该建模语言统一了基于代数公理方法和Hoare公理方法来描述软件规格说明.为支持模型转换,提出了将WSDL语言描述的Web服务通过等价变换生成为Radl-WS建模语言的方法,并设计了相应的WSDL→Radl-WS自动转换系统.最后采用真实案例,验证了该方法的有效性.     

用形式化和非形式化技术对VB程序逆向工程

研究了采用形式化和非形式化相结合的方法，为VB程序生成形式化规格说明的逆向工程技术。给出了VB语言基本结构的最强后件语义表示、模式匹配规则、抽象匹配规则以及产生规格说明的基于结构化分析的3阶段过程。在此基础上使用VB语言实现了原型工具BasicSpec。此工具首先为VB程序建立非形式化的抽象模型：窗体结构图和过程调用图；然后为关键模块生成形式化规格说明。生成的结果清晰明确，有助于软件工程师理解VB源程序。     

一种形式语言代数模型

针对形式语言研究的国内外现状,对形式系统规约描述语言的数学模型进行了初步探讨,建立了一种形式语言的代数模型,依据软件重用的思想及转换语义的方法提出了语言重用的概念,根据软件工程分层设计原则构建了形式语言族模型.该模型在不同层次上描述复杂形式系统软件规约的抽象表达程度,适于复杂形式系统的开发与测试.此外,文中应用范畴理论...     

一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法

形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一,尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作,以自定义泛型抽象顺序设计语言Apla为基础,进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言,使其既支持顺序算法的验证又能有效地验证并发分布式算法.在依赖-卫式推理的基础上,提出一种新颖的2层并发分布式算法形式化验证方法,其中系统层用于处理并发级验证,而组件层用于处理顺序级验证.最后,通过2个实例验证了该方法的有效性和可行性.     

一种在万维网上显示Z规格说明的方法

万维网的普及和发展给软件工程师提供了交流和共享知识的场所。Ｚ是一种基于一阶谓词逻辑和集合论的形式规格说明语言,Ｚ语言用大量的数学符号和模式来构造规格说明,然而,当前的ＨＴＭＬ标准不支持在万维网上显示Ｚ规格说明所需的一些符号,此外如何在ＨＴＭＬ文件中表示模式框、公理框和类描述同样是困难的,本文实现了一种在万维网上显示Ｚ规格说明的解决方法,并给出了程序代码和实例。     

基于ZML的Z语言规范

ISO的Z标准为Z语言工具的开发及不同Z开发工具间的互操作提供了基础,然而它所建立的只是开发工具必须遵守和使用记号,而没有说明如何实现这些记号。ZML采用XML模式文档形式来描述Z语言规范,可以实现Z语言在不同工具间的交换。本文讨论XML模式的重用、替换设计机理在ZML中的应用;并讨论了在设计ZML时,所引入的XML模型元素与Z标准对应的问题;以及随着ZML的演化,如何减少Z语言XML文档的开发维护时间问题。     

分布式工程数据库系统中事务管理机制相关技术的研究

从分布式工程设计事务环境和事务管理特点出发,给出一种分布式工程数据库系统（DEDBS）事务管理子系统的体系结构,提出一种适用于DEDBS中的事务两阶段提交协议,介绍两种支持工程设计事务的并发控制方法;基于20L的扩充分层封锁模型的并发控制方法和改进的乐观并行控制方法。     

Refinement and Transformation from Z Specification to C + +

As a kind of formal specification language, Z has gained a position in the field of software development, but there is still no standard way of transforming Z specification into executable code that is promising in increasing the quality, reusability and maintainability of software. With the automatic programming model of software engineering, through the analysis for Z specification language, a feasible semi-automatic way of refinement and transformation is proposed, and the correctness of the procedure is also discussed.     

形式规约模式及其重用技术研究综述

设计模式的形式规约描述的研究对于设计模式的广泛重用具有重要意义.规约模式就是用某种形式化语言表示的设计模式.文章从模式定义、重用机制、可用工具、方法可用性等角度分析比较了几种主要的设计模式形式化方法.最后讨论了当前存在的问题及其发展趋势。     

函数－规约混合语言的设计与实现

在函数式语言中引入约束类型和优化规则定义机制，并将扩展的函数式语言与代数规约说明语言相结合，支持从规约到程序的设计，并提高编程的效率及灵活性．混合语言系统将代数规约转换为合流的重写系统，将函数定义、计算约束和优化规则视为重写规则，基于重写模型，以平行最外方法辅以必要归约进行计算．