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