A new static analyzer is described, based on the analyzer Fluctuat, Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are added to the program that simulate the action of sensors and actuators, making the continuous environment and the program communicate; We demonstrate our approach on an industrial case study, a part of the flight control software of ASTRIUM's Automated Transfer Vehicle (ATV).
展开▼
