Jonathan Jacky

University of Washington
Orthopaedics and Sports Medicine
Box 356500
Seattle, Washington 98195-6500
Phone:   206-543-3690


1972 - 1977 Ph.D. Physiology and Biophysics University of Washington (UW)
1968 - 1972 B.S. Biology and Engineering California Institute of Technology


2002 - present Research Scientist Orthopaedics and Sports Medicine Department, UW, Seattle, WA
2003 - 2004 Visisting Researcher Microsoft Research, Redmond, WA
2002 - 2003 Senior Software Architect Modeled Computation LLC, Seattle, WA
2000 - 2001 Adjunct Faculty The Evergreen State College, Olympia, WA
1991 - 2002 Research Scientist Radiation Oncology Department, UW, Seattle, WA
1984 - 1991 Research Assistant Professor Radiation Oncology Department, UW, Seattle, WA
1982 - 1984 Systems Programmer Radiation Oncology Department, UW, Seattle, WA
1980 - 1982 Scientific Programmer Radiation Oncology Department, UW, Seattle, WA
1977 - 1980 Research Fellow Pediatrics Department, UW, Seattle, WA


Clinical Neutron Therapy System: Produced a real-time safety-critical control system for a unique radiation therapy machine now in use treating cancer patients at University of Washington Medical Center. Responsible for entire project from specification through design, coding, testing, installation, staff training and ongoing support; also hiring and project management. Modeled and analyzed the design using the Z notation and the SMV model checker. The control program is coded in C and runs under the VxWorks operating system. It was developed under Unix (HP-UX) using Wind River's Tornado cross-development product. (UW) [html]

Web Services: Analyzed specifications (written in prose and XML) for proposed web services. Reported omissions, ambiguities, and inconsistencies; proposed solutions. Modeled the services in AsmL, an executable specification language. Demonstrated service behaviors in interesting scenarios by executing the models. (Modeled Computation)

DICOM-RT: Produced a facility that transfers treatment beam setup information from a treatment planning system to computer-controlled radiation therapy machines over a computer network using an industry-standard protocol, DICOM-RT. The facility is coded in Common Lisp. It is now in use at University of Washington Medical Center. (UW) [html]

Foundations of Computing: Created and taught an intensive year-long introduction to computer science for undergraduates, including programming (in Scheme, awk, and Java), systems (the Linux operating system and TCP/IP networks), as well as readings and seminars on the social, economic, and human factors aspects of computing. (Evergreen) [html]

The Way of Z: Wrote a textbook on Z, a formal notation for specifying, designing and analyzing computer software and systems, now used in industry training and university software engineering courses around the world. (UW) [html]

Radiotherapy Treatment Planning Tools: Chaired National Cancer Institute task group that designed a language-independent API for radiation therapy-planning software. We specified API language bindings in C and Common Lisp. I coded the C library, built it, and ran application programs that usedit at U.W. and other NCI-funded research centers. (UW) [html]

Selected Publications

A control system for a radiation therapy machine. (with Ruedi Risler and four co-authors) Technical Report 2001-05-01, Radiation Oncology Department, University of Washington, Seattle, WA, May 2001. [html, pdf]
Formal safety analysis of the control program for a radiation therapy machine. In Wolfgang Schlegel and Thomas Bortfeld, editors, The Use of Computers in Radiation Therapy: XIIIth International Conference, pages 68-70. Springer, 2000. [html, pdf]
Analyzing a real-time program with Z. In Jonathan Bowen, Andreas Fett, and Michael Hinchey, editors, ZUM '98: The Z Formal Specification Notation. Eleventh International Conference of Z Users, Springer-Verlag, 1998. Lecture Notes in Computer Science. (This analysis also used the SMV model checker.) [html, ps, SMV code]
The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, 1997. [html]
Safety-critical computing: hazards, practices, standards, and regulation. In Rob Kling, editor, Computerization and Controversy: Value Conflicts and Soc`ial Choices. Academic Press, 1996. (second edition). [html]
Portable software tools for 3-D radiation therapy planning. (with 13 co-authors) International Journal of Radiation Oncology, Biology and Physics, 30(4):921-928, November 1994. [html, ps]
Testing a 3-D radiation therapy planning program. (with Cheryl White) International Journal of Radiation Oncology, Biology and Physics, 18:253-261, January 1990. [html]
An object-oriented approach to a large scientific application. (with Ira Kalet) In Norman Meyrowitz, editor, OOPSLA '86 Object Oriented Programming Systems, Languages and Applications Conference Proceedings, pages 368-376. Association for Computing Machinery, 1986. (also SIGPLAN Notices, 21(11), Nov. 1986). [html]
Programmable gas mixer for controlling concentration as a function of time. Journal of Applied Physiology: Respiratory, Environmental and Exercise Physiology, 49(1):160-166, 1980. [html]

Complete list of publications [html]

Printer-friendly version of this resume [PDF, PS, HTML, MS Word, plain text]