HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment
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).
KeywordsHybrid System Control Software Abstract Interpretation Hybrid Automaton Numerical Program
- 3.Bouissou, O., Martel, M.: GRKLib: a guaranteed runge-kutta library. In: Follow-up of International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics. IEEE Press, Los Alamitos (2007)Google Scholar
- 6.Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages 4, 238–252 (1977)Google Scholar
- 9.Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: ERTS, SEE (2006)Google Scholar
- 10.Kowalewski, S., Stursberg, O., Fritz, M., Graf, H., Preuß, I.H.J., et al.: A case study in tool-aided analysis of discretely controlled continuous systems: the two tanks problem. In: Antsaklis, P.J., Kohn, W., Lemmon, M.D., Nerode, A., Sastry, S.S. (eds.) HS 1997. LNCS, vol. 1567, p. 163. Springer, Heidelberg (1999)CrossRefGoogle Scholar