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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Automated verification of code generated from models: Comparing specifications with observations


    Additional title:

    Automatische Verifizierung von aus Modellen generiertem Code: Vergleich von Spezifikationen mit Beobachtungen


    Contributors:


    Publication date :

    2008


    Size :

    10 Seiten, 2 Bilder, 4 Tabellen, 8 Quellen




    Type of media :

    Conference paper


    Type of material :

    Storage medium


    Language :

    English




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

    Gerlich, R. / Sigg, D. / European Space Agency | British Library Conference Proceedings | 2008


    Automated testing from specifications

    Srinivasan, J. / Leveson, N. | IEEE | 2002



    Automated derivation of tests from specifications

    Stoitsev, Todor / Straw, Steven / Legat, Christoph et al. | AIAA | 2018