Copyright © 2004-2017 BSSE.
All rights reserved.
Impressum Privacy Policy/Datenschutzerklärung Legal Notice

Document: Automated Verification of Code Generated from Models: Comparing Specifications with Observations

Automated Verification of Code Generated from Models: Comparing Specifications with Observations [00070]
EventDASIA 2008
Date27 May 2008 - 30 May 2008
LocationPalma de Mallorca, Spain
Files

Certification is based on compliance of the code of the code generator with given standards. Such compliance never can guarantee correctness of the whole chain through transformation down to the environment for execution, though the belief is that certification implies well-formed code at a reduced fault rate.

The approach presented here goes a direction different from manual certification.. It is guided by the idea of automated proof: each time code is generated from a model the properties of the code when being executed in its environment are compared with the properties specified in the model. This allows to conclude on the correctness of the whole chain for every application and related generated code.