Reference:
, "Towards Verified Model Transformations", in David Hearnden, J.G. Süß, Benoît Baudry, Nicolas Rapin, Eds., Proc. of the 3rd International Workshop on Model Development, Validation and Verification (MoDeVa), Genova, Italy, pp. 78–93, Le Commissariat à l'Energie Atomique - CEA, October 2006.
Abstract:
Model-driven software development (MDD) is seen as a promising approach to improve software quality and reduce production costs significantly. However, one of the problems in using MDD especially in the area of safety-critical systems is the lack of verified transformations. The verification of crucial safety properties on the model level is only really useful, if the automatic code generation is also guaranteed to be correct, i.e., the verified properties are guaranteed to hold also for the generated code. This particularly means to check semantic equivalence, at least to a certain extent between the model specification and the generated code. This paper addresses the problem of verifying that a given transformation ensures semantic equivalence between an arbitrary model in a given model specification language and the resulting programming language code. While the presented approach ensures that the transformation algorithm is correct, existing related work is restricted on verifying only the correctness of a particular transformation result.
Links:
@InProceedings{GieseGLSW06,
AUTHOR = {Giese, Holger and Glesner, Sabine and Leitner, Johannes and Sch\"{a}fer, Wilhelm and Wagner, Robert},
TITLE = {{Towards Verified Model Transformations}},
YEAR = {2006},
MONTH = {October},
BOOKTITLE = {Proc. of the 3rd International Workshop on Model Development, Validation and Verification (MoDeVa), Genova, Italy},
PAGES = {78--93},
EDITOR = {Hearnden, David and Süß, J.G. and Baudry, Benoît and Rapin, Nicolas},
PUBLISHER = {Le Commissariat à l'Energie Atomique - CEA},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2006/GGL+06.pdf},
OPTacc_url = {},
PDF = {uploads/pdf/GGL+06_ag_2006_Giese_Glesner_Leitner_Schäfer_Wagner_Towards Verified Model Transformations.pdf},
OPTacc_pdf = {},
ABSTRACT = {Model-driven software development (MDD) is seen as a promising approach to improve software quality and reduce production costs significantly. However, one of the problems in using MDD especially in the area of safety-critical systems is the lack of verified transformations. The verification of crucial safety properties on the model level is only really useful, if the automatic code generation is also guaranteed to be correct, i.e., the verified properties are guaranteed to hold also for the generated code. This particularly means to check semantic equivalence, at least to a certain extent between the model specification and the generated code. This paper addresses the problem of verifying that a given transformation ensures semantic equivalence between an arbitrary model in a given model specification language and the resulting programming language code. While the presented approach ensures that the transformation algorithm is correct, existing related work is restricted on verifying only the correctness of a particular transformation result.}
}Copyright notice: This material is presented to ensure timely dissemination of
scholarly and technical work. Copyright and all rights therein are retained by
authors or by other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each author's copyright.
In most cases, these works may not be reposted without the explicit permission of
the copyright holder.
Powered by
bibtexbrowser