with the support of AESE

The TOPCASED project aims at developing an open source CASE environment for critical applications and systems development. Its main benefits should be to perpetuate the methods and tools for software development, minimize ownership costs, ensure independence of development platform, integrate, as soon as possible, methodological changes and advances made in academic world, be able to adapt tools to the process instead of the opposite, take into account qualification constraints.

One key point is that TOPCASED focuses on critical system development, which means that a strong emphasis is made on system validation and on traceability.

Topcased was followed by the OpenEmbeDD project (Model Driven Engineering open-source platform for Real-Time and Embedded systems), is an initiative for an open-source embedded system design toolchain based on Eclipse (funded by RNTL, from 2006 to 2009). Today, development are part of the PolarSys Eclipse WP.

CNRS Researcher

My research interests include formal methods and concurrency semantics.


An Experiment on Parallel Model Checking of a CTL Fragment

We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, …

Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction

We propose an algorithm for parallel state space construction based on an original concurrent data structure, called a …

A General Lock-Free Algorithm for Parallel State Space Construction

Verification via model-checking is a very demanding activity in terms of computational resources. While there are still gains to …

Formal Verification of AADL models with Fiacre and Tina

This paper details works undertaken in the scope of the Spices project concerning the behavioral verification of AADL models. We …

Enumerative Parallel and Distributed State Space Construction

Model Checking requires high end computers to verify complex systems. Consequently, it is interesting to use a multi-processors …

Formal Verification of AADL Specifications in the Topcased Environment

We describe a formal verification toolchain for AADL, the SAE Architecture Analysis and Design Language, enriched with its …

Observation Graph implementation for TINA toolbox

Model Checking is a formal technique for the verification of finite systems. However, it is well known that this technique …