Sites Inria

Version française

Inria-Industry Meetings

The aeronautical and space industries - Part 2: Demos

GOLAEM

This event on May 17 featured demonstrations of technologies created by Inria and its industrial partners.

Astrée: Proof of Absence of Run-Time Errors

Project-team: ABSTRACTION

Joint project-team with the Ecole Normale Supérieure de Paris and the French National Centre for Scientific Research

Summary: Astrée is a static analyser for the proof of absence of run-time errors in critical embedded C programs. This proof is entirely automatic and carried out at the level of the source code, in terms of the language semantics. Astrée has successfully analysed industrial-scale applications in the field of aeronautics and space. The Astrée analyser was designed and developed by the Abstraction team. It is currently marketed by the company Absint Angewandte Informatik.

Keywords: static analysis, verification, qualification, safety, critical embedded systems

The SynDEx tool for the optimised distributed implantation under real-time constraints of critical embedded applications

Project-team: AOSTE

Joint project-team with the I3S laboratory (University of Nice Sophia Antipolis and French National Centre for Scientific Research)

Summary:  Critical embedded applications are usually modelled and simulated with tools that use block diagrams. The presentation will feature the SynDEx tool, which reads these types of application models, specifies constraints and temporal characteristics, specifies heterogeneous distributed material architectures, and then, after automatically carrying out a real-time schedulability and optimisation analysis, generates the correct code per construction for these embedded architectures. It will also feature a gateway between the Scicos modelling and simulation tool for control-command systems and the SynDEx tool.

Keywords: Schedulability, distributed, real time, embedded, implantation

TimeSquare: Functional Specifications based on Logical Time in Model Engineering

Project-team:  AOSTE

Joint project-team with the I3S laboratory (University of Nice Sophia Antipolis and French National Centre for Scientific Research)

Summary: TimeSquare is based on the CCSL formalism (Clock Constraint Specification Language), which is part of the OMG UML MARTE profile (modelling and analysis of real-time and embedded systems). The tool enables users to specify logical clocks and to associate these with behavioural activations and rhythms within an embedded system (for example, modelled in UML or SysML). TimeSquare enables the analysis and unification of logical clocks and their heterogeneous times, with the aim of placing/scheduling applications in runtime platforms.

Keywords: embedded systems, UML/SysML, logical clocks, polychronous languages, constraint-based scheduling

A sustainable development process: the ATL experiment

Project-team: ATLANMOD

Joint project-team with the Ecole des Mines de Nantes.

Industrial partner:  Obeo

Summary:  Model-Directed Engineering consists of defining software elements using precise models. The conversion of models then enables their operation to be automated. This is used in particular for software development, reverse engineering and as an element of the software system (runtime models). The AtlanMod team works in collaboration with Obeo on ATL: a model conversion tool.

Keywords:  model conversion

Architecture exploration in the field of aeronautics and space by synchronous technology

Project-team:  ESPRESSO

Joint project-team with the French National Centre for Scientific Research, the National Institute of Applied Sciences in Rennes and the University of Rennes 1

Industrial partner: Geensoft

Summary:  Application for the management of power distribution modes in an orbiting satellite, with optimisation of its load in survival mode. Evaluation of the performance of distributed embedded systems via synchronous technology.

Keywords: synchronous, SIGNAL, RT-Builder, polychrony, real time

3D object content-based searches

Project-team:  IMEDIA

Summary: Recent 3D digitisation and modelling technologies allow the creation of large 3D model databases. These models are widely used in fields such as CAD, computer graphics and audiovisual production. Content-based searching is a necessary solution for structuring and managing these multimedia data and for navigating in these databases. In this context, our system allows users to automatically find 3D models that are visually similar to a requested 3D object.

Keywords: 3D object content-based searches, 3D indexing

Tom: a Java extension for more easily converting tree structures and models

Project-team:  PAREO

A team from the Lorraine Laboratory of Computer Science Research and Applications, jointly run with the French National Centre for Scientific Research, the Henri Poincaré and Nancy 2 universities and the National Polytechnic Institute of Lorraine

Summary: Tom is a programming language that allows users to extend other languages, particularly Java, to integrate filtering constructions such as "match" (a construction also present in the Caml language for example). "Filtering" is a task consisting of searching for motifs in a data item. Tom lets users easily manipulate tree structures, making it a suitable tool for model conversion. It is currently being used in the QUARTEFT project financed by the FRAE. Also involved are the Laboratory for the Analysis and Architecture of Systems, the Toulouse Institute for Computer Science Research, the National Office of Aerospace Studies and Research, Airbus and Ellydis. Our long-term objective is to offer certified model conversion tools.

Keywords: Java, conversions, models, trees, certification

Frama-C, a toolbox for verifying software in C

Project-team: PROVAL

Joint project-team with Paris-Sud 11 University and the French National Centre for Scientific Research (Computer Science Research Laboratory)

Industrial partner: Adacore. Summary: Frama-C brings together numerous static analysis techniques, the verification of coding rules in analysis by abstract interpretation and the verification of functional specifications using the principles of the deductive approach of program verification. The targeted fields are critical embedded software, cryptographic library implementations and security.

Keywords: static analysis, verification, Hoare logic, abstract interpretation

Alt-Ergo, automatic proving for critical code certification

Project-team: PROVAL

Joint project-team with Paris-Sud 11 University and the French National Centre for Scientific Research (Computer Science Research Laboratory)

Summary:  Alt-Ergo is a software program for automatic theorem proving. It is dedicated to the deductive proving of programs, which reduces the correction of a program in terms of its specification to the validity of a logical formula. In one major use, Alt-ergo is situated at the end of the chain in proving platforms used in avionics. Depending on the complexity of the codes analysed, thousands of formulae may need to be proved. Because it is not conceivable to manually conduct all of these proofs, the use of a tool such as Alt-Ergo is crucial for the scaling-up of this approach.

Keywords:  automatic proving, program proving

Operation planning optimisation

Project-team:  REALOPT

Joint project-team with University of Bordeaux 1, University of Bordeaux 2, the ENSEIRB and the French National Centre for Scientific Research.

Industrial partners: Exeo and Eurodecision

Summary:  We take a look at the issues of planning and production, the combined optimisation of delivery routes linked with inventory management, waste collection optimisation, the construction of flight and crew rotation programmes, and design optimisation. Our Inria team, RealOpt, and our industrial partners, Synoptis eXEO Solutions and Eurodecision, are developing resolution methods and software for these types of applications. The demonstration includes a presentation of the Synoptis software package (from eXEO Solutions) and OptiFleet (from Eurodecision).

Keywords:  combinative optimisation, logistics, planning, design, rotation

Verification of temporal constraints in critical embedded systems

Project-team:  TRIO

A team from the Lorraine Laboratory of Computer Science Research and Applications, jointly run with the French National Centre for Scientific Research, the Henri Poincaré and Nancy 2 universities, the National Polytechnic Institute of Lorraine and the Ecole Normale Superieure de Lyon.

Industrial partner:  Rtaw

Summary:  Certain critical embedded systems in avionics and automotives are currently made up of dozens of computers that run the software. These have major real-time constraints and exchange thousands of data flows. We present an analysis and simulation software suite that provides guarantees on the temporal behaviour of embedded systems and optimises their hardware dimensioning.

Keywords:  embedded system, safety engineering, temporal guarantees, scheduling, certification

Model Driven Language Engineering using Kermeta

Inria project-team: TRISKELL

Joint project-team with the French National Centre for Scientific Research, the National Institute of Applied Sciences in Rennes and the University of Rennes 1

Summary:  In many fields such as the aerospace and automotive industries, engineers rely on Domain Specific Modeling Languages to solve the complex issues of engineering safety critical software. This tutorial aims to show how Model Driven Engineering can help to easily obtain a complete environment for such a language, including interpreter, compiler, V&V tools, pretty-printer and customisable editors. We illustrate the conceptual simplicity and elegance of this approach using the running example of the well known LOGO programming language, developed within the Kermeta environment.

Keywords:  model-based development, domain specific language, model driven engineering, executable modelling, V&V

Verification of critical embedded systems with CADP 2009

Project-team:  VASY

Summary:  The development of critical embedded systems requires tools that can ensure the reliability of these systems right from the initial phases of their design. The CADP software toolbox enables the modelling and formal verification of these systems. We illustrate the use of CADP in several avionics case studies.

Keywords: Reliability, formal methods, model checking, validation

Java Multitouch/Webserver/HRTJ application on low-cost targets

Company:  IS2T

Summary: Multi-touch capabilities on ARM7-LPC2478 at 67Mhz; Managing sensors on a board from a web server embedded on AVR32 EVK1100; Implementing the principles of HRT on a Java Virtual Machine on ARM9

Keywords:  multi-touch, Java, HRTJ, DO178C, Web server

Top