Papers
UML-based Design of Synchronization Aspects
- A Structured Approach to Develop Concurrent Programs in UML, in Proc. of the Third International Conference on the Unified Modeling Langauge (UML2000), Lecture Notes in Computer Science 1939, pp 451-465.
- A Pattern-Based Approach to Develop Concurrent Programs in UML --- Part 1, Masaaki Mizuno, February 2001, KSU Technical Report 2001-02. (Send mail to masaaki@cis.ksu.edu for a copy of this paper).
- A Pattern-Based Approach to Develop Concurrent Programs in UML --- Part 2, Masaaki Mizuno, March 2001, KSU Technical Report 2001-03. (Send mail to masaaki@cis.ksu.edu for a copy of this paper).
Synthesis of Synchronization
- A Structured Approach for Developing Concurrent Programs in Java, Information Processing Letters, Vol 69, No 5, pp232-238, 1999.
- Invariant-based Specification, Synthesis, and Verification of Synchronization in Concurrent Programs, Xianghua Deng, Matthew Dwyer, John Hatcliff, and Masaaki Mizuno. Proceedings of the International Conference on Software Engineering (ICSE 2002), IEEE Press.
- Enhancing Real-Time Event Service for Synchronization in Object Oriented Distributed Systems, Gurdip Singh, Bob Maddula and Qiang Zeng. Proceedings of the IEEE International Symposium on Object Oriented Real-Time Computing, Washington, D.C., 2002
- Invariant Consistency: A Mechanism for Inter-Process Ordering in Distributed Shared Memory Systems, G. Singh, IEEE International Conference on Distributed Computing Systems, 2002.
- Region Synchronization in Message Passing Systems ,G. Singh and Ye Su, 31st International Conference on Parallel Processing, Vancouver, August 2002.
Model-checking Concurrent Java Software
For checking synchronization specifications and code generated using the SyncGen tool, the following paper is most appropriate.
- Invariant-based Specification, Synthesis, and Verification of Synchronization in Concurrent Programs, Xianghua Deng, Matthew Dwyer, John Hatcliff, and Masaaki Mizuno. To appear in the Proceedings of the Internation Conference on Software Engineering (ICSE 2002), IEEE Press.
For checking concurrent Java software in general, see some recent papers below from the Bandera group or see more papers on the Bandera project web-site
- Expressing Checkable Properties of Dynamic Systems: The Bandera Specification Language, June, 2001. James Corbett, Matthew Dwyer, John Hatcliff, and Robby KSU CIS Technical Report 2001-04. (Submitted for journal publication; this paper is an extended version of our 2000 Spin Workshop paper)
- Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software, John Hatcliff and Matthew Dwyer, in Proceedings of CONCUR 2001, Lecture Notes in Computer Science, August 2001.
- Tool-supported Program Abstraction for Finite-state Verification, Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Willem Visser and Hongjun Zheng, Proceedings of the 23rd International Conference on Software Engineering, May 2001.
- Finding Feasible Counter-examples when Model Checking Abstracted Java Programs, Corina S. Pasareanu, Matthew B. Dwyer and Willem Visser, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer-Verlag, April, 2001.
- Bandera : Extracting Finite-state Models from Java Source Code, James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, and Hongjun Zheng in Proceedings of the 22nd International Conference on Software Engineering, June, 2000.
Applications to Controller-Area-Network (CAN)
- Application Specific Ordering in Group Communication, G. Singh and S. Badarpura, IEEE International Workshop on Applied Research in Group Communication, April 2001.
- A Flexible Real-time Transport Protocol for Controller area Networks, Mitch Neilsen, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 250-256, June 25-28, 2001.
- Synthesizing Dependable Synchronization Code for CAN-based Applications, Y. Su, G. Singh,M. Mizuno, and M. Neilsen, IEEE Workshop on Reliability in Embedded Systems, October 2001. (To appear).