Home : Current Projects : FORGES
 

FORGES

Formal Synthesis of Generators for Embedded Systems

Principal Investigators: Dr John Anton & Dr Lindsay Errington

Sponsor: DARPA ITO/MOBIES

Objective

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.

Approach

Kestrel's approach is to capture existing domain knowledge in automated tools that support engineers in designing and implementing embedded systems.

• Kestrel will formalize existing domain models of embedded components that have been produced by practicing domain experts (expressed, e.g., in UML or MatLab/Simulink). Kestrel will capture such knowledge as timing properties, memory constraints, functionality and reliability.
• Kestrel will formalize existing domain models of embedded system frameworks that constrain how components are composed and interact.
• Kestrel will construct multiple, inter-related taxonomies of the models that rank components and frameworks in terms of, for example, functionality and cost.

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.

• Incremental selection with constraint checking leads to early detection of constraint violations. For example, the development environment may aid the engineer in detecting that subtle interactions between components violate cross-cutting constraints (such as timing and memory constraints). Early detection of constraint violations reduces the time and hence the cost of developing embedded software.
• Formalizing the constraints that a framework imposes on components supports parallel development.  Separate teams of engineers can develop components independently but with confidence that the integrated system will meet the overall requirements.
• The availability of formal specifications for both the components and the overall requirements gives confidence in the coverage of the tests generated from them, for example, by ensuring cases are not missed.
• The formal specifications associated with components creates opportunities for context dependent optimizations during component integration and consequently better performance.

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.

Materials

Slides from the MoBIES PI meeting in New Orleans, January 23-25, 2001

Project reports: January, February, March.

- Back to Top -

- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -