Critical control systems are often built as a combination of a control core with safety mechanisms allowing to recover from failures. For example a PID controller used with triplicated inputs. Typically those systems would be designed at the model level in a synchronous language like Lustre or Simulink, and their code automatically generated from those models.In previous SAE symposium, we addressed the formal analysis of such systems - focusing on the safety parts - using a combination of formal techniques, ie. k-induction and abstract interpretation.The approach developed here extends the analysis of the system to the control core. We present a new analysis framework combining the analysis of open-loop stable controller with those safety constructs. We introduce the basic analysis approaches: abstract interpretation synthesizing quadratic invariants and backward analysis based on quantifier elimination. Then we apply it on a simple but representative example that no other available state-of-the-art technique is able to analyze.This contribution is another step towards early use of formal methods for critical embedded software such as the ones of the aerospace industry.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses


    Weitere Titelangaben:

    Sae Int. J. Aerosp


    Beteiligte:

    Kongress:

    SAE 2013 AeroTech Congress & Exhibition ; 2013


    Erschienen in:

    Erscheinungsdatum :

    2013-09-17


    Format / Umfang :

    11 pages




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems

    Champion, Adrien / Roux, Pierre / Garoche, Pierre-loïc et al. | SAE Technical Papers | 2011



    Stability Analysis Methods: Linear Systems

    Bielawa, Richard L. | AIAA | 2006


    Generalized Linear Models for Analyses of Kilometrage and Accident Data

    Bäumer, Marcus / Hautzinger, Heinz / Heidemann, Dirk | ASCE | 2000


    Generalized linear models for analyses of kilometrage and accident data

    Baeumer, M. / Hautzinger, H. / Heidemann, D. | Tema Archiv | 2000