Advertisement

A temporal logic language for system implementation

Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

The XYZ system consists of a temporal logic language XYZ/E and several supporting tools. This paper introduces many special features of XYZ/E with its tools which are desirable for a good implementation language in addition to portability and efficiency. These features include (1) its suitability for stepwise refinement, specification of different abstract levels, verification and rapid prototyping, (2) modules and visual tools to support programming in the large and and (3) a simple, formal method and a corresponding tool for transforming a program from another source language into XYZ/E, a feature which is useful for software reengineering and for embedding standard programs from other languages into an XYZ/E.

Keywords

Temporal logic language system implementation language stepwise-refinement specification verification prototyping module visual tools 

References

  1. Abrial, J.R., Boerger, E., and Langmaack (1996) Formal methods for industrial applications: specifying and programming the steam boiler. Lecture Notes in Computer Science, volume 1165, Springer-Verlag, Berlin.CrossRefGoogle Scholar
  2. Ashcroft, E. and Wadge, W.W. (1977) Lucid: a non-procedural language with iteration, Communications of ACM, 20, 7.CrossRefGoogle Scholar
  3. Chandy, K.M. and Misra, J. (1988) Parallel Program Design, Addison-Wesley.zbMATHGoogle Scholar
  4. Manna, Z. and Pnueli, A. (1996) Clocked transition system, Logic and Software Engineering (ed. A. Pnueli and H. Lin), World Scientific Singapore.Google Scholar
  5. Pnueli, A. (1996) Preface to (Manna and Pnueli, 1996). Ibid.Google Scholar
  6. Shen W. and Tang, Z. (1994) The correct translation for programming languages and its application in the XYZ system, Chinese Journal Of Advanced Software Research 4.Google Scholar
  7. Shen W. and Tang, Z, (1998) Domain orientation based on the XYZ system, To appear in Chinese Journal of Advanced Software Research 1, Allerton Press, New York.Google Scholar
  8. Tang, Z. (1996) An outline of the XYZ system. In (Manna and Pnueli, 1996). Ibid.Google Scholar
  9. Yan, A. and Tang, C.S. (1997a) A unified linear time temporal logic solution to the “Steam Boiler Control Specification Problem”, Laboratory of Computer Science, Institute of Software, CAS. Technical report ISCAS-LCS-97–5.Google Scholar
  10. Yan, A. and Tang, C.S. (1997b) Building hybrid real-time system in XYZ/E. Laboratory of Computer Science, Institute of Software, CAS. Technical report ISCAS-LCS-97–6.Google Scholar
  11. Zhang, W. (1995) Verification of XYZ/SE programs, Chinese Journal of Advanced Software Research, 4, Allerton Press, New York.Google Scholar

Copyright information

© IFIP 1998

Authors and Affiliations

  • Z. Tang
    • 1
  1. 1.Institute of SoftwareBeijingChina

Personalised recommendations