Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

Group : Verification of Algorithms, Languages and Systems

Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages

Starts on 01/02/2013
Advisor : WOLFF, Burkhart
[Delphine LONGUET]

Funding : Autre financement à préciser
Affiliation : Université Paris-Saclay
Laboratory : LRI

Defended on 06/04/2016, committee :
Directeur de thèse :
M. Burkhart WOLFF

Examinateurs :
M. Stéphane MAAG
M. Safouan TAHA

Rapporteurs :
Mme Catherine DUBOIS
M. Bernhard RUMPE

Research activities :
   - Formalisation of (Specification and Programming) Languages in Proof Assistants
   - Formal Model-Based Testing

Abstract :
Object-based and object-oriented specification languages (like
UML/OCL, JML, Spec#, or Eiffel) allow for the
creation and destruction, casting and test for dynamic types of
statically typed objects. On this basis, class invariants and
operation contracts can be expressed; the latter represent the key
elements of object-oriented specifications. A formal semantics of
object-oriented data structures is complex: imprecise descriptions can
often imply different interpretations in resulting tools.

In this thesis we demonstrate how to turn a modern proof environment
into a emph{meta-tool} for definition and analysis of formal
semantics of object-oriented specification languages. Given a
representation of a particular language embedded in Isabelle/HOL, we
build for this language an extended Isabelle environment by using a
particular emph{method} of code generation, which actually involves
several variants of code generation. The result supports the
asynchronous editing, type-checking, and formal deduction activities,
all ``inherited'' from Isabelle.

Following this method, we obtain an emph{object-oriented modelling
tool} for textual UML/OCL. We also integrate certain idioms not
necessarily present in UML/OCL --- in other words, we develop
support for domain-specific dialects of UML/OCL.

As a meta construction, we define a meta-model of a part of UML/OCL
in HOL, a meta-model of a part of the Isabelle API in HOL, and a
translation function between both in HOL. The meta-tool will then
exploit two kinds of code generation to produce either emph{fairly
efficient code}, or emph{fairly readable code}. Thus, this provides
two animation modes to inspect in more detail the semantics of a
language being embedded: by loading at a native speed its semantics,
or just delay at another ``meta''-level the previous experimentation
for another type-checking time in Isabelle, be it for performance,
testing or prototyping reasons.

Note that generating ``fairly efficient code'', and ``fairly readable
code'' include the generation of emph{tactic code} that proves a
collection of theorems forming an object-oriented datatype theory from
a denotational model: given a UML/OCL class model, the proof of the
relevant properties for casts, type-tests, constructors and selectors
are automatically processed. This functionality is similar to the
emph{datatype theory packages} in other provers of the HOL family,
except that some motivations have conducted the present work to
program high-level tactics in HOL itself.

This work takes into account the most recent developments of the
UML/OCL 2.5 standard. Therefore, all UML/OCL types including the
logic types distinguish two different exception elements:
inlineocl{invalid} (exception) and inlineocl{null} (non-existing
element). This has far-reaching consequences on both the logical and
algebraic properties of object-oriented data structures resulting from
class models.

Since our construction is reduced to a sequence of conservative theory
extensions, the approach can guarantee logical soundness for the
entire considered language, and provides a methodology to soundly
extend domain-specific languages.

Ph.D. dissertations & Faculty habilitations
The topic of this habilitation is the study of very small data visualizations, micro visualizations, in display contexts that can only dedicate minimal rendering space for data representations. For several years, together with my collaborators, I have been studying human perception, interaction, and analysis with micro visualizations in multiple contexts. In this document I bring together three of my research streams related to micro visualizations: data glyphs, where my joint research focused on studying the perception of small-multiple micro visualizations, word-scale visualizations, where my joint research focused on small visualizations embedded in text-documents, and small mobile data visualizations for smartwatches or fitness trackers. I consider these types of small visualizations together under the umbrella term ``micro visualizations.'' Micro visualizations are useful in multiple visualization contexts and I have been working towards a better understanding of the complexities involved in designing and using micro visualizations. Here, I define the term micro visualization, summarize my own and other past research and design guidelines and outline several design spaces for different types of micro visualizations based on some of the work I was involved in since my PhD.