by
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 (), In Proc. of the $3^rd$ International Workshop on Model Development Validation and Verification (MoDeV$^2$a), Genova, Italy (Hearnden, David, Süß, J.G., Baudry, Beno^it, Rapin, Nicolas, eds.), Le Commissariat `a l'Energie Atomique - CEA, 2006.
Bibtex Entry:
@InProceedings{GieseGLSW06_1,
AUTHOR = {Giese, Holger and Glesner, Sabine and Leitner, Johannes and Schafer},
TITLE = {{Towards Verified Model Transformations}},
YEAR = {2006},
MONTH = {October},
BOOKTITLE = {Proc. of the $3^rd$ International Workshop on Model Development Validation and Verification (MoDeV$^2$a), Genova, Italy},
PAGES = {78--93},
EDITOR = {Hearnden, David and Süß, J.G. and Baudry, Beno^it and Rapin, Nicolas},
PUBLISHER = {Le Commissariat `a l'Energie Atomique - CEA},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2006/GGL+06.pdf},
PDF = {uploads/pdf/GGL+06_ag_2006_Giese_Glesner_Leitner_Sch�fer_Wagner_Towards Verified Model Transformations.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.}
}