Formal Synthesis of Generators for Embedded Systems
Principal Investigators: Dr John Anton & Dr Lindsay Errington
Sponsor: DARPA ITO/MOBIES
Kestrel's objectives in the FORGES project is to synthesize domain-specific generators for developing and testing embedded software. These tools will employ automated reasoning and synthesis techniques to reduce the time and cost of developing embedded software, and to provide greater confidence that systems meet their requirements.
Kestrel's approach is to capture existing domain knowledge in automated tools that support engineers in designing and implementing embedded systems.
Kestrel will incorporate this domain knowledge, along with generic software design principles and implementation techniques, into its general-purpose specification and synthesis tool to construct domain-specific development and testing environments.
Using a development environment, engineers will formally define the requirements on an embedded software system and incrementally develop the system by selecting and composing components and frameworks. Engineers will be guided and assisted during development by the environment which will, for example, manage requirements and constraints. It will ensure that the constraints are not violated when a component is selected and will propagate the constraints to the remaining, uninstantiated parts of the framework. In this way, engineers can explore the design space and, at each stage of development, assess the implications of a design decision (e.g., which component is selected) with respect to the overall constraints. Moreover, at each stage, the tool will allow a user to visualize the constraint margins with ``gauges''.
This combination of formal methods, automated reasoning and incremental component selection and their application to embedded systems is novel. It offers a number of benefits.
Another novel aspect of Kestrel's work is how these tools will be produced. To avoid writing new tools for each application domain or when there are small changes to a domain, Kestrel will synthesize the tools automatically. By extending Kestrel's synthesis technology, generic algorithms will be automatically refined using domain knowledge to yield domain-specific tools. The domain knowledge includes the taxonomies of components and formal specifications of the target frameworks described above.
Slides from the MoBIES PI meeting in New Orleans, January 23-25, 2001
- Back to Top -