by Holger Giese, Sabine Glesner, Johannes Leitner, Wilhelm Schäfer, Robert Wagner
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.
Reference:
Towards Verified Model Transformations (Holger Giese, Sabine Glesner, Johannes Leitner, Wilhelm Schäfer, Robert Wagner), In Proc. of the 3rd International Workshop on Model Development, Validation and Verification (MoDeVa), Genova, Italy (David Hearnden, J.G. Süß, Benoît Baudry, Nicolas Rapin, eds.), Le Commissariat à l'Energie Atomique - CEA, 2006.
Bibtex Entry:
@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.}
}