-
Notifications
You must be signed in to change notification settings - Fork 0
/
models2015-demo.tex
125 lines (102 loc) · 3.8 KB
/
models2015-demo.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
\documentclass[conference]{IEEEtran}
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{epstopdf}
\usepackage{verbatim} %long comments with the comment environment
\usepackage{AMMALanguages}
\usepackage[table]{xcolor}
\usepackage{tabularx}
\usepackage{booktabs}
\usepackage{cleveref}
\usepackage{url}
\usepackage{enumitem}
\input{commentSupport}
\newcommand{\chunk}[2]{%
\fcolorbox{black}{yellow}{\bfseries\sffamily\scriptsize#1}%
{$\blacktriangleright$#2$\blacktriangleleft$}%
}
\newcommand{\bentley}[1]{\chunk{Bentley}{\textbf{\textcolor{green}{\textsl{#1}}}}}
\newcommand{\levi}[1]{\chunk{Levi}{\textbf{\textcolor{red}{\textsl{#1}}}}}
\newcommand{\cgg}[1]{\chunk{Cl\'audio}{\textbf{\textcolor{blue}{\textsl{#1}}}}}
\newcommand{\javi}[1]{\chunk{Javi}{\textbf{\textcolor{brown}{\textsl{#1}}}}}
\begin{document}
\title{SyVOLT: Full Model Transformation\\Verification Using Contracts}
%\title{Full Verification of Model Transformation Contracts for Declarative ATL}
\author{Levi L\'{u}cio, Bentley James Oakes, Cl\'{a}udio Gomes, Gehan Selim,
Juergen Dingel and Hans Vangheluwe}
\author{\IEEEauthorblockN{Levi L\'{u}cio\IEEEauthorrefmark{1},
Bentley James Oakes\IEEEauthorrefmark{1},
Cl\'{a}udio Gomes\IEEEauthorrefmark{2},\\
Gehan Selim\IEEEauthorrefmark{3},
Juergen Dingel\IEEEauthorrefmark{3},
James R. Cordy\IEEEauthorrefmark{3} and
Hans Vangheluwe$^{\dagger,*}$}
\IEEEauthorblockA{\IEEEauthorrefmark{1}School of Computer Science,
McGill University,
Canada\\ [email protected], [email protected]}
\IEEEauthorblockA{\IEEEauthorrefmark{2}MSDL Lab,
University of Antwerp,
Belgium\\ [email protected], [email protected]}
\IEEEauthorblockA{\IEEEauthorrefmark{3}School of Computing,
Queen's University,
Canada\\ \{gehan, cordy, dingel\}@cs.queensu.ca}
}
\date{\today}
\maketitle
%\tableofcontents
\begin{abstract}
We introduce SyVOLT, a plugin for the Eclipse development environment for the
verification of structural pre-/post-condition contracts on model
transformations. The plugin allows the user to build transformations in our
transformation language DSLTrans using a visual editor. The pre-/post-condition contracts to be proved on the transformation can also be built in a similar
interface. Our contract proving process is exhaustive, meaning that if a
contract is said to hold, then the contract will hold for all input models of a
transformation. If the contract does not hold, then the counter-examples (i.e., input models) where the contract fails will be presented.
Demo: \url{https://www.youtube.com/watch?v=8PrR5RhPptY}
\end{abstract}
\section{Introduction}
\label{sec:intro}
\input{text/introduction}
\section{Highlights}
\label{sec:highlights}
\input{text/highlights}
\section{Architecture}
\label{sec:arch}
\input{text/arch}
%
%\section{Mapping ATL into DSLTrans}
%\label{sec:mapping}
%\input{text/mapping}
%
%% \section{Transformation to DSLTrans}
%% \label{sec:transformation}
%% \input{text/hot}
%
%%\section{Properties and Property Prover}
%%\label{sec:prover}
%%\input{text/prover}
%
%\section{Results and Discussion}
%\label{sec:results}
%\input{text/results}
%
%
%\section{Related Work}
%\label{sec:related}
%\input{text/related}
%
%\section{Summary}
%\label{sec:conclusion}
%\input{text/conclusion}\vspace{-.5cm}
% \section*{Acknowledgements}
% The authors warmly thank Gehan Selim for her work on the
% implementation of the contract prover. Bentley Oakes and Levi L\'ucio are
% researchers working for the NECSIS project, funded by the Automotive Partnership
% Canada. %The work of Javier Troya and Manuel Wimmer is funded by the European
% %Commission under ICT Policy Support Programme, grant no. 317859.
\bibliographystyle{abbrv}
\bibliography{models2015}
\end{document}