|
2002 FREENIX Track Technical Program - Abstract
X Meets Z: Verifying Correctness In
The Presence Of POSIX Threads
Bart Massey, Computer Science Department, Portland State University; Robert Bauer, Rational Software Corporation
Abstract
The engineering of freely-available UNIX software normally
utilizes an informal analysis and design process coupled
with extensive user testing. While this approach is often
appropriate, there are situations for which it produces
less-than-stellar results.
A case study is given of such a situation that arose during
the design and implementation of a thread-safe library for
interaction with the X Window System. XCB is a C binding
library for the X protocol designed to work transparently
with either single-threaded or multi-threaded clients.
Managing XCB client thread access to the X server while
honoring the constraints of both XCB and the X server is
thus a delicate matter.
The problem of ensuring that this complex system is coded
correctly can be attacked through the use of lightweight
formal methods. A model is constructed of the troublesome
portion of the system using the Z formal specification
notation. This model is used to establish important system
properties and produce C code with a high likelihood of
correctness.
- View the full text of this paper in
HTML and
PDF.
The Proceedings are published as a collective work, © 2002 by the USENIX Association. All Rights Reserved. Rights
to individual papers remain with the author or the author's employer.
Permission is granted for the noncommercial reproduction of the complete
work for educational or research purposes. USENIX acknowledges all
trademarks within this paper.
- If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.
 To become a USENIX Member, please see our Membership Information.
|
Need help? Use our Contacts page.
Technical Program