Z语言的实时扩展及应用
摘要
实时软件系统在现代工业和社会生活中扮演着越来越重要的角色，随着需求的逐步增加，实时系统的软件开发方法学渐渐成为研究的热点问题。形式化方法在实时系统的开发过程中的使用也越来越多，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集成还是使用规格描述语言转换的非集成方法都不能很好地解决系统设计的所有问题，因此在实时系统设计中选择合适的方法是非常重要的。经过进一步研究，我们在微机仿真系统的设计过程中提取了通用的设计模式，这个模式基于多视点的软件工程方法，采用集成方法从功能视点得到的规格说明和采用非集成方法从控制视点得到的规格说明在一个统一的语义下结合起来，这样就可以利用两种规格说明方法直接得到在语法和机制上一致的规格说明，因此可以避免单独使用两种方案所产生的缺陷。
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 the
formal 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.
在本文，我们归纳了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集成还是使用规格描述语言转换的非集成方法都不能很好地解决系统设计的所有问题，因此在实时系统设计中选择合适的方法是非常重要的。经过进一步研究，我们在微机仿真系统的设计过程中提取了通用的设计模式，这个模式基于多视点的软件工程方法，采用集成方法从功能视点得到的规格说明和采用非集成方法从控制视点得到的规格说明在一个统一的语义下结合起来，这样就可以利用两种规格说明方法直接得到在语法和机制上一致的规格说明，因此可以避免单独使用两种方案所产生的缺陷。
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 the
formal 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.
引文
[1] 罗秉安．软件能力成熟度模型在实时系统开发中的应用[硕士学位论文]广东工业大学 2003年
[2] 周之英．编著 现代软件工程 科学出版社 2001
[3] 徐其龙．实时控制网络通讯协议的研究、设计与实现[硕士学位论文] 合肥工业大学 2002年
[4] 董护斌．面向实时系统的实时区域时态逻辑：RRTL[硕士学位论文] 西北工业大学 2002年
[5] J.E.Cooling. Software design for real-time System.New York:Chapman and Hall, 1991
[6] H.Gomma.Software design methods for concurrent and real-time systems.Reading MA:Address Wesley,1993
[7] 顿海强．基于Z对UML中Use Case图的形式化[硕士学位论文] 郑州大学 2002年
[8] 郑红军，张乃武．软件开发过程中的形式化方法．计算机科学．1997，VOL．22，NO．5
[9] 侯建民，李宣东，郑国梁．实时系统软件开发过程中形式方法的作用 计算机应用与软件 2002年04期
[10] 缪淮扣，高晓雷，李刚．结构化方法、面向对象方法和形式方法的比较与结合 计算机工程与科学 1999年第21卷第4期
[11] 缪淮扣，李刚，朱关铭 编著 软件工程语言-Z 上海科学技术文献出版社 1999年4月 第1版
[12] M. Awad, et al. Object-Oriented Technology for Real-time System. Prentice Hall PTR.Upper saddle River.UJ07458,1996
[13] Spiver J.M. The Z notation: a reference manual,second edition Prentice Hall International (UK) Ltd. 1992
[14] 刘玲，缪淮扣．Z规格说明构造方法 计算机工程 2000年2月第26卷第6期
[15] 何炎强，宋强，黄谦．从过程描述语言到Z语言 小型微型计算机系统 2002 23(9)：1110-1113
[16] 毋国庆，杨杰，王敏，应时．描述实时系统需求的模型 小型微型计算机系统 2001 22(4)：
473-476
[17] 微型计算机原理及应用 郑学坚，周斌 编著 清华大学出版社(第二版)1995年8月
[18] Araki, K., Galloway, A. and Taguchi, K., editors: Proceedings of the 1st International Conference on Integrated FormalMethods. Springer-Verlag, 1999.
[19] Benjamin, M.: A message passing system: an example of combining CSP and Z. In J. E. Nicholls, editor, 4th Z UserWorkshop, Workshop in Computing, pages 221 {228, 1990.
[20] Butler, M. J.: Re_nement and decomposition of value-passing action systems. In E. Best, editor, Proceedings of CONCUR ,number 715 in Lecture Notes in Computer Science. Springer-Verlag, 1993.
[21] Bolognesi, T., van de Lagemaat, J. and Vissers, C.: LOTOSphere: Software Development with LOTOS. Kluwer Academic Publishers, 1995.
[22] Davies, J.: Speci_cation and Proof in Real-Time CSP. Technical monograph, Oxford University, 1993.
[23] Derrick, J., Boiten, E., Bowman, H. and Steen, M.: Supporting ODP: translating LOTOS into Z. In E. Najm and J.-B.Stefani, editors, Proceedings of FMOODS '96, pages 399 {406. Chapman & Hall, 1996.
[24] Fischer, C.: How to combine Z with a process algebra. In J. P. Bowen, A. Fett, and M. G Hinchey, editors, ZUM '98: The Z Formal Speci_cation Language, number 1493 in Lecture Notes in Computer Science, pages 5 {23. Springer-Verlag, 1998.
[25] Galloway, A. and Stoddart, B.: Integrated formal methods. In Proceedings ofINFORSID '97, 1997.
[26] Heisel, M. and S"uhl, C.: Methodological support for formally specifying safety-critical software. In Proceedings 16th International Conference on Computer Safety, Reliability and Security. Springer-Verlag, 1997.
[27] Mahony, B. and Dong, J. S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering, 26(2): 150 {176,2000.
[28] Schneider, S.: Concurrent and Real-Time Systems: The CSP Approach. John Wiley & Sons, 1999.
[29] Smith, G: A semantic integration of Object-Z and CSP for the speci_cation of concurrent systems.
In J. Fitzgerald, C.B.Jones, and R Lucas, editors, Proceedings of FME'97, number 1313 in Lecture Notes in Computer Science, pages 62 {81.Springer-Verlag, 1997.
[30] Smith, G: The Object-Z Speci_cation Language. Advances in Formal Methods Series. Kluwer Academic Publishers, 2000.
[31] Suhl, C.: RT-Z: An integration of Z and timed CSE In Araki et al. [AGT99], pages 51 {65.
[32] Suhl, C.: Applying RT-Z to develop safety-critical systems. In T. Maibaum, editor, Proceedings of the Third InternationalConference on Fundamental Approaches to Software Engineering (FASE 2000), number 1783 in Lecture Notes in ComputerScience, pages 51 {65. Springer-Verlag, 2000.
[33] Woodcock, J. C. E and Davies, J.: Using Z: Speci_cation, Re_nement, and Proof. Prentice-Hall, a.Software design methods for concurrent and real-time systems.Reading MA:Address Wesley,1993
[2] 周之英．编著 现代软件工程 科学出版社 2001
[3] 徐其龙．实时控制网络通讯协议的研究、设计与实现[硕士学位论文] 合肥工业大学 2002年
[4] 董护斌．面向实时系统的实时区域时态逻辑：RRTL[硕士学位论文] 西北工业大学 2002年
[5] J.E.Cooling. Software design for real-time System.New York:Chapman and Hall, 1991
[6] H.Gomma.Software design methods for concurrent and real-time systems.Reading MA:Address Wesley,1993
[7] 顿海强．基于Z对UML中Use Case图的形式化[硕士学位论文] 郑州大学 2002年
[8] 郑红军，张乃武．软件开发过程中的形式化方法．计算机科学．1997，VOL．22，NO．5
[9] 侯建民，李宣东，郑国梁．实时系统软件开发过程中形式方法的作用 计算机应用与软件 2002年04期
[10] 缪淮扣，高晓雷，李刚．结构化方法、面向对象方法和形式方法的比较与结合 计算机工程与科学 1999年第21卷第4期
[11] 缪淮扣，李刚，朱关铭 编著 软件工程语言-Z 上海科学技术文献出版社 1999年4月 第1版
[12] M. Awad, et al. Object-Oriented Technology for Real-time System. Prentice Hall PTR.Upper saddle River.UJ07458,1996
[13] Spiver J.M. The Z notation: a reference manual,second edition Prentice Hall International (UK) Ltd. 1992
[14] 刘玲，缪淮扣．Z规格说明构造方法 计算机工程 2000年2月第26卷第6期
[15] 何炎强，宋强，黄谦．从过程描述语言到Z语言 小型微型计算机系统 2002 23(9)：1110-1113
[16] 毋国庆，杨杰，王敏，应时．描述实时系统需求的模型 小型微型计算机系统 2001 22(4)：
473-476
[17] 微型计算机原理及应用 郑学坚，周斌 编著 清华大学出版社(第二版)1995年8月
[18] Araki, K., Galloway, A. and Taguchi, K., editors: Proceedings of the 1st International Conference on Integrated FormalMethods. Springer-Verlag, 1999.
[19] Benjamin, M.: A message passing system: an example of combining CSP and Z. In J. E. Nicholls, editor, 4th Z UserWorkshop, Workshop in Computing, pages 221 {228, 1990.
[20] Butler, M. J.: Re_nement and decomposition of value-passing action systems. In E. Best, editor, Proceedings of CONCUR ,number 715 in Lecture Notes in Computer Science. Springer-Verlag, 1993.
[21] Bolognesi, T., van de Lagemaat, J. and Vissers, C.: LOTOSphere: Software Development with LOTOS. Kluwer Academic Publishers, 1995.
[22] Davies, J.: Speci_cation and Proof in Real-Time CSP. Technical monograph, Oxford University, 1993.
[23] Derrick, J., Boiten, E., Bowman, H. and Steen, M.: Supporting ODP: translating LOTOS into Z. In E. Najm and J.-B.Stefani, editors, Proceedings of FMOODS '96, pages 399 {406. Chapman & Hall, 1996.
[24] Fischer, C.: How to combine Z with a process algebra. In J. P. Bowen, A. Fett, and M. G Hinchey, editors, ZUM '98: The Z Formal Speci_cation Language, number 1493 in Lecture Notes in Computer Science, pages 5 {23. Springer-Verlag, 1998.
[25] Galloway, A. and Stoddart, B.: Integrated formal methods. In Proceedings ofINFORSID '97, 1997.
[26] Heisel, M. and S"uhl, C.: Methodological support for formally specifying safety-critical software. In Proceedings 16th International Conference on Computer Safety, Reliability and Security. Springer-Verlag, 1997.
[27] Mahony, B. and Dong, J. S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering, 26(2): 150 {176,2000.
[28] Schneider, S.: Concurrent and Real-Time Systems: The CSP Approach. John Wiley & Sons, 1999.
[29] Smith, G: A semantic integration of Object-Z and CSP for the speci_cation of concurrent systems.
In J. Fitzgerald, C.B.Jones, and R Lucas, editors, Proceedings of FME'97, number 1313 in Lecture Notes in Computer Science, pages 62 {81.Springer-Verlag, 1997.
[30] Smith, G: The Object-Z Speci_cation Language. Advances in Formal Methods Series. Kluwer Academic Publishers, 2000.
[31] Suhl, C.: RT-Z: An integration of Z and timed CSE In Araki et al. [AGT99], pages 51 {65.
[32] Suhl, C.: Applying RT-Z to develop safety-critical systems. In T. Maibaum, editor, Proceedings of the Third InternationalConference on Fundamental Approaches to Software Engineering (FASE 2000), number 1783 in Lecture Notes in ComputerScience, pages 51 {65. Springer-Verlag, 2000.
[33] Woodcock, J. C. E and Davies, J.: Using Z: Speci_cation, Re_nement, and Proof. Prentice-Hall, a.Software design methods for concurrent and real-time systems.Reading MA:Address Wesley,1993