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
- Program resynthesis: This investigates how to revise a
program derivation according to changes made to its high-level
- 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.
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.
- Back to Top -