Invisible Formal Methods for Safety Assurance of Aerospace Applications
10.10.07 - 07:04
French-Algerian Cycle of Seminars
Following an initiative of Marc Daumas (LIRMM & ELIAUS) and Professeur Mohamed Mezghiche, we had in the summer of 2007 a cycle of seminars between the University of Perpignan Via Domitia and the University M’hamed Bougara of Boumerdès in Algeria. The first two seminars were broadcasted live and the last two ones were recorded.
Speaker: César Muñoz
National Institute of Aerospace at NASA Langley Research Center
César Muñoz has been an Invited Professor of the University of Perpignan Via Domitia in June 2007 funded by the UFR SEE of the University of Perpignan Via Domitia. Report of his work is available from HAL.
Abstract
The expression « Invisible Formal Methods », coined by J. Rushby at SRI International, refers to the use of formal analysis tools in an unobtrusive way, e.g., in a way that is acceptable to the engineering practice. This is done by providing a set of tools that increase the safety assurance by incrementally performing a series non-trivial formal analyses. In this talk, we report on our experience at NIA on the use of invisible formal methods for the safety analysis of aerospace applications. First, we present a series of automated strategies for proving real number properties on theorem provers. These strategies are at the base of a tool that formally verifies computational errors of expressions using interval analysis. This tool requires a minimum user interaction with the theorem prover. Finally, we present an automated tool for checking safety properties of C programs involving non-linear arithmetic. This tool integrates a constraint solver for interval arithmetic to Berkeley Lazy Abstraction Software Verification Tool (BLAST).
Tags: aérospace, formal methods, seminars
Fil baladodiffusion
Fil articles
Ecrivez un commentaire