共查询到16条相似文献,搜索用时 62 毫秒
1.
一种从Z到精化演算的软件开发方法 总被引:3,自引:0,他引:3
一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解,并通 相似文献
2.
一种基于Z和精化演算的形式化开发方法 总被引:1,自引:0,他引:1
通过分析Z和精化演算各自的特点,本文提出了一种使两者无缝集成的形式化开发方法。该方法利用Z良好的描述特性和扩充的类机制,将系统规约直妆定义成精化演算中的抽象程序,然后用精化规则对抽象程序逐步精化,直到可执行程序。最后给出了一个简单例子。 相似文献
3.
4.
5.
利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。 相似文献
6.
并行程序设计是并行计算的难点之一。提出了一种将设计模式用于程序精化演算的并行程序设计方法。它通过在Z语言的Schema演算体系中扩充并行的概念和表示,使用设计模式,将问题求解和并行开发的知识进行形式化的定义与描述,通过扩充的Schema演算将其与模型规范进行复合,逐步精化得到抽象并行程序。通过实例对这一方法进行了详细的描述。 相似文献
7.
提出了并发系统的一种规约方法.这一方法可用于对并发系统进行建模和对模型的验证.将形式化工具融入到一种二维的规约方法中,这样就能使形式化工具更易于应用到并发软件的开发过程中.此外,还提出了一种并发系统的形式化抽象模型. 相似文献
8.
9.
在总结和评价现有Z语言面向对象扩充的基础上,设计了一种新的扩充语言GOOZ,该语言克服了Z++,Object_Z等语言的一些缺点,其书写规约具有简洁,明确,接口定义清晰,模块无整,结构良好,易于验证的特点。 相似文献
10.
11.
The fact that Z is a specification language only, with no associated program development method, is a widely recognised problem.
As an answer to that, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows
its style and conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly in
that ZRC is completely formalised. In this paper, we explain how programs can be derived from Z specifications using ZRC.
We present ZRC-L, the language of our calculus, and its conversion laws, which are concerned with the transformation of Z
schemas into programs of this language. Moreover, we present the weakest precondition semantics of ZRC-L, which is the basis
for the derivation of the laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement for Z.
Received July 1997 / Accepted in revised form October 1998 相似文献
12.
The advantage of COOZ(Complete Object-Oriented Z) is to specify large scale software,but it does not support refinement calculus.Thus its application is comfined for software development.Including refinement calculus into COOZ overcomes its disadvantage during design and implementation.The separation between the design and implementation for structure and notation is removed as well .Then the software can be developed smoothly in the same frame.The combination of COOZ and refinement calculus can build object-oriented frame,in which the specification in COOZ is refined stepwise to code by calculus.In this paper,the development model is established.which is based on COOZ and refinement calculus.Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement,since data refinement usually has to be done on a large program component at once.As to the implementation technology of refinement calculus,the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered. 相似文献
13.
本文介绍了一种基于形式化规格说明语言COOZ的面向对象设计方法并给出实例。该方法用COOZ描述类的设计规格说明,实现了从形式化需求描述到形式化设计的平滑过渡。文中重点讨论了与设计方法有关的一些面向对象概念:对象类型和类的分开、子类型和继承的分开、灵活的消息传递和参数转换机制、主动对象和被动对象、根类的定义等。 相似文献
14.
This article discusses mutation testing strategies in the context of refinement. Here, a novel generalization of mutation testing techniques is presented to be applied to contracts ranging from formal specifications to programs. It is demonstrated that refinement and its dual abstraction are the key notions leading to a precise and yet simple theory of mutation testing. The refinement calculus of Back and von Wright is used to express the concepts like contracts, useful mutations, test-cases and test-coverage. 相似文献
15.
精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明. 相似文献
16.
基于细胞膜演算的Web服务事务处理形式化描述与验证 总被引:4,自引:0,他引:4
采用细胞膜演算具体分析了当前比较主流的Web服务中原子事务协调协议WS-AT.针对WS-AT协议采用简单的状态转换表和转换图,无法描述协调者和多个参与者的复杂协调活动,采用细胞膜演算给出了其形式化描述,用于规范协调者和参与者的活动,并分析了该协议的活性和安全性,得到了38187个状态.模型检验的实验结果表明,该协议满足稳定性、一致性和非平凡性,而不满足非阻塞性.进而,分析出注册和协调协议混在一起是其不满足非阻塞性的原因. 相似文献