Modeling and Verification using Different Notations for CPSs: The One-Water-Tank Case Study

• Autorzy: Staroletov Sergey , Schulte Horst , Baar Thomas , Konyukhov Ivan , Shilov Nikolay , Rozov Andrei , Liakh Tatiana , Zyubin Vladimir

Identyfikatory

DOI

10.15439/2021F98

• Konferencja: Federated Conference on Computer Science and Information Systems (16 ; 02-05.09.2021 ; online)
• Języki publikacji: EN

Abstrakty

EN

The choice of an adequate notation and subsequent system formalization are the crucial points for the design of cyber-physical systems (CPSs). Here, an appropriate notation allows an explicit specification of the deterministic system behavior for specified initial states and inputs. We base our study on an industrial example (water tank) that comprises nominal as well as safety-critical states, and focus on the notation’s support to validate/verify crucial safety properties. Several industrial notations (e.g. Matlab/Simulink©) to design and simulate such a hybrid system have been tried based on our physical model. In addition, we remodel our example using the well-founded mathematical formalism of hybrid automata. It enables us to formally express and verify important safety properties using the theorem prover KeYmaera

Słowa kluczowe

EN

automata theory; cyber-physical systems; formal specification; formal verification; safety critical software; theorem proving

PL

teoria automatów; systemy cyber-fizyczne; formalna specyfikacja; weryfikacja formalna; oprogramowanie krytyczne dla bezpieczeństwa; dowodzenie twierdzeń

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2021
• Tom: Vol. 25
• Strony: 485--488
• Opis fizyczny: Bibliogr. 17 poz., wz., il.

Twórcy

autor

Staroletov Sergey

• Polzunov Altai State Technical University / Institute of Automation and Electrometry, Russia

autor

Schulte Horst

• HTW Berlin, School of Engineering I, Berlin, Germany

autor

Baar Thomas

• HTW Berlin, School of Engineering I, Berlin, Germany

autor

Konyukhov Ivan

• nnopolis University, Innopolis, Republic of Tatarstan, Russia

autor

Shilov Nikolay

• nnopolis University, Innopolis, Republic of Tatarstan, Russia

autor

Rozov Andrei

• Institute of Automation and Electrometry / NSU, Novosibirsk, Russia

autor

Liakh Tatiana

• Institute of Automation and Electrometry / NSU, Novosibirsk, Russia

autor

Zyubin Vladimir

• Institute of Automation and Electrometry / NSU, Novosibirsk, Russia

Bibliografia

• [1] M. Blanke, M. Kinnaert, J. Lunze, and M. Staroswiecki, Diagnosis and Fault-Tolerant Control, 2nd ed. Springer-Verlag Berlin Heidelberg, 2006. ISBN 978-3-540-35653-0
• [2] E. A. Lee, “Fundamental limits of cyber-physical systems modeling,” ACM Transactions on Cyber-Physical Systems, vol. 1, no. 1, 2016. doi: 10.1145/2912149
• [3] S. Staroletov, N. Shilov, I. Konyukhov, V. Zyubin, T. Liakh, A. Rozov, I. Shilov, T. Baar, and H. Schulte, “Model-driven methods to design of reliable multiagent cyber-physical systems,” in CEUR Workshop Proceedings, vol. 2478, 2019, pp. 74-91.
• [4] T. A. Henzinger, “The theory of hybrid automata,” in Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, 1996. doi: 10.1109/LICS.1996.561342 pp. 278-292.
• [5] R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, Eds., Hybrid Systems, ser. Lecture Notes in Computer Science, vol. 736. Springer, 1993. doi: 10.1007/3-540-57318-6
• [6] R. Alur, T. A. Henzinger, and P. H. Ho, “Automatic symbolic verification of embedded systems,” in Proc. of the 14th Annual Real-time Systems Symp., 1993. doi: 10.1109/32.489079 pp. 2-11.
• [7] B. I. Silva, O. Stursberg, B. H. Krogh, and S. Engell, “An assessment of the current status of algorithmic approaches to the verification of hybrid systems,” in Proc. of the 40th IEEE Conf. on Decision and Control, 2001. doi: 10.1109/CDC.2001.980711 pp. 2867-2874.
• [8] S. Mitsch and A. Platzer, “Modelplex: verified runtime validation of verified cyber-physical system models,” Formal Methods System Design, vol. 49, no. 1,2, pp. 33-74, 2016. doi: 10.1007/s10703-016-0241-z
• [9] A. Platzer, Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Heidelberg: Springer, 2010. ISBN 978-3-642-14508-7
• [10] A. Platzer, Logical Foundations of Cyber-Physical Systems. Springer, 2018. ISBN 978-3-319-63587-3
• [11] G. K. Fourlas, K. J. Kyriakopoulos, and C. D. Vournas, “Hybrid systems modeling for power systems,” Circuits and Systems Magazine, IEEE, vol. 4, no. 3, pp. 16-23, 2004. doi: 10.1109/MCAS.2004.1337806
• [12] K. G. Larsen, “Verification and performance analysis for embedded systems,” in Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). Tianjin, China: IEEE Computer Society, July 2009. doi: 10.1109/TASE.2009.66
• [13] A. Kroll and H. Schulte, “Benchmark problems for nonlinear system identification and control using soft computing methods: Need and overview,” Applied Soft Computing, vol. 25, no. 12, pp. 496-513, December 2014. doi: 10.1016/j.asoc.2014.08.034
• [14] I. Anureev, N. Garanina, T. Liakh, A. Rozov, H. Schulte, and V. Zyubin, “Towards safe cyber-physical systems: the Reflex language and its transformational semantics,” in 2019 International Siberian Conference on Control and Communications (SIBCON). IEEE, 2019. doi: 10.1109/SIBCON.2019.8729633 pp. 1-6.
• [15] R. Alur, C. Courcoubetis, T. A. Henzinger, and P. Ho, “Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems,” in Hybrid Systems, 1992. doi: 10.1007/3-540-57318-6 pp. 209-229.
• [16] J.-D. Quesel, S. Mitsch, S. Loos, N. Aréchiga, and A. Platzer, “How to model and prove hybrid systems with KeYmaera: A tutorial on safety,” STTT, vol. 18, no. 1, pp. 67-91, 2016. doi: 10.1007/s10009-015-0367-0
• [17] T. Baar and S. Staroletov, “A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier,” Modeling and Analysis of Information Systems, vol. 25, no. 5, pp. 465-480, 2018. doi: 10.18255/1818-1015-2018-5-465-480

Uwagi

1. Track 3: Software, System and Service Engineering

2. Short Papers