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

Ph.D
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-Sud
Laboratory : LRI

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

Examinateurs :
M. Achim D. BRUCKER
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
APPRENTISSAGE ET OPTIMISATION SUR LES GRAPHES


ANALYSE DE DONNéES MULTI-MODALES POUR LES PATHOLOGIES COMPLEXES PAR LA CONCEPTION ET L’IMPLéMENTATION DE PROTOCOLES REPRODUCTIBLES ET RéUTILISABLES


DESIGNING INTERACTIVE TOOLS FOR CREATORS AND CREATIVE WORK
Creative work has been at the core of research in Human-Computer Interaction (HCI). I describe the results of a series of studies that look at how creators work, where creators include artists with years of professional practice, as well as learners, or novices and casual makers. My research focuses on three creation activities: drawing, physical modeling, and music composition. For these activities, I examine how artists switch between representations and how these representations evolve throughout their creative process, from early sketches to fine-grained forms or structured vocabularies. I present interactive systems that enrich their workflow (i) by extending their computer tools with physical user interfaces, or (ii) by making physical materials interactive. I also argue that sketch-based representations can allow for user interfaces that are more personal and less rigid. My presentation will reflect on lessons and limitations of this work and discuss challenges for future design-support tools.