Browsing by Author "Tasistro, Álvaro"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    A type-theoretic framework for certified model transformations
    (Universidad ORT Uruguay. Facultad de Ingeniería, 2010) Calegari, Daniel; Luna, Carlos; Szasz, Nora; Tasistro, Álvaro
    "We present a framework based on the Calculus of Inductive Constructions (CIC) and its associated tool the Coq proof assistant to allow certification of model transformations in the context of Model-Driven Engineering (MDE). The approached is based on a semi-automatic translation process from metamodels, models and transformations of the MDE technical space into types, propositions and functions of the CIC technical space. We describe this translation and illustrate its use in a standard case study." [Abstract]
  • Thumbnail Image
    Item
    Experiment with a type-theoretic approach to the verification of model transformations
    (Universidad ORT Uruguay. Facultad de Ingeniería, 2009) Calegari, Daniel; Luna, Carlos; Szasz, Nora; Tasistro, Álvaro
    "This paper presents ongoing work on the application of constructive type theory for safe development in Model-Driven Engineering. In particular, we put into practice a certification framework based on the Calculus of Inductive Constructions (CIC) as follows: we first describe methods for representing metamodels and specifications of model transformations as types and then outline principles for representing given transformations, written in a certain transformation language, as functions in CIC. Then properties of these functions are proven, including their correctness with respect to sufficiently expressive specifications, thereby providing a semiformal way to verify the original transformations. We carry out a concrete case taken from an on-line base of basic examples and patterns of use of the ATL transformation language, implementing it on machine using the Coq proof assistant." [Abstract]