This Article 
 Bibliographic References 
 Add to: 
Formal Derivation of Concurrent Programs: An Example from Industry
May 1993 (vol. 19 no. 5)
pp. 503-528

The formal derivation of an implementation of the I/O (input/output) subsystem portion of an existing operating system is presented. The I/O subsystem is responsible for allocating I/O resources such as tapes, disks, I/O channels in response to requests from user processes. The derivation employs the UNITY methodology which captures the concurrent interaction of the I/O subsystem with its environment. The verified resource allocation algorithm that results from the derivation has been used as part of a high-level design by software engineers implementing the I/O subsystem. As the largest application to date of the UNITY methodology, the derivation illustrates a number of techniques for organizing large specifications and proofs.

[1] K. M. Chandy and J. Misra, "The drinking philosophers problem,"ACM Trans. Programming Lang. Syst., vol. 6, no. 4, pp. 632-646, 1984.
[2] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[3] D. M. Goldschlag, "Mechanically verifying concurrent programs with the Boyer-Moore prover,"IEEE Trans. Software Eng., vol. 16, no. 9, pp. 1005-1023, Sept. 1990.
[4] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: Prentice-Hall International, 1987.
[5] E. Knapp, "An exercise in formal development of parallel programs: maximum flow in graphs,"ACM Trans. Programming Languages and Syst., 12(2), pp. 203-221, Apr. 1990.
[6] S. S. Lam and A. U. Shankar, "A relational notation for state-transition systems,"IEEE Trans. Software Eng., vol. 16, no. 7, July 1990, pp. 755-775.
[7] L. Lamport, "Specifying Concurrent ProgramModules,"ACM Trans. Programming Languages and Systems, Vol. 5, No. 2, Apr. 1983, pp. 190-222.
[8] N. Lynch and M. R. Tuttle, "Hierarchical correctness proofs for distributed algorithms," inProc. Sixth Annu. ACM Symp. Principles of Distrib. Comput., 1987, pp. 137-151.
[9] S. Owicki and D. Gries, "An axiomatic technique for parallel programs I,"Acta Informatica, vol. 6, no. 1, pp. 319-340.
[10] M. G. Staskauskas, "The formal specification and design of a distributed electronic funds transfer system,"IEEE Trans. Comput., vol. 37, no. 12, pp. 1515-1528, Dec. 1988.
[11] M. G. Staskauskas, "Mapping the UNITY implementation of NIOS to the GCOS execution environment," The University of Texas at Austin, draft, Aug. 17, 1990.
[12] M. G. Staskauskas, "An exercise in verifying concurrent programs in industry: the I/O subsystem," inProc. 10th Annu. Phoenix Conf. Comput. and Commun., Mar. 1991, pp. 325-331.
[13] M. G. Staskauskas, "Specification and verification of large-scale reactive programs," Tech. Rep. TR-92-34, Dept. Comput. Sci., The University of Texas at Austin, July 1992.
[14] M. G. Staskauskas, "An experience in the formal verification of industrial software,"Commun. ACM, to be published.

Index Terms:
formal derivation; I/O subsystem; concurrent programs; operating system; tapes; disks; I/O channels; UNITY methodology; resource allocation algorithm; specifications; proofs; formal specification; parallel programming; program verification
M.G. Staskauskas, "Formal Derivation of Concurrent Programs: An Example from Industry," IEEE Transactions on Software Engineering, vol. 19, no. 5, pp. 503-528, May 1993, doi:10.1109/32.232015
Usage of this product signifies your acceptance of the Terms of Use.