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-Saclay
Laboratory : LRI Fortesse

Defended on 12/12/2012, committee :

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.

CAUSAL LEARNING FOR DIAGNOSTIC SUPPORT


CAUSAL UNCERTAINTY QUANTIFICATION UNDER PARTIAL KNOWLEDGE AND LOW DATA REGIMES


MICRO VISUALIZATIONS: DESIGN AND ANALYSIS OF VISUALIZATIONS FOR SMALL DISPLAY SPACES
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.