Abstract
We wrote a formal specification in Z for the graphical user interface of a radiation therapy machine. We implemented our specification in a Pascal dialect on a workstation that uses the X window system to manage the keyboard and display. We initially model the user interface as a collection of separate Z operation schemas based on the informal prose requirements. From these we derive a state machine model, represented as a state transition table whose entries are schema names from the Z specification. Our state transition table format compactly represents nested states that are modelled in Z by schema inclusion. We implement each table entry as a Pascal function or procedure. We also implement a dispatcher that selects the proper state transition whenever any X event occurs; our dispatcher is the X event loop. Our dispatcher is a table-driven interpreter that can handle any state transition system expressed in the format we defined. We model the dispatcher in Z and formally derive some of its code. Experiences implementing and testing the program are described.
Preview
Unable to display preview. Download preview PDF.
References
Jonathan P. Bowen. X: Why Z? Computer Graphics Forum, 11(4):221–234, October 1992.
Digital Equipment Corporation, Maynard, Massachusetts. Introduction to VAXELN, October 1991.
Digital Equipment Corporation, Maynard, Massachusetts. VAXELN: Pascal Programming Guide, December 1991.
Jonathan Jacky. Formal specifications for a clinical cyclotron control system. In Mark Moriconi, editor, Proceedings of the ACM SIGSOFT International Workshop on Formal Methods in Software Development, pages 45–54, Napa, California, USA, May 9–11 1990. (also in ACM Software Engineering Notes, 15(4), Sept. 1990).
Jonathan Jacky. Formal specification and development of control system input/output. In J. P. Bowen and J. E. Nicholls, editors, Z User Workshop, London 1992, pages 95–108. Proceedings of the Seventh Annual Z User Meeting, Springer-Verlag, Workshops in Computing Series, 1993.
Jonathan Jacky. Specifying a safety-critical control system in Z. IEEE Transactions on Software Engineering, 21(2):99–106, 1995. (also in [15], pages 388–402).
Jonathan Jacky, Ruedi Risler, Ira Kalet, and Peter Wootton. Clinical neutron therapy system, control system specification, part I: System overview and hardware organization. Technical Report 90-12-01, Radiation Oncology Department, University of Washington, Seattle, WA, December 1990.
Jonathan Jacky, Ruedi Risler, Ira Kalet, Peter Wootton, and Stan Brossard. Clinical neutron therapy system, control system specification, part II: User operations. Technical Report 92-05-01, Radiation Oncology Department, University of Washington, Seattle, WA, May 1992.
Jonathan Jacky and Jonathan Unger. Formal specification of control software for a radiation therapy machine. Technical Report 94-07-01, Radiation Oncology Department, University of Washington, Seattle, WA, July 1994. (Draft).
Matthew S. Jaffe, Nancy G. Leveson, Mats P. E. Heimdahl, and Bonnie E. Melhart. Software requirements analysis for real-time process control systems. IEEE Transactions on Software Engineering, 17(3):241–258, March 1991.
Adrian Nye. Xlib Programming Manual. O'Reilly and Associates, Inc., Sebastopol, CA, 1988.
R. W. Scheifler and J. Gettys. The X window system. ACM Transactions on Graphics, 5(2):79–109, 1986.
J. M. Spivey. The fuzz Manual. J. M. Spivey Computing Science Consultancy, Oxford, second edition, July 1992.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, Hemel Hempstead, second edition, 1992.
J. C. P. Woodcock and P. G. Larsen, editors. FME '93: Industrial-Strength Formal Methods, Odense, Denmark, April 1993. First International Symposium of Formal Methods Europe, Springer-Verlag. Lecture Notes in Computer Science 670.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacky, J., Unger, J. (1995). From Z to code: A graphical user interface for a radiation therapy machine. In: Bowen, J.P., Hinchey, M.G. (eds) ZUM '95: The Z Formal Specification Notation. ZUM 1995. Lecture Notes in Computer Science, vol 967. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60271-2_128
Download citation
DOI: https://doi.org/10.1007/3-540-60271-2_128
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60271-2
Online ISBN: 978-3-540-44782-5
eBook Packages: Springer Book Archive