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

Ph.D
Group : Formal Testing and System Exploration

Semantics-Based Testing for Circus

Starts on 01/10/2009
Advisor : GAUDEL, Marie-Claude

Funding : A
Affiliation : Université Paris-Sud
Laboratory : LRI Fortesse

Defended on 12/12/2012, committee :
Rapporteurs:

- Rob Hierons, Professor of Computing, Brunel University, UK
- Stephan Merz, directeur de recherche INRIA Nancy, LORIA

Examinateurs:

- Pascale Le Gall, Professeur Université d'Evry-Val d'Essonne, LMAS
- Claude Marché, directeur de recherche INRIA saclay

Directeurs de thèse:

- Marie-Claude Gaudel, professeur émérite Paris Sud, LRI
- Burkhart Wolff, professeur Paris Sud, LRI

Invités:

- Ana Cavalcanti, Reader, University of York, UK

=

Research activities :

Abstract :
The work presented in this thesis is a contribution to formal specification and verification methods.
Formal specifications are used to describe a software, or more generally a system, in a mathematical unambiguous way.
Formal verification techniques are defined on the basis of these specifications to ensure the correctness of the resulting system.
However, formal methods are often not convenient and easy to use in real system developments.
One of the reasons is that many specification formalisms are not rich enough to cover both data-oriented and behavioral requirements.
Some specification languages were proposed to cover this kind of requirements.
The Circus language distinguishes itself among these languages by a rich syntax and a fully integrated semantics.

The aim of this thesis is to provide a formal environment for specifying and verifying complex systems.
Specifications are written in Circus and verification is performed either by testing or by theorem proving.
Similar specifications and verification environment have already been proposed.
A specificity of our approach is to combine supports for proofs and test generation.
Moreover, most test generation methods are based on a syntactic characterization of the studied languages.
Our proposed environment is different since it is based on the denotational and operational semantics of Circus.
The Isabelle/HOL theorem prover is the formal platform on top of which we built our specification and verification environment.

The first main contribution of our work is the Isabelle/Circus specification and proof environment based on the denotational semantics of Circus.
On top of Isabelle/HOL we provide a machine-checked shallow embedding of UTP, the semantics basis of Circus .
This embedding is used to formalize the denotational semantics of the Circus language.
The Isabelle/Circus environment associates to this semantics some parsing facilities that help writing Circus specifications.
The proof support of Isabelle/HOL can be used directly to reason on these specifications thanks to the shallow embedding of the semantics.
We present an application of the environment to refinement proofs on Circus processes (involving both data and behavioral aspects).

The second main contribution is the CirTA testing framework build on top of Isabelle/Circus.
The framework provides two symbolic test generation tactics that allow checking two notions of refinement: traces inclusion and deadlocks reduction.
The framework is based on a shallow symbolic formalization of the operational semantics of Circus using Isabelle/Circus.
Several symbolic definition and test generation tactics are defined in the CirTA framework.
The formal infrastructure allows us to represent explicitly test theories as well as test selection hypothesis.
Proof techniques and symbolic computations are the basis of test generation tactics.

The test generation environment was used for a case study to test an existing message monitoring system.
A specification of the system is written in Circus , and used to generate tests following the defined conformance relations.
The tests are then compiled in forms of JUnit test methods and executed against a Java implementation of the monitoring system.

This thesis is a step towards, on one hand, the development of sophisticated testing tools making use of proof techniques and,on the other hand, the integration of testing and proving within formally verified software developments.

Ph.D. dissertations & Faculty habilitations
DECODING THE PLATFORM SOCIETY: ORGANIZATIONS, MARKETS AND NETWORKS IN THE DIGITAL ECONOMY
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.

DISTRIBUTED COMPUTING WITH LIMITED RESOURCES


VALORISATION DES DONNéES POUR LA RECHERCHE D'EMPLO