Specifying modules to satisfy interfaces: A state transition system approach

Summary We defineinterface, module and the meaning ofM offers I, whereM denotes a module andI an interface. For a moduleM and disjoint interfacesU andL, the meaning ofM using L offers U is also defined. For a linear hierarchy of modules and interfaces,M ₁, I₁, M₂, I₂, ...,M _n, I_n, we present the following composition theorem: IfM ₁ offersI ₁ and, fori=2, ...,n, M _i usingI _i–1 offersI _i, then the hierarchy of modules offersI _n.Our theory is applied to solve a problem posed by Leslie Lamport at the 1987 Lake Arrowhead Workshop. We first present a formal specification of a serializable database interface. We then provide specifications of two modules, one based upon two-phase locking and the other multi-version timestamps; the two-phase locking module uses an interface offered by a physical database. We prove that each module offers the serializable interface. Simon S. Lam is Chairman of the Department of Computer Sciences at the University of Texas at Austin and holds and endowed professorship. His research interests are in the areas of computer networks, communication protocols, performance models, formal methods, and network security. He serves on the editorial boards ofIEEE Transactions on Software Engineering andPerformance Evaluation. He is an IEEE Fellow, and was a corecipient of the 1975 Leonard G. Abraham Prize Paper Award from the IEEE Communications Society. He organized and was program chairman of the first ACM SIGCOMM Symposium on Communications Architectures and Protocols in 1983. He received the BSEE degree (with Distinction) from Washington State University in 1969, and the MS and Ph.D. degrees from the University of California at Los Angeles in 1970 and 1974 respectively. Prior to joining the University of Texas faculty, he was with the IBM T.J. Watson Research Center from 1974 to 1977. A. Udaya Shankar received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, Kanpur, in 1976, the M.S. degree in Computer Engineering from Syracuse University, Syracuse, NY, in 1978, and the Ph.D. degree in Electrical Engineering from the University of Texas at Austin, in 1982. Since January 1983, he has been with the University of Maryland, College Park, where he is now an Associate Professor of Computer Science. Since September 1985, he has been with the Institute for Advanced Computer Studies at the University of Maryland. His current research interests include the modeling and analysis of distributed systems and network protocols, from both correctness and performance aspects. He is a member of IEEE and ACM.The work of Simon S. Lam was supported by National Science Foundation grants no. NCR-8613338 and no. NCR-9004464. The work of A. Udaya Shankar was supported by National Science Foundation grants no. ECS-8502113 and no. NCR-8904590