A Contribution of Graph Grammar Techniques to the Specification, Verification and Certification of Code Generation Tools

AbstractThe software and hardware quality of safety-critical embedded systems in avionics and the automotive sector is currently ensured by extensive assurance procedures (e.g. certification). In this application area the use of models in the development of embedded systems has become increasingly important. These models are used from the early development stages through to implementation to verify desired software behaviour (model-based development). New approaches allow automatic generation of compact controller code directly from the software model via so-called code generators. However, certifying a code generator (as well as a compiler) premises a complete and comprehensible description of the translation process from the model to the generated code. This paper proposes the use of different graph grammar techniques as a basis for the specification and verification of the transformation process as a contribution to the certification of code generation tools