*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*   ENS, Equipe-projet INRIA "Abstraction" commune avec ENS & CNRS  *
*                                                                   *
*                        Vendredi, 14h00--16h00                     *
*                  Salle S16, etage -1 /Ceylan/Amphi Galois         *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

***  Vendredi 08 Septembre 2010, 14h00-15h00, Salle Celan ***********

Analysis of aerospace domain models containing arithmetic computations.

Michael Dierkes, Rockwell Collins France

Re'sume'/ Abstract:

For several years, Rockwell Collins has been developing and using a 
verification framework for MATLAB Simulink and SCADE Suite models that can 
generate input for different proof engines. Recently, we have used this 
framework to analyze aerospace domain models containing arithmetic 
computations. In particular, we investigated the properties of a redundancy 
management unit that is implemented using linear arithmetic operations as well 
as conditional expressions (such as saturation) that increase the complexity 
of the state space. 

In order to deal with such systems, we intend to combine analysis results 
obtained by different proof techniques, and to apply compositional 
verification by verifying different subsystems separately. The objective of 
this analysis is to verify functional properties, but also to parameterize 
certain parts of the model based on the analysis of other parts. 

In this presentation, we describe our ongoing work and the improvements we 
would like to obtain in order to integrate formal verification into the 
production process. 

*********************************************************************
Pour recevoir l'annonce par courrier electronique:
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************