We have developed a product-oriented certification approach that does not rely on the correctness of the code generator itself but uses mathematical reasoning to demonstrate that every individually generated program is free of different defect classes.
Reliable Autocoding from High-Level Models
Autocoding from domain-specific high-level models can increase productivity and flexibility in a spiral software development process, but conventional autocoding techniques lack the required reliability and assurance. Using automatic code generation from high-level models instead of manual low-level coding enables software developers to focus on understanding the problem. This increases productivity and flexibility in the software development process and decreases turn-around times. The reliable autocoding technique developed here helps to realize this potential for the high-reliability exploration systems.
We have developed a product-oriented certification approach in which the code generator is extended to generate not only the code, but at the same time also auxiliary information that supports independent safety arguments for every generated program individually. An external trusted tool or verification condition generator
(VCG) processes this information together with the program and produces a number of safety obligations. The program is safe with regard to the applied safety policy if all emerging obligations can formally be shown by an external prover (ATP); the proofs can be double-checked by an independent proof checker. Our approach is justified by the soundness of the applied mathematical reasoning: errors in either part of the code generator (i.e., the original generator or the certification extension) will lead to formally unprovable safety obligations.
Automatic code generation from domain-specific high-level models allows developers to focus on understanding the problem and frees them from understanding and implementing the low-level algorithmic details of the solution.
This can increase productivity and flexibility in a spiral development process.
Conventional autocoding techniques lack the reliability and assurance required for future exploration missions. In particular, any safety argument for the generated code relies on the correctness of the code generator itself. In practice, this cannot be demonstrated because code generators for relevant application domains are complex and dynamic systems.
- Supports customizable and domain-specific safety policies
- Applicable to arbitrary code generators
- Based on formal mathematical reasoning
- Interfaces to different off-the-shelf theorem provers
- Fully automatic certification, no false positives
- Generation of human-readable safety documents
- Integration with requirements and design documentation