Embedded software is widely used in automotive applications, often in critical situations where reliability of the system is extremely important. Such systems often use model based development approaches. Model transformation is an important step in such scenarios. This includes generating code from models, transforming design models into analysis models, or transforming a model between variants of a formalism (such as variants of Statecharts). It becomes important to verify that the transformation was correct, and the transformed model or code preserved the semantics of the design model. In this paper, we will look at a technique called “goal-directed certification” that provides a pragmatic solution to the verification problem. We will see how we can use concepts of bisimulation to verify whether a certain transformation instance preserved certain properties. We will then extend this idea using weak bisimulation and semantic anchoring, to a more general class of transformations.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Towards Verification of Model Transformations Via Goal-Directed Certification


    Contributors:

    Conference:

    Automotive Software Workshop ; 2006 ; San Diego, CA, USA March 15, 2006 - March 17, 2006



    Publication date :

    2008-01-01


    Size :

    17 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Towards Verification of Model Transformations Via Goal-Directed Certification

    Karsai, G. / Narayanan, A. | British Library Conference Proceedings | 2008


    A goal-directed transportation planning model

    Morlok, Edward K. | Elsevier | 1969




    The Multiple Process Model of Goal-directed Reaching Revisited

    Elliott, D / Lyons, J / Hayes, SJ et al. | BASE | 2017

    Free access