Automatic Derivation, Integration and Verification of Synchronization Aspects in Object-Oriented Design Methods


ProjectTitleLine:
Automatic Derivation, Integration and Verification of Synchronization Aspects in Object-Oriented Design Methods
Period:
01 July 2000 through 30 June 2004
Grant Number:
DARPA Order K203/AFRL Contract F33615-00-C-3044
Investigators:
Matthew Dwyer, John Hatcliff, Masaaki Mizuno, Mitch Neilsen, Gurdip Singh
InstitutionLine:
Kansas State University
POC:
dwyer@cis.ksu.edu
Objective:
In this project we investigate solutions to the problem of implementing robust, efficient global synchronization policies in concurrent object-oriented software.

Synchronization is an important aspect in the design of complex, concurrent embedded systems. Object-oriented analysis and design techniques have been used successfully to design and maintain large software systems, but multiple shortcomings in their treatment of synchronization aspects limit their effectiveness in many applications. We propose to advance the use of object-oriented methodologies to design high-assurance embedded systems by addressing the following challenges:

To meet these challenges, we will develop techniques, tools and methodologies that support high-level specifications of synchronization aspects, derivation and weaving of aspect code into core functional code written in languages commonly used for embedded applications. This will involve the following activities.

The impact of this work will be immediate and measurable because it addresses limitations in commonly used methods and tools. We will demonstrate this by providing a repository of case-studies. In particular, we will evaluate the effectiveness of our techniques by developing components for Common Digital Architecture (CDA101) --- an evolving standard for networking target vehicle electronics including seaborne targets (ST-2000, Navy) ground targets, and airborne targets (MQM-107, Army; BQM-74, Air Force).


Project Reports


Talks


Milestones


Project Publications

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

  1. 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.
  2. A Structured Approach to Develop Concurrent Programs in UML, Masaaki Mizuno, Mitch Neilsen and Gurdip Singh, in Proceedings of the Third International Conference on the Unified Modeling Langauge, Sept, 2000.
  3. 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.
  4. Application Specific Ordering in Group Communication, G. Singh and S. Badarpura, IEEE International Workshop on Applied Research in Group Communication, April 2001.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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)
  10. A Pattern-Based Approach to Develop Concurrent Programs in UML --- Part 1, Masaaki Mizuno, March 2001, KSU Technical Report 2001-03. (Send mail to masaaki@cis.ksu.edu for a copy of this paper)
  11. Expressing Checkable Properties of Dy namic Systems: The Bandera Specification Language, June, 2001. James Corbett, Matthew Dwyer, John Hatcliff, and Robby to appear in Springer-Verlag's International Journal on Software Tools for Technology Transfer.
  12. Invariant-based Specification, Synthesis, and Verification of Synchronization in Concurrent Programs, Xianghua Deng, Matthew B. Dwyer, John Hatcliff, and Masaaki Mizuno, to appear in Proceedings of the 24th International Conference on Software Engineering (ICSE), 2002.

Related Links