AFRL Contract F33615-00-C-3044 Progress Report : July, 2000


Synchronization is an important aspect in the design of complex, concurrent embedded systems. It is also notoriously difficult to implement efficient, robust synchronization solutions, especially in the context of object-oriented systems. We propose to advance the use of object-oriented methodologies to design high-assurance embedded systems by developing a high-level, modular approach for specification of global synchronization policies and technologies for automatically integrating implementations of the specified policies into core functional code. The resulting systems will have known synchronization properties (by construction) and will be amenable to further analysis for critical safety/liveness properties.


Our approach to this problem is to leverage our previous work in the development of distributed protocol implementations and in finite-state verification of software. The "paper" approaches to synchronization protocols will be integrated into a tool-based framework that includes sophisticated program analysis and transformation components (developed for our finite-state verification work). This will enable high-level specifications of protocols to be mapped onto selected concurrency models and optimized. Finally, code will be generated for these optimized realizations of synchronization policy and integrated with a user supplied functional core code base.

Work will proceed simultaneously along several fronts including the development of the foundations of synchronization specifications, analysis of and code generation for such specifications, optimization of integrated synchronization and functional code, and application and assessment of these technologies on realistic embedded systems applications.

This will result in an integrated collection of software development tools that largely automate the process of defining, implementing, and validating synchronization aspects of concurrent, embedded applications. The high degree of tool support and automation promises to make these techniques accessible to practicing software developers.

Recent Accomplishments:

New Start

Current Plan:

Our initial plans involve work in four areas.

Work is underway on formalization of the basic approach to counter-based global invariants. We plan to expand this work to include more general synchronization patterns that might be specified using, e.g., a temporal logic.

Based on the results of this formalization process, we will begin the process of defining a linguistic framework for writing synchronization aspect specifications. This framework will allow for high-level synchronization patterns to be defined.

Tool support to process synchronization specifications (syntactic and semantic), analyze them and produce intermediate representations that are amenable to further analysis, optimization and code-generation will be developed.

We will gather a collection of applications drawn from the domain of Controller Area Network (CAN) applications. These embedded systems are commonly found in both commercial and military on-board vehicle systems. We will assess the flexibility and generality of the synchronization aspect specifications in terms of their support for these applications.

Technology Transition:

New Start