Automating commutativity analysis at the design level

ABSTRACT

Two operations commute if executing them serially in either order results in the same change of state. In a system in which commands may be issued simultaneously by different users, lack of commutativity can result in unpredictable behaviour, even if the commands are serialized, because one user's command may be preempted by another's, and thus executed in an unanticipated state. This paper describes an automated approach to analyzing commutativity. The operations are expressed as constraints in a declarative modelling language such as Alloy, and a constraint solver is used to find violating scenarios. A case study application to the beam scheduling component of a proton therapy machine (originally specified in OCL) revealed several violations of commutativity in which requests from medical technicians in treatment rooms could conflict with the actions of a beam operator in a master control room. Some of the issues involved in automating the analysis for OCL itself are also discussed.

REFERENCES

• 1: BRAT, G., HAVELUND, K., PARK, S., AND VISSER, W. Java PathFinder - A second generation of a Java modelchecker. In Workshop on Advances in Verification (July 2000).
• 2: Object Modeling with the OCL, The Rationale behind the Object Constraint Language, January 2002
• 3: Alan Fekete , Nancy Lynch , Michael Merritt , William Weihl, Commutativity-based locking for nested transactions, Journal of Computer and System Sciences, v.41 n.1, p.65-156, August 1990 [doi>10.1016/0022-0000(90)90034-I]
• 4: FOOD AND DRUG ADMININSTRATION. FDA Statement on Radiation Overexposures in Panama. http://www.fda.gov/cdrh/ocd/panamaradexp.html.
• 5: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 6: HUSSMANN, H., DEMUTH, B., AND FINGER, F. Modular Architecture for a Toolset Supporting OCL. In Proceedings of UML 2000: Advancing the Standard (York, UK, Oct. 2000), A. Evans, S. Kent, and B. Selic, Eds., no. 1939 in LNCS.
• 7: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 8: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 9: J.R. BURCH, E.M. CLARKE, K.L. MCMILLAN, D.L. DILL, AND L.J. HWANG. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (Washington, D.C., 1990), IEEE Computer Society Press, pp. 1--33.
• 10: N. G. Leveson , C. S. Turner, An Investigation of the Therac-25 Accidents, Computer, v.26 n.7, p.18-41, July 1993 [doi>10.1109/MC.1993.274940]
• 11: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 12: MIT SOFTWARE DESIGN GROUP. The Alloy Analyzer. http://alloy.mit.edu.
• 13: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 14: Mark Richters , Martin Gogolla, OCL: Syntax, Semantics, and Tools, Object Modeling with the OCL, The Rationale behind the Object Constraint Language, p.42-68, January 2002
• 15: RICKS, R. C., BERGER, M. E., HOLLOWAY, E. C., AND GOANS, R. E. REACTS Radiation Accident Registry: Update of Accidents in the United States. International Radiation Protection Association, 2000.
• 16: Martin C. Rinard , Pedro C. Diniz, Commutativity analysis: a new analysis technique for parallelizing compilers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.942-991, Nov. 1997 [doi>10.1145/267959.269969]
• 17: WARMER, J., Ed. Response to the UML 2.0 OCL RfP (ad/2000-09-03). Object Management Group, Jan. 2003. Revised submission, version 1.6. OMG Document ad/2003-01-07.
• 18: Jos Warmer , Anneke Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 19: W. E. Weihl, Commutativity-Based Concurrency Control for Abstract Data Types, IEEE Transactions on Computers, v.37 n.12, p.1488-1505, December 1988 [doi>10.1109/12.9728]
• 20: WU, P., AND FEKETE, A. An empirical study of commutativity in application code. In Proceedings of International Database Engineering and Applications Symposium (Hong Kong, July 2003).

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

  H. Information Systems
  H.1 MODELS AND PRINCIPLES
      H.1.2 User/Machine Systems

General Terms:
Design, Human Factors, Reliability, Verification

Keywords:
OCL, alloy, case study, commutativity, concurrency, critical systems, formal specification, lightweight formal methods, model checking, proton therapy, radiation therapy, testing