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:

• high-level, modular specification of global, cross-cutting synchronization aspects,
• automatic derivation and weaving (i.e., integration) of verifiable synchronization code into core functional code,
• automated verification of critical safety and liveness properties of woven embedded code.

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.

• A high-level domain-specific language for specifying synchronization aspects such as coordination, scheduling and distribution, will be developed. This language will be integrated with the various intermediate specification stages of the Unified Software Development Process (USDP) of the Unified Modeling Language (UML). Tools will be implemented to automatically translate these high-level specifications to synchronization code in multiple target languages including Java and C++.
• Static analysis and program specialization techniques will be used to weave synchronization aspects with core functionality code to achieve efficient implementations.
• A repository of high-level synchronization specification patterns will be provided for common synchronization problems. Elegant composition properties make it easy to compose these patterns to form more complex specifications.
• Existing light-weight verification techniques will be used to build domain-specific software model-checking engines that can (a) verify that synchronization aspect code conforms to its specification, and (b) verify crucial safety and liveness properties of woven code.

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

• Project Quad-Chart : July, 2000 (powerpoint)
• Project Progress Report : July, 2000
• Project Progress Report : January, 2001
• Project Plan : August, 2001
• Project Progress Report : January, 2002

Talks

• Project summary at status report from February 2001 PI Meeting (San Diego).
• Project summary at status report from May 2001 PI Meeting (St. Louis).

Milestones

• (Winter 2001) We have applied the global-invariant based synchronization specification methodology (by hand) to (re)implement solutions for a wide-variety of synchronization problems from the concurrency literature, for example, the textbooks by Andrews and Hartley.
• (Winter 2001) We have developed a systematic approach to calculating the coarse-grain, i.e., await statement, solution for a synchronization specification. This approach uses automated decision procedures for a logic with quantifier-free arithmetic terms to optimize the solution. For the examples described above, this method automatically produces the same solutions as were produced by hand.
• (Spring 2001) Implementation of coarse-grain solution approach using the Stanford Validity Checker.
• (Spring 2001) Implementation of initial code generators to produce Java and C code, the latter with calls to POSIX library routines.
• (Summer 2001) Design and implementation of a solution that generates distributed synchronization code for CAN-based control systems. specifications. We have performed experiments that show that using the broadcasting capability of the CAN networks, the distributed solution outperforms the solution based on a centralized monitor.
• (Summer 2001) Extension of the Bandera toolset to construct checkable models of systems from a hybrid of the coarse-grain solution and functional core code for static synchronization. The results provide for both verification of the correctness of generated synchronization implementations and for significant (more than 3 order of magnitude) reductions in the cost of checking properties of generated applications.
• (in progress) Extension of code generators and verification support to handle dynamic, i.e., group forming, synchronization patterns.
• (in progress) Modification of the TAO real-time event service to incorporate synchronization capabilities. We have developed a technique to transform our high-level synchronization specification into an implementation in TAO event service.

Project Publications

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

• The SAnToS Laboratory at Kansas State University
• The Real Time Embedded Systems Laboratory at Kansas State University
• Computing and Information Sciences Department home page
• DARPA Project Reporting Site
• DARPA Information Technology Office
• Air Force Research Laboratory