The S2aVES project (Specification, Synthesis, and Verification of Embedded Systems) is investigating 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.
The project seeks 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, the project is developing 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 involves the following activities.
- Designing a high-level domain-specific language for specifying synchronization aspects such as coordination, scheduling and distribution. This language is integrated with the various intermediate specification stages of the Unified Software Development Process (USDP) of the Unified Modeling Language (UML). We have implemented the SyncGen tool to automatically translate these high-level specifications to synchronization code in multiple target languages including Java and C++.
- Using static analysis and program specialization techniques to weave synchronization aspects with core functionality code to achieve efficient implementations.
- Collecting a repository of high-level synchronization specification patterns for common synchronization problems. Elegant composition properties make it easy to compose these patterns to form more complex specifications.
- Using existing light-weight verification techniques 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.
We believe the impact of this work can be immediate and measurable because it addresses limitations in commonly used methods and tools. We are demonstrating this by providing a repository of case-studies. In particular, we are evaluating 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).