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-Sud
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 original manuscript conceptualizes the recent rise of digital platforms along three main dimensions: their nature of coordination devices fueled by data, the ensuing transformations of labor, and the accompanying promises of societal innovation. The overall ambition is to unpack the coordination role of the platform and where it stands in the horizon of the classical firm – market duality. It is also to precisely understand how it uses data to do so, where it drives labor, and how it accommodates socially innovative projects. I extend this analysis to show continuity between today’s society dominated by platforms and the “organizational society”, claiming that platforms are organized structures that distribute resources, produce asymmetries of wealth and power, and push social innovation to the periphery of the system. I discuss the policy implications of these tendencies and propose avenues for follow-up research.