Certification does not guarantee at all that the generated code does comply with the model. 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. The paper presents and discusses this approach and first results obtained from practice in the context of the ISG modelling environment. In chapter 2 the principal approach to verification of the whole chain is explained. Chapter 3 identifies the steps needed in practice for auto-proving. Chapter 4 discusses the current results. In chapter 5 the chosen approach is compared to model verification based on Message Sequence Charts (MSC). Finally, conclusions are drawn in chapter 6.
Automated verification of code generated from models: Comparing specifications with observations
Automatische Verifizierung von aus Modellen generiertem Code: Vergleich von Spezifikationen mit Beobachtungen
2008
10 Seiten, 2 Bilder, 4 Tabellen, 8 Quellen
Conference paper
Storage medium
English
Automated Verification of Code Generated from Models: Comparing Specifications with Observations
British Library Conference Proceedings | 2008
|Automated testing from specifications
IEEE | 2002
|Comparing ionospheric models with mid-latitude ionosonde observations
Elsevier | 2008
|Automated derivation of tests from specifications
AIAA | 2018
|Comparing ionospheric models with mid-latitude ionosonde observations
Online Contents | 2009
|