ACES
Sponsor: DARPA ITO/PCES
Approach
Kestrel’s ACES project aims to build a system to synthesize event-driven Real-Time Java (RTJ) applications from formal specifications that include real-time requirements, using stepwise refinement and aspect weaving.
We are currently in preliminary stages of investigating adequate modeling logics for the RTJ platform, and aiming this at:
- Specifications for the RTJ platform: The RTJ specification is currently under active design, with support from NIST. We envisage to enrich the language specification with mathematically precise descriptions that can be used directly for synthesis and analysis tools that interoperatve with RTJ.
- Program resynthesis: This investigates how to revise a program derivation according to changes made to its high-level specification.
- Type-based program analysis: This seeks to design expressive but tractable type systems that guarantee properties of embedded systems such as race- and deadlock-freedom.
Benefits
The anticipated benefits include:
- greater operational flexibility and robustness - rapid change;
- scalability through decentralization and synthesis of efficient code;
- software adaptation to actual operational conditions;
- high-assurance through correctness by construction;
- incremental software evolution.