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. 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. 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.