• DocumentCode
    646433
  • Title

    Verification of embedded control programs

  • Author

    Thao Dang ; Jeannet, Bertrand ; Testylier, Romain

  • Author_Institution
    VERIMAG, France
  • fYear
    2013
  • fDate
    17-19 July 2013
  • Firstpage
    4252
  • Lastpage
    4256
  • Abstract
    In this paper we are concerned with the problem of verifying embedded control programs. The approach we use combines the logico-numerical techniques developed for the verification of Lustre programs and the set-based image computation for continuous systems. The practical interest of this approach lies in the fact that there exists a tool for generating Lustre code for controllers described in Simulink. We also illustrate the approach with some experimental results obtained for a robotic controller for LEGO Mindstorm.
  • Keywords
    continuous systems; control engineering computing; embedded systems; numerical analysis; program compilers; program verification; LEGO Mindstorm; Lustre code generation; Lustre program verification; Simulink; continuous systems; embedded control program verification; logico-numerical techniques; robotic controller; set-based image computation; Computational modeling; Polynomials; Robot sensing systems; Software packages; Vectors;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Control Conference (ECC), 2013 European
  • Conference_Location
    Zurich
  • Type

    conf

  • Filename
    6669843