Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification

Bertrand Boisvert, Louis Féraud, Sergei Soloviev

2013

Abstract

This paper deals with model transformations based on attributed graphs transformation. Our approach is based on the categorical approach called Single Pushout. The principal goal being to strengthen the attribute computation part, we generalize our earlier approach based on the use of typed lambda-terms with inductive types and recursion to represent attributes and computation functions. The generalized approach takes terms in variable context as attributes and partial proofs as computation functions that permit to combine computation with proof development and verification. The intended domains of application are the development of cerified software models and semantics models for interactive proof development and verification.

Download


Paper Citation


in Harvard Style

Boisvert B., Féraud L. and Soloviev S. (2013). Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification . In Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-8565-42-6, pages 62-74. DOI: 10.5220/0004321200620074

in Bibtex Style

@conference{modelsward13,
author={Bertrand Boisvert and Louis Féraud and Sergei Soloviev},
title={Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification},
booktitle={Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2013},
pages={62-74},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004321200620074},
isbn={978-989-8565-42-6},
}


in EndNote Style

TY - CONF
JO - Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification
SN - 978-989-8565-42-6
AU - Boisvert B.
AU - Féraud L.
AU - Soloviev S.
PY - 2013
SP - 62
EP - 74
DO - 10.5220/0004321200620074