Journée de conférences

• Pr Ladjel Bellatreche – LIAS/ISAE-ENSMA
  

Design and Exploitation of Smart Data-Enabled Systems/Applications

L’objectif de ce séminaire est de présenter les enjeux et les solutions pour concevoir et exploiter des systèmes/applications intelligents basés sur les données. Pour mieux comprendre la situation actuelle autour des systèmes de données, une présentation historique sera largement discutée et commentée. Des pistes de recherche ainsi que des outils développés dans l’équipe Ingénierie des Données et des Modèles du Laboratoire d’Informatique et d’Automatique pour les Systèmes (LIAS) seront exposés.

• Pr Dominique Méry – Université de Lorraine, LORIA UMR CNRS 7503
  

Verification by Construction of Distributed Algorithms

The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof assistants. The difficulties, even for powerful tools, lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algo- rithms. Verification by construction can be achieved by using a formal framework in which models are constructed at different levels of abstrac- tion; each level of abstraction is refined by the one below, and this re- finement relationships is documented by an abstraction relation namely a gluing invariant. The highest levels of abstraction are used to express the required behavior in terms of the problem domain and the lowest level of abstraction corresponds to an implementation from which an efficient implementation can be derived automatically. In this paper, we describe a methodology based on the general concept of refinement and used for developing distributed algorithms satisfying a given list of safety and live- ness properties. The modelling methodology is defined in the Event-B modelling language using the IDE Rodin.

• Pr André-Luc BEYLOT – IRIT-ENSEEIHT . Toulouse
  

Acrux : Localisation en intérieur à l’aide des capteurs d’un smartphone »

Les systèmes de localisation constituent des éléments incontournables dans notre vie quotidienne. En extérieur, les solutions GPS donnent des résultats satisfaisants depuis longtemps. En revanche, elles ne fonctionnent pas à l’intérieur des bâtiments. Ce problème a donné lieu à des solutions nombreuses et compliquées souvent liées à une infrastructure lourde. Les smartphones sont désormais équipés de très nombreux capteurs et l’originalité de notre solution va consister à permettre à l’utilisateur de se localiser avec les seules informations collectées par ces capteurs de mouvement, qui constituent une centrale inertielle. Nous contournons leur imprécision en étudiant la locomotion humaine et son effet sur les signaux des capteurs. Une campagne de tests a permis de montrer que nous obtenons une précision de l’ordre du mètre.

• Pr Yamine AIT AMEUR – IRIT-ENSEEIHT Toulouse

Modelling ontologies as theories in formal system development

Critical systems are running in heterogeneous domains. This heterogeneity is rarely considered explicitly when describing and validating processes. Handling explicitly such domain knowledge increases design models robustness due to the expression and validation of new properties mined from the domain models. This talk discusses an approach to enrich design models describing complex information systems with domain knowledge. We use ontologies to model such domain knowledge. Design models are annotated by references to domain ontologies. The resulting annotated models are checked. It becomes possible to verify domain-related properties and obtain strengthened and/or enriched models. The approach is deployed for two design model development approaches a correct by construction formal modelling one based on refinement and proof using the Event-B method and the second one is based on state transition systems and weak bi-simulation. This talk presents first the notion of ontologies. Then it shows how formal models borrow ontology concepts in two cases.