Nous présenterons la problématique de la modélisation des systèmes à logiciel dominant d'un point de vue architectural. Plusieurs points seront abordés : quelle est la sémantique d'un système ? Quels sont les opérateurs qui agissent sur les systèmes ? Comment représenter les systèmes sous forme de vues architecturales ? Des illustrations de ces concepts sur quelques cas d'application seront présentés.
Hi-Lite is a project aiming at popularizing formal methods for the development of high-integrity software. It targets ease of adoption through a loose integration of formal proofs with testing and static analysis, that allows combining techniques around a common expression of specifications. Its technical focus is on modularity, that allows a divide-and-conquer approach to large software systems, as well as an early adoption by all programmers in the system life cycle. Hi-Lite is completely based on libre software. The project is structured in two different toolchains for Ada and C based on GNAT/GCC compilers, the SPARK verification toolset and the Frama-C platform. The integration of these toolchains inside two industrial IDEs will offer to the user a common interaction on Ada and C programs. In particular, mixed Ada/C programs will be verified against a common specification. The project partners are AdaCore, Altran (in particular its Praxis entity), Astrium, CEA-List, the ProVal team of INRIA and Thales. AdaCore is the project leader. The project is scheduled to start mid 2010 and to last 3 years.
La formalisation de démonstrations complexes comme celle du théorème des quatre couleurs ou celle de la correction d'un compilateur ont montré l'importance crucial de l'intégration du calcul dans les démonstrations. En déduction modulo, les systèmes de déduction sont appliqués modulo une congruence sur les formules logiques qui représente le calcul, et qui est le plus souvent spécifiée à l'aide d'un système de réécriture. En encodant une théorie dans la congruence, on peut dériver de la déduction modulo des prouveurs qui sont mieux adaptés à cette théorie. De plus, on peut réduire arbitrairement la taille des démonstrations. On obtient aussi un formalisme très expressif : il est possible d'y encoder l'arithmétique, la théorie des ensembles de Zermelo, mais aussi des systèmes d'ordre supérieur comme la théorie simple des types de Church (HOL) ou bien les systèmes de type purs (les systèmes qui servent de fondation aux assistants à la démonstration comme Coq). Cette expressivité permet d'envisager la déduction modulo comme un cadre universel pour faire des démonstrations, dans lequel sont traduites et combinées des démonstrations provenant de prouveurs extérieurs (automatiques et/ou interactifs).
Proof normalization is a fundamental property that ensures witness and disjunction properties for constructive proofs, completeness of certain methods of automated deduction, etc... In 1971, following the work of Tait, Girard developed a method, called reducibility candidates, for building proofs of strong normalization, giving, by the universal aspect of its method, a sound criterion for proof normalization in various logical frameworks. But this criterion is not known to be complete, there could exists normalizing theories for which one cannot build such a set of reducibility candidates. In this talk, we present how to refine this notion of reducibility candidates in order to provide a sound and complete criterion for proof normalization. This criterion is defined for the $\lambda \Pi$-calculus modulo, a logical framework with dependent types in which theories such as functional Pure Type Systems can be expressed within a set of rewrite rules.
La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Le principal outil industriel dans ce domaine est Simulink. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications permet de valider les logiciels embarqués en étant au plus près de leurs modes de fonctionnement. Nous présentons une analyse statique par interprétation abstraite de modèles Simulink. L'objectif de cette analyse est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs.
LISE is a multidisciplinary project involving lawyers and computer scientists with the aim to put forward a set of methods and tools to (1) define software liability in a precise and unambiguous way and (2) establish such liability in case of incident. This talk provides an overview of the overall approach taken in the project based on a case study. The case study illustrates a situation where, in order to reduce legal uncertainties, the parties to a contract wish to include in the agreement specific clauses to define as precisely as possible the share of liabilities between them for the main types of failures of the system.