maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2019-4-488-501mais-1272Research ArticleComputing Methodologies and ApplicationsАнализ безопасности контроллеров продольного движения во время набора высотыSafety Analysis of Longitudinal Motion Controllers during Climb Flighthttps://orcid.org/0000-0002-8443-1558БаарТомасBaarThomasthomas.baar@htw-berlin.dehttps://orcid.org/0000-0001-5851-3616ШультеХорстSchulteHorsthorst.schulte@htw-berlin.deHochschule f¨ur Technik und Wirtschaft (HTW)ГерманияHochschule f¨ur Technik und Wirtschaft (HTW)Germany201913122019264488501Copyright © Баар Т., Шульте Х., 20192019Баар Т., Шульте Х.Baar T., Schulte H.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1272

Во время набора высоты на больших пассажирских самолетах вертикальное движение самолета, то есть его угол наклона, зависит от угла отклонения руля высоты, выбранного пилотом. Если угол наклона становится слишком большим, самолет рискует нарушить воздушный поток на крыльях, что может привести к его падению. В некоторых самолетах пилоту помогает программное обеспечение, задачей которого является предотвращение нарушения воздушного потока. Когда угол наклона становится больше определенного порога, программное обеспечение отменяет решения пилота относительно угла отклонения руля высоты и обеспечивает предположительно безопасные значения. Хотя вспомогательное программное обеспечение может помочь предотвратить человеческие сбои, само программное обеспечение также подвержено ошибкам и, как правило, представляет собой риск для тщательной оценки. Например, если разработчики программного обеспечения забыли, что датчики могут давать неправильные данные, программное обеспечение может привести к тому, что угол наклона станет отрицательным. Следовательно, самолет теряет высоту и может – в конечном итоге – разбиться.

В этой статье мы представляем исполняемую модель, написанную на Matlab/Simulink® для системы управления пассажирским самолетом. Наша модель также учитывает программное обеспечение, помогающее пилоту предотвращать нарушение воздушного потока. При моделировании набора высоты с использованием нашей модели легко увидеть, что самолет может потерять высоту, если данные, предоставленные датчиком угла наклона, неверны. Для противоположного случая правильных данных датчика, моделирование предполагает, что система управления работает правильно и способна эффективно предотвращать нарушение воздушного потока.

Однако симуляция не является гарантией безопасности системы управления. По этой причине мы переводим Matlab/Simulink®-модель в гибридную программу (НР), т. е. во входной синтаксис средства доказательства теорем KeYmaera. Это открывает путь для формальной проверки свойств безопасности систем управления, смоделированных в Matlab/Simulink®. В качестве дополнительного вклада в эту статью мы обсудим текущие ограничения нашей трансформации. Например, оказывается, что простые пропорциональные (Р) контроллеры могут быть легко представлены программами НР, но более продвинутые контроллеры РD (пропорционально-производные) или РID (пропорционально-интегрально-производные) могут быть представлены как программы НР только в исключительных случаях.

During the climb flight of big passenger airplanes, the airplane’s vertical movement, i.e. its pitch angle, results from the elevator deflection angle chosen by the pilot. If the pitch angle becomes too large, the airplane is in danger of an airflow disruption at the wings, which can cause the airplane to crash. In some airplanes, the pilot is assisted by a software whose task is to prevent airflow disruptions. When the pitch angle becomes greater than a certain threshold, the software overrides the pilot’s decisions with respect to the elevator deflection angle and enforces presumably safe values. While the assistance software can help to prevent human failures, the software itself is also prone to errors and is - generally - a risk to be assessed carefully. For example, if software designers have forgotten that sensors might yield wrong data, the software might cause the pitch angle to become negative. Consequently, the airplane loses height and can - eventually - crash.

In this paper, we provide an executable model written in Matlab/Simulink® for the control system of a passenger airplane. Our model takes also into account the software assisting the pilot to prevent airflow disruptions. When simulating the climb flight using our model, it is easy to see that the airplane might lose height in case the data provided by the pitch angle sensor are wrong. For the opposite case of correct sensor data, the simulation suggests that the control system works correctly and is able to prevent airflow disruptions effectively.

The simulation, however, is not a guarantee for the control system to be safe. For this reason, we translate the Matlab/Simulink® -model into a hybrid program (HP), i.e. into the input syntax of the theorem prover KeYmaera. This paves the way to formally verify safety properties of control systems modelled in Matlab/Simulink®. As an additional contribution of this paper, we discuss the current limitations of our transformation. For example, it turns out that simple proportional (P) controllers can be easily represented by HP programs, but more advanced PD (proportional-derivative) or PID (proportional-integral-derivative) controllers can be represented as HP programs only in exceptional cases.

киберфизическая система (CРS)анализ формальной безопасностигибридный автоматCyber-Physical System (CPS)Formal Safety AnalysisHybrid AutomatonReferencesStengel R. F., Flight Dynamics, Princeton University Press, 2004.Stengel R. F., Flight Dynamics, Princeton University Press, 2004.Yechout T. R., Introduction to Aircraft Flight Mechanics, American Institute of Aeronautics & Astronautics, 2003.Yechout T. R., Introduction to Aircraft Flight Mechanics, American Institute of Aeronautics & Astronautics, 2003.Platzer A., Logical Foundations of Cyber-Physical Systems, Springer, Heidelberg, 2018.Platzer A., Logical Foundations of Cyber-Physical Systems, Springer, Heidelberg, 2018.Platzer A., Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, Heidelberg, 2010.Platzer A., Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, Heidelberg, 2010.Platzer A., “Logic and Compositional Verification of Hybrid Systems (Invited Tutorial)”, In: Gopalakrishnan G., Qadeer S. (eds) Computer Aided Verification. CAV 2011. LNCS. Springer, Berlin, Heidelberg, 6806 (2011), 28–43.Platzer A., “Logic and Compositional Verification of Hybrid Systems (Invited Tutorial)”, In: Gopalakrishnan G., Qadeer S. (eds) Computer Aided Verification. CAV 2011. LNCS. Springer, Berlin, Heidelberg, 6806 (2011), 28–43.Quesel J. D., Mitsch S., Loos S., Ar´echiga N., Platzer A., “How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety”, International Journal on Software Tools for Technology Transfer, 18:1 (2016), 67–91.Quesel J. D., Mitsch S., Loos S., Ar´echiga N., Platzer A., “How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety”, International Journal on Software Tools for Technology Transfer, 18:1 (2016), 67–91.Henzinger T. A., “The Theory of Hybrid Automata”, Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 1996, 278– 292.Henzinger T. A., “The Theory of Hybrid Automata”, Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 1996, 278– 292.Baar T., “A Metamodel-Based Approach for Adding Modularization to KeYmaera’s InputSyntax”, Proceedings, 11th A. P. Ershov Informatics Conference, Akademgorodok, Novosibirsk, Russia. 2019.Baar T., “A Metamodel-Based Approach for Adding Modularization to KeYmaera’s InputSyntax”, Proceedings, 11th A. P. Ershov Informatics Conference, Akademgorodok, Novosibirsk, Russia. 2019.Harel D., Kozen D., Tiuryn J., Dynamic Logic, MIT Press Cambridge, 2000.Harel D., Kozen D., Tiuryn J., Dynamic Logic, MIT Press Cambridge, 2000.Frehse G., Kekatos N., Nickovic D., Oehlerking J., Schuler S., Walsch A., Woehrle M., “A Toolchain for Verifying Safety Properties of Hybrid Automata via Pattern Templates”, Proceedings, Annual American Control Conference (ACC), Milwaukee, USA, 2018, 2384– 2391.Frehse G., Kekatos N., Nickovic D., Oehlerking J., Schuler S., Walsch A., Woehrle M., “A Toolchain for Verifying Safety Properties of Hybrid Automata via Pattern Templates”, Proceedings, Annual American Control Conference (ACC), Milwaukee, USA, 2018, 2384– 2391.Alur R., Courcoubetis C., Henzinger T. A., Ho P. H., “Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems”, International Hybrid Systems Workshop. LNCS, Springer, Berlin, Heidelberg, 736 (1991), 209–229.Alur R., Courcoubetis C., Henzinger T. A., Ho P. H., “Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems”, International Hybrid Systems Workshop. LNCS, Springer, Berlin, Heidelberg, 736 (1991), 209–229.Osher S., Sethian J. A., “Fronts Propagating with Curvature-dependent Speed: Algorithms Based on Hamilton-Jacobi Formulations”, Journal of Computational Physics, 79:1 (1988), 12–49.Osher S., Sethian J. A., “Fronts Propagating with Curvature-dependent Speed: Algorithms Based on Hamilton-Jacobi Formulations”, Journal of Computational Physics, 79:1 (1988), 12–49.Tomlin C. J., Mitchell I., Bayen A. M., Oishi M., “Computational Techniques for the Verification of Hybrid Systems”, Proceedings of the IEEE, 91:7 (2003), 986–1001.Tomlin C. J., Mitchell I., Bayen A. M., Oishi M., “Computational Techniques for the Verification of Hybrid Systems”, Proceedings of the IEEE, 91:7 (2003), 986–1001.Asarin E., Bournez O., Dang T., Maler O., “Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems”, In: Lynch N., Krogh B.H. (eds) Hybrid Systems: Computation and Control. HSCC 2000. LNCS, Springer, Berlin, Heidelberg, 1790 (2000), 20–31.Asarin E., Bournez O., Dang T., Maler O., “Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems”, In: Lynch N., Krogh B.H. (eds) Hybrid Systems: Computation and Control. HSCC 2000. LNCS, Springer, Berlin, Heidelberg, 1790 (2000), 20–31.Clarke Jr. E. M., Grumberg O., Kroening D., Peled D., Veith H., Model Checking (second edition), MIT Press, 2018.Clarke Jr. E. M., Grumberg O., Kroening D., Peled D., Veith H., Model Checking (second edition), MIT Press, 2018.Chen J., Patton R. J., Robust Model-Based Fault Diagnosis for Dynamic Systems, Kluwer Academic Publishers Norwell, MA, USA, 1999.Chen J., Patton R. J., Robust Model-Based Fault Diagnosis for Dynamic Systems, Kluwer Academic Publishers Norwell, MA, USA, 1999.Goupil P., Marcos A., Advanced Diagnosis for Sustainable Flight Guidance and Control: The European ADDSAFE Project, SAE technical paper 2011-01-2804, 2011.Goupil P., Marcos A., Advanced Diagnosis for Sustainable Flight Guidance and Control: The European ADDSAFE Project, SAE technical paper 2011-01-2804, 2011.Goupil P., Marcos A., “Industrial Benchmarking and Evaluation of ADDSAFE FDD Design”, In Proc. of 8th IFAC Symposium on Fault Detection, Supervision and Safety of Technical Processes, 45:20 (2012), 1131–1136.Goupil P., Marcos A., “Industrial Benchmarking and Evaluation of ADDSAFE FDD Design”, In Proc. of 8th IFAC Symposium on Fault Detection, Supervision and Safety of Technical Processes, 45:20 (2012), 1131–1136.Grenaille S., Henry D., Zolghadri A., “A method for designing fault diagnosis filters for LPV polytopic systems”, Journal of Control Science and Engineering, 2008.Grenaille S., Henry D., Zolghadri A., “A method for designing fault diagnosis filters for LPV polytopic systems”, Journal of Control Science and Engineering, 2008.Christopher E., Thomas L., Hafid S., “Fault Tolerant Flight Control: A Benchmark Challenge”, Lecture Notes in Control and Information Sciences, 399 (2010).Christopher E., Thomas L., Hafid S., “Fault Tolerant Flight Control: A Benchmark Challenge”, Lecture Notes in Control and Information Sciences, 399 (2010).Witczak M., “Fault Diagnosis and Fault-Tolerant Control Strategies for Non-Linear Systems”, Lecture Notes in Electrical Engineering, Springer, 266 (2014), 375–392.Witczak M., “Fault Diagnosis and Fault-Tolerant Control Strategies for Non-Linear Systems”, Lecture Notes in Electrical Engineering, Springer, 266 (2014), 375–392.Mitsch S., Loos S. M., Platzer A., “Towards Formal Verification of Freeway Traffic Control”, In Proc. of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems(ICCPS), 2012, 171–180.Mitsch S., Loos S. M., Platzer A., “Towards Formal Verification of Freeway Traffic Control”, In Proc. of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems(ICCPS), 2012, 171–180.Jeannin J. B., Ghorbal K., Kouskoulas Y., Gardner R., Schmidt A., Zawadzki E., Platzer A., “A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System”, In Proc. of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015, 21–36.Jeannin J. B., Ghorbal K., Kouskoulas Y., Gardner R., Schmidt A., Zawadzki E., Platzer A., “A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System”, In Proc. of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015, 21–36.Platzer A., Quesel J. D., “European Train Control System: A Case Study in Formal Verification”, In: Breitman K., Cavalcanti A. (eds) Formal Methods and Software Engineering. ICFEM 2009. LNCS, Springer, 5885 (2009), 246–265.Platzer A., Quesel J. D., “European Train Control System: A Case Study in Formal Verification”, In: Breitman K., Cavalcanti A. (eds) Formal Methods and Software Engineering. ICFEM 2009. LNCS, Springer, 5885 (2009), 246–265.Frehse G., Le Guernic C., Donz´e A.,Cotton S., Ray R., Lebeltel O., Ripado R., Girard A., Dang Th. Maler O., “SpaceEx: Scalable Verification of Hybrid Systems”, In: Gopalakrishnan G., Qadeer S. (eds) Computer Aided Verification. CAV 2011. LNCS, Springer, 6806 (2011), 379–395.Frehse G., Le Guernic C., Donz´e A.,Cotton S., Ray R., Lebeltel O., Ripado R., Girard A., Dang Th. Maler O., “SpaceEx: Scalable Verification of Hybrid Systems”, In: Gopalakrishnan G., Qadeer S. (eds) Computer Aided Verification. CAV 2011. LNCS, Springer, 6806 (2011), 379–395.Chen X., Abrah´am E., Sankaranarayanan S., “Flow*: An Analyzer for Non-linear Hy- ´ brid Systems”, In: Sharygina N., Veith H. (eds) Computer Aided Verification. CAV 2013. LNCS, Springer, 8044 (2013), 258–263.Chen X., Abrah´am E., Sankaranarayanan S., “Flow*: An Analyzer for Non-linear Hy- ´ brid Systems”, In: Sharygina N., Veith H. (eds) Computer Aided Verification. CAV 2013. LNCS, Springer, 8044 (2013), 258–263.Cimatti A., Griggio A., Mover S., Tonetta S., “HyComp: An SMT-Based Model Checker for Hybrid Systems”, In: Baier C., Tinelli C. (eds) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Springer, 9035 (2015), 52–67.Cimatti A., Griggio A., Mover S., Tonetta S., “HyComp: An SMT-Based Model Checker for Hybrid Systems”, In: Baier C., Tinelli C. (eds) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Springer, 9035 (2015), 52–67.“Formal Verification of Hybrid Systems Using CheckMate: A Case Study”, Proceedings of the 2000 American Control Conference, 3 (2000), 1679–1683.“Formal Verification of Hybrid Systems Using CheckMate: A Case Study”, Proceedings of the 2000 American Control Conference, 3 (2000), 1679–1683.Zolghadri A., “Advanced Model-Based FDIR Techniques for Aerospace Systems: Today Challenges and Opportunities”, Progress in Aerospace Sciences, Elsevier, 53 (2012), 18– 29.Zolghadri A., “Advanced Model-Based FDIR Techniques for Aerospace Systems: Today Challenges and Opportunities”, Progress in Aerospace Sciences, Elsevier, 53 (2012), 18– 29.Grenaille S., Henry D., Zolghadri A., “A Method for Designing Fault Diagnosis Filters for LPV Polytopic Systems”, Journal of Control Science and Engineering, 2008, 1–11.Grenaille S., Henry D., Zolghadri A., “A Method for Designing Fault Diagnosis Filters for LPV Polytopic Systems”, Journal of Control Science and Engineering, 2008, 1–11.Witczak M., Dziekan L., Puig V., Korbicz J., “Design of a Fault-Tolerant Control Scheme for Takagi-Sugeno Fuzzy Systems”, In Proc. 16th Mediterranean Conference on Control and Automation, 2008, 280–285.Witczak M., Dziekan L., Puig V., Korbicz J., “Design of a Fault-Tolerant Control Scheme for Takagi-Sugeno Fuzzy Systems”, In Proc. 16th Mediterranean Conference on Control and Automation, 2008, 280–285.

The authors declare that there are no conflicts of interest present.