%% LyX 1.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[10pt,english]{article}
\usepackage{ae}
\usepackage{aecompl}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{geometry}
\geometry{verbose,letterpaper,tmargin=1cm,bmargin=1cm,lmargin=1cm,rmargin=1cm,headheight=1cm,headsep=1cm,footskip=1cm}
\setlength\parskip{\smallskipamount}
\setlength\parindent{0pt}

\makeatletter
\usepackage{babel}
\makeatother
\begin{document}

\title{Internship report outline\\
(intended to the ENS staff)}


\author{Tahina Ramananandro\\
Daniel Jackson}

\maketitle

\section{Introduction}


\subsection{The VSR Project}

Verified Software Repository, a level 6 Grand Challenge.

The VSR/NET workshops in England, with Jim Woodcock.

To share the same case study with many different methods. To seek
proofs as automatically as possible. List of candidates. Why Coq,
for instance, would not have suited.


\subsection{The Mondex Case Study}

The Mondex electronic purses. Abstract and Concrete protocols.

Introducing the Z specification language, in which the Mondex has
been modeled and proved by hand.


\section{The Alloy method}


\subsection{The Alloy specification language}

Signature, relations, ... A short example of an Alloy model.


\subsection{The Alloy Analyzer}

Principles of model-finding. Finite scope. (Some screenshots.)

It interacts with the specification process to find bugs in the constraints.


\section{The Mondex spec in Alloy}


\subsection{Constraints}

Global and local constraints. Global constraints may make me miss
some cases.

Many differences with Z, though. Some imprecisions with specifying
in Z (operations and constraints).


\subsection{Atom identification and canonicalization}

Distinguishing identified (purses) and unidentified (PayDetails) objects.

Unidentified objects have to be canonicalized.

Notion does not exist in Z.


\subsection{Existential theorems and model finding}

With a model finder, an existential theorem is generally false (empty
instance). Enforcing objects to exist increase the scope, and so the
search space.

So, consider defining objects through their properties.

But this requires to be very careful about global constraints, which
could make those objects actually not exist.


\subsection{Results}

The use of the Alloy Analyzer implementation raised technical issues
which led to modifying the specification : why not use integers ?

Bugs found in the original specification.

Time of SAT-Solving.

How could it be improved with Kodkod (currently under development,
but using the same method) ?


\subsection{Limits to the method}

The finite scope : results are valid only for a given scope. The higher,
the longer time and the more resources.

So, finiteness properties ignored.


\section{Extended analysis : Alloy and theorem proving}


\subsection{Translating Alloy to FOL.}

Alloy semantics in FOL. Problem : transitive closures.


\subsection{Results (in progress)}

Which theorems have been proved from the existing specification ?
How long time ?


\subsection{Limits to the method}

Undecidable in general (existentials).

Transitive closures. Fortunately, the Mondex spec has none of them. 

In general, does not solve how to tackle finiteness. In the Mondex
spec in Z, there are some required properties. Dropped again.

Using proof assistants could help (cf. Prioni), but we lose automation.
(Some failed example with Coq)


\section{Conclusion and future work}

In particular we would have shown that the Mondex specification can
be fitted into FOL if finiteness properties are dropped.

The Alloy language has a high potential of use ; though, I would say
Daniel's group should give a hand for other groups to use the Alloy
spec language with other methods than model-finding. But on the contrary,
I fear from the fact that the current evolution of Alloy, with scripting
features, would enforce the use of the next Alloy/Kodkod model-finding
analyzer.

For the Mondex case study in particular : I'll technically present
my work on October 5-6th, and they'll decide how to use it. Probably
to interact Alloy with other methods.

Even though obviously the general model-finding method is not enough
to prove specifications, it allows to quickly and easily find bugs
in them. So it is an interesting method for the preliminary treatment
of a spec.
\end{document}