Advertisement

HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment

  • Olivier Bouissou
  • Eric Goubault
  • Sylvie Putot
  • Karim Tekkal
  • Franck Vedrine
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

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).

Keywords

Hybrid System Control Software Abstract Interpretation Hybrid Automaton Numerical Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 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
  4. 4.
    Bouissou, O., Martel, M.: Abstract interpretation of the physical inputs of embedded programs. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 1–3. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Cousot, P.: Integrating physical systems in the static analysis of embedded control software. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 135–138. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 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
  7. 7.
    Frehse, G.: Phaver: Algorithmic verification of hybrid systems past hytech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Goubault, E., Martel, M., Putot, S.: Asserting the precision of floating-point computations: A simple abstract interpreter. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 209–212. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: ERTS, SEE (2006)Google Scholar
  10. 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
  11. 11.
    Putot, S., Goubault, E., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Dagstuhl Seminar 2003. LNCS, vol. 2991, pp. 306–313. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Olivier Bouissou
    • 1
  • Eric Goubault
    • 1
  • Sylvie Putot
    • 1
  • Karim Tekkal
    • 2
  • Franck Vedrine
    • 1
  1. 1.CEA, LIST, Modelisation and Analysis of Systems in InteractionGif-sur-YvetteFrance
  2. 2.FCS DigiteoSaint-AubinFrance

Personalised recommendations