Z语言的实时扩展及应用

【作者】 陈广明；

【导师】 张立臣；

【作者基本信息】 广东工业大学 ， 软件工程， 2004， 硕士

【摘要】 实时软件系统在现代工业和社会生活中扮演着越来越重要的角色，随着需求的逐步增加，实时系统的软件开发方法学渐渐成为研究的热点问题。形式化方法在实时系统的开发过程中的使用也越来越多，Z语言是一种广泛应用的形式化规格说明语言，然而，它并不是为处理系统的动态行为而设计的，因此对Z进行扩充以适应实时应用的需要是非常重要的。 在本文，我们归纳了Z实时扩展，提出了分类标准，一类是被称为集成的扩展方法，它基于形式化说明语言Z和其它形式化方法的集成，在这里由其它形式化方法提供表示动态行为的结构；另一类称之为非集成的扩展方法则只使用Z的语义，而由其它形式化方法对时间约束性和并发进行的描述则被转换成Z规格说明，完成了上述分析之后实际就给出了一个对Z进行实时扩展的通用方法。 一种被称为RT-Z的基于规格描述语言Z和timed CSP的实时扩展是集成扩展方法的典型代表，RT-Z将Z和timed CSP的功能用一个紧密的框架结合起来，实际上无论是Z还是timed CSP都缺乏对结构化的支持机制，为了能适应系统复杂性的需要，RT-Z另外引入了对结构化的支持机制。RT-Z的语义基于Z和timed CSP，这是它具有正确性和数学严格性的基础。RT-Z可以用于需求描述，也可以用于设计阶段，非常适合于实时系统的开发。 另一方面，使用过程描述语言可以方便的描述时序关系，在本文中，我们也讨论了这种非集成的扩展方式，它能够利用时序状态转换系统将过程描述语言转换为Z规格。 通常，实时系统开发依赖于时间约束性和复杂的外部因素，因此无论是采用Z和timed CSP集成还是使用规格描述语言转换的非集成方法都不能很好地解决系统设计的所有问题，因此在实时系统设计中选择合适的方法是非常重要的。经过进一步研究，我们在微机仿真系统的设计过程中提取了通用的设计模式，这个模式基于多视点的软件工程方法，采用集成方法从功能视点得到的规格说明和采用非集成方法从控制视点得到的规格说明在一个统一的语义下结合起来，这样就可以利用两种规格说明方法直接得到在语法和机制上一致的规格说明，因此可以避免单独使用两种方案所产生的缺陷。更多还原

【Abstract】 Real-time software system has been acting as a more and more important role in our industry and sociallife .With requirements growing rapidly, the developing methodology for real-time systems gradually becomes the focus of researchers. Formal methods has gained huge popularity in real-time system domains . Z is a wide used formal specifiation and calculated to describe the real-time system ,However,it is not designed to model aspects of the dynamic behaviour.It is significant to extend Z to suit requirement for real-time applications.now , we summarize classifications of the real-time extension of Z . a species of methods has based on integration of the formal specification Z and other formal specification can provide adequate constructs to model for dynamic behaviour, the other side of shield ,the another method has only based on semanteme of Z and translate the specifications of other farmal method into Z specification to describe timing constraints and concurrents . then we can extract a general method about to extent Z in real-time domain .It is famous typification of integration method that we present an integration of the formal specification languages Z and timed CSP, called RT-Z, incorporating their combined strengths in a coherent frame. To cope with complex systems, RT-Z is equipped with structuring constructs built on top of the integration, because both Z and timed CSP lack appropriate facilities. The formal semantics of RT-Z, based on the denotation semantics of Z and timed CSP, is a prerequisite for preciseness and mathematical rigour. RT-Z is intended to be used in the requirements denotation and design phases of the system and software development process. The envisaged application area is the development of real-time systems.On the other hand ,it is convenient to describe the temporal relations Using process descrption.in this paper ,is discussed for translating description of process description language to Z specifiation,and temporal status transition system is used as intermediary.generally ,real-time system development depend on its timing constraints and complicated factors of outside , consequently Not only the integration method of theformal specification languages Z and timed CSP but also translating description of process description language to Z specifiation can not solve all this problem.it is important to choose the suitable mothods in real-time software developments, further on,we extract a design pattern from the instance of real-time simulative system development. this pattern is based on multi-viewpoint software engineering .the specifications of non-integration formalism derive from control view-point and the specifications of integrantion derive from function view-point are combined into an uniform semanteme ,therefor the storng conherence between the formalisms and the notational conciseness of being able to directly merge the syntaxes of the formalisms. They hence avoid some disadvantages of both other classes.更多还原