«

»

A formal framework to prove the correctness of model driven engineering composition operators

by Mounira Kezadri, Marc Pantel, Benoit Combemale, Xavier Thirioux
Abstract:
Current trends in system engineering combine modeling, composition and verification technologies in order to harness their ever growing complexity. Each composition operator dedicated to a different modeling concern should be proven to be property preserving at assembly time. These proofs are usually burdensome with repetitive aspects. Our work targets the factorisation of these aspects relying on primitive generic composition operators used to express more sophisticated language specific ones. These operators are defined for languages expressed with OMG MOF metamodeling technologies. The proof are done with the Coq proof assistant relying on the Coq4MDE framework defined previously. These basic operators, Union and Substitution, are illustrated using the MOF Package Merge as composition operator and the preservation of model conformance as verified property.
Reference:
A formal framework to prove the correctness of model driven engineering composition operators (Mounira Kezadri, Marc Pantel, Benoit Combemale, Xavier Thirioux), In 16th International Conference on Formal Engineering Methods (ICFEM 2014), Springer, 2014.
Bibtex Entry:
@inproceedings{kezadri:hal-01024067,
	Abstract = {{Current trends in system engineering combine modeling, composition and verification technologies in order to harness their ever growing complexity. Each composition operator dedicated to a different modeling concern should be proven to be property preserving at assembly time. These proofs are usually burdensome with repetitive aspects. Our work targets the factorisation of these aspects relying on primitive generic composition operators used to express more sophisticated language specific ones. These operators are defined for languages expressed with OMG MOF metamodeling technologies. The proof are done with the Coq proof assistant relying on the Coq4MDE framework defined previously. These basic operators, Union and Substitution, are illustrated using the MOF Package Merge as composition operator and the preservation of model conformance as verified property.}},
	Address = {Luxembourg},
	Author = {Kezadri, Mounira and Pantel, Marc and Combemale, Benoit and Thirioux, Xavier},
	Booktitle = {{16th International Conference on Formal Engineering Methods (ICFEM 2014)}},
	Month = Nov,
	Pdf = {http://hal.inria.fr/hal-01024067/PDF/paper_84-camera.pdf},
	Publisher = {Springer},
	Title = {{A formal framework to prove the correctness of model driven engineering composition operators}},
	Url = {http://hal.inria.fr/hal-01024067},
	Year = {2014},
	Bdsk-Url-1 = {http://hal.inria.fr/hal-01024067}}