Sites Inria

Version française

Inria-Industry Meetings

The aeronautical and space industries - Part 2: Speakers

This event featured presentations from several specialists from the field of aeronautics and space. They gave an overview of the research carried out by Inria and its partners into this type of activity.

Roberto di Cosmo: free/open-source software: scientific and technological challenges for complex engineering systems

Roberto Di Cosmo

Quick bio:  Roberto Di Cosmo is a professor of computer science at Paris Diderot University, where he works on the formal aspects of free software, notably as part of the European project Mancoosi, which he coordinates; he was the founder and first chairman of the Free Software Thematic Group at the Systematic competitiveness cluster; on secondment at Inria since September 2009, he is working on the creation of a research and innovation centre in Computer Science in Free Software.

Presentation summary:  The boom in free software is irrepressible and brings with it new scientific problems that need to be rapidly resolved using the results of fundamental research. This presentation features two success stories from this field: the Coccinelle project and the Mancoosi project. We will also address issues linked with the impact that free software has on the training of computer science engineers and on industrial business models.

Keywords:  free software, complex systems, engineering, software engineering, verification, formal methods.

Robert de Simone: models and code at the same time: the benefits and requirements of multiform logical time in the design of critical real-time embedded systems

Robert de Simone

Quick bio: Robert de Simone is a Senior Research Scientist at Inria and leader of the Aoste project-team. His main centres of interest cover the Semantics of Parallelism (process algebra, reactive synchronous languages, automatic verification and model checking), the formal approach to the design of embedded systems by Model Engineering and static scheduling in Process Networks. He has coordinated numerous collaborative projects on these topics for Inria, some of which resulted in the OMG official UML profile MARTE for the modelling and analysis of real-time and embedded systems.

Presentation summary:  The current design cycle for critical real-time embedded systems is increasingly dependent on the engineering of models. These frequently involve parallelism and concurrency both in terms of applications and execution architectures, and design teams and their cooperation. These models can be executable to enable their analysis by simulation and can also be formal in order to allow for more mathematical analysis. They are rarely both at the same time. We will illustrate how an approach based on multiform time and logical clocks aims to reconcile these two qualities (executable, formal) and spread them throughout the design cycle.

Keywords:  embedded system, critical system, real-time, scheduling, model engineering, multiform logical time, clock computation.

Xavier Leroy: an introduction to the formal verification of critical codes

Xavier Leroy

Quick bio:  Xavier Leroy is a Senior Research Scientist at Inria and leader of the Inria project-team Gallium. He is one of the main authors of the functional programming language OCaml. He has also worked on software security, including smartcard applications. His current work relates to the formal verification of compilers and other program verification and transformation tools.

Presentation summary:  What do you do when a test is insufficient (or becomes too costly) for qualifying a critical software program? One solution is formal verification, assisted by tools and the codes in question - a practice that is starting to break through in the aeronautical industry. To illustrate this approach, I will give a quick introduction of a few verification tools, based on the static analysis or deductive verification of programs and their uses in aeronautics. I will then address the issue of compilers and other automatic code generators: their formal verification enables the guarantees obtained by verification of the source program to be extended to the executable code.

Marc Pouzet: the large-scale action Inria SYCHRONICS, "Synchronous programming languages for embedded systems"

Marc Pouzet

Quick bio:  Marc Pouzet is a Professor of Computer Science at France's École Normale Supérieure. Together with Alain Girault, he coordinates the large-scale action Inria Synchronics. His research activity involves the design and implementation of programming languages for embedded systems. Several of his accomplishments have been integrated into the industrial environment SCADE 6, developed by the company Esterel-Technologies.

Presentation summary:  The presentation will provide an update on the developments carried out as part of the Inria large-scale action. It will provide details on current work carried out in connection with ReactiveML, which combines the principles of functional programming in OCaml and reactive programming in Esterel.