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.
Chapter PDF
References
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.
Ashcroft, E. and Wadge, W.W. (1977) Lucid: a non-procedural language with iteration, Communications of ACM, 20, 7.
Chandy, K.M. and Misra, J. (1988) Parallel Program Design, Addison-Wesley.
Manna, Z. and Pnueli, A. (1996) Clocked transition system, Logic and Software Engineering (ed. A. Pnueli and H. Lin), World Scientific Singapore.
Pnueli, A. (1996) Preface to (Manna and Pnueli, 1996). Ibid.
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.
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.
Tang, Z. (1996) An outline of the XYZ system. In (Manna and Pnueli, 1996). Ibid.
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.
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.
Zhang, W. (1995) Verification of XYZ/SE programs, Chinese Journal of Advanced Software Research, 4, Allerton Press, New York.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 IFIP
About this chapter
Cite this chapter
Tang, Z. (1998). A temporal logic language for system implementation. In: Horspool, R.N. (eds) Systems Implementation 2000. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35350-0_23
Download citation
DOI: https://doi.org/10.1007/978-0-387-35350-0_23
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2873-5
Online ISBN: 978-0-387-35350-0
eBook Packages: Springer Book Archive