FORGES: Formal Synthesis of Generators for Embedded Systems
Lindsay Errington · Defense Technical Information Center (DTIC) · 2005
A number of tools exist that allow engineers to construct models of embedded systems. Models are expressed in a variety of languages including domain specific languages. These models provide input to generators that: 1) produce code, test suites, views of components in the model, and/or 2) analyze or compose models. Generators, however, are often difficult and expensive to develop. Moreover, due to the safety critical nature of embedded systems, it is crucial that generators be high assurance. This project has developed technology for the automated synthesis of model-based generators from language meta-models. Using partial evaluation, Kestrel has demonstrated the synthesis of generators that are provably correct, and that can be produced and modified with drastically less time and effort compared with manual production. The success of the project can be traced to two major contributions. The first, a technology breakthrough, is a new tractable formulation of partial evaluation. The second is a collection of meta-models that serve as comprehensive definitions of the semantics of widely-used commercial modeling languages.