Logo PTI Logo FedCSIS

Proceedings of the 16th Conference on Computer Science and Intelligence Systems

Annals of Computer Science and Information Systems, Volume 25

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

, , , , , , ,

DOI: http://dx.doi.org/10.15439/2021F98

Citation: Proceedings of the 16th Conference on Computer Science and Intelligence Systems, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 25, pages 485–488 ()

Full text

Abstract. The choice of an adequate notation and subsequent system formalization is a crucial point for the design of cyber-physical systems (CPSs). Here, appropriate notations allow an explicit formulation of the deterministic system behavior under initial states and known inputs. In this paper, we examine and analyse different industrial notations for the design of hybrid systems such as Matlab/Simulink. We base our investigation on an industrial example (water tank), which contains nominal and safety-critical states. We especially focus on the notation's support to validate/verify crucial safety properties.

References

  1. A. Platzer (2018). Logical Foundations of Cyber-Physical Systems. Springer. http://dx.doi.org/10.1007/978-3-319-63588-0.
  2. Alur, R., Dang, T., Esposito, J., Fierro, R., Hur, Y., Ivancic, F., Kumar, V., Lee, I., Mishra, P., Pappas, G., and Sokolsky, O. (2001). Hierarchical hybrid modeling of embedded systems. In EMSOFT 2001: Embedded Software, First International Workshop, 14–31. Springer-Verlag.
  3. Alur, R., Henzinger, T.A., and Ho, P.H. (1993). Automatic symbolic verification of embedded systems. In Proc. of the 14th Annual Real-time Systems Symp., 2–11.
  4. Alur, R., Courcoubetis, C., Henzinger, T.A., and Ho, P. (1992). Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Grossman et al. (1993), 209–229. http://dx.doi.org/10.1007/3-540-57318-6. URL https://doi.org/10.1007/3-540-57318-6.
  5. Asarin, E., Dang, T., and Maler, O. (2002). The d/dt tool for verification of hybrid systems. In Proc. of 14th Intl. Conf. on Computer-Aided Verification, 365–370.
  6. Baar, T. and Staroletov, S. (2018). A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier. Modeling and Analysis of Information Systems, 25(5), 465–480.
  7. Basile, F., Chiacchio, P., and Gerbasio, D. (2013). On the Implementation of Industrial Automation Systems Based on PLC. IEEE Trans. on automation science and engineering, 10(4), 990–1003.
  8. Blanke, M., Kinnaert, M., Lunze, J., and Staroswiecki, M. (2006). Diagnosis and Fault-Tolerant Control. Springer-Verlag Berlin Heidelberg, 2nd edition.
  9. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., and Yovine, S. (1998). Kronos: A model-checking tool for realtime systems. In A.J. Hu and M.Y. Vardi (eds.), 10th Intl. Conf. on Computer-Aided Verification, 546–550. Springer-Verlag.
  10. Carloni, L.P., Passerone, R., Pinto, A., and Sangiovanni-Vincentelli, A.L. (2006). Languages and tools for hybrid systems design. Foundations and Trends in Electronic Design Automation, 1(1/2), 1–193.
  11. Deshpande, A., Göllü, A., and Varaiya, P. (1996). Shift: a formalism and a programming language for dynamic networks of hybrid automata. In P.J. Antsaklis, W. Kohn, A. Nerode, and S. Sastry (eds.), Hybrid Systems, volume 1273, 113–133. Springer. http://dx.doi.org/10.1007/BFb0031558.
  12. Fourlas, G.K., Kyriakopoulos, K.J., and Vournas, C.D. (2004). Hybrid systems modeling for power systems. Circuits and Systems Magazine, IEEE, 4(3), 16–23. http://dx.doi.org/10.1109/MCAS.2004.1337806.
  13. Grossman, R.L., Nerode, A., Ravn, A.P., and Rischel, H. (eds.) (1993). Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer. http://dx.doi.org/10.1007/3-540-57318-6. URL https://doi.org/10.1007/3-540-57318-6.
  14. Henzinger, T.A. (1996). 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, 278–292. IEEE Computer Society. http://dx.doi.org/10.1109/LICS.1996.561342. URL https://doi.org/10.1109/LICS.1996.561342.
  15. International Electrotechnical Commission (2003a). Iec 61131-3: Programmable controllers part 3: Programming languages.
  16. International Electrotechnical Commission (2004/2005b). Iec 61499: Function blocks for industrial process measurement and control systems, parts 1 - 4.
  17. Jeannin, J.B., Ghorbal, K., Kouskoulas, Y., Schmidt, A., Gardner, R., Mitsch, S., and Platzer, A. (2017). A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. International Journal on Software Tools for Technology Transfer, 19(6), 717–741. http://dx.doi.org/10.1007/s10009-016-0434-1.
  18. Kroll, A. and Schulte, H. (2014). Benchmark problems for nonlinear system identification and control using soft computing methods: Need and overview. Applied Soft Computing, 25(12), 496–513.
  19. Larsen, K.G. (2009). Verification and performance analysis for embedded systems. In Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society, Tianjin, China. http://dx.doi.org/10.1109/TASE.2009.66.
  20. Lee, E.A. (2016). Fundamental limits of cyber-physical systems modeling. ACM Transactions on Cyber-Physical Systems, 1(1). http://dx.doi.org/10.1145/2912149. Mitsch, S. and Platzer, A. (2016). Modelplex: verified runtime validation of verified cyber-physical system models. Formal Methods System Design, 49(1,2), 33–74. http://dx.doi.org/10.1007/s10703-016-0241-z.
  21. Platzer, A. (2010). Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg. http://dx.doi.org/10.1007/978-3-642-14509-4. Quesel, J.D., Mitsch, S., Loos, S., Aréchiga, N., and Platzer, A. (2016). How to model and prove hybrid systems with KeYmaera: A tutorial on safety. STTT, 18(1), 67–91. http://dx.doi.org/10.1007/s10009-015-0367-0.
  22. Rozov, A.S. and Zyubin, V.E. (2013). Process-oriented programming language for MCU-based automation. 2013 International Siberian Conference on Control and Communications (SIBCON), 1–4.
  23. Rozov, A.S. and Zyubin, V.E. (2015). A hyperprocess-based approach in Arduino programming. International Conference on Advanced Technology & Sciences (ICAT15).
  24. Silva, B.I., Stursberg, O., Krogh, B.H., and Engell, S. (2001). 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, 2867–2874.
  25. Staroletov, S., Shilov, N., Konyukhov, I., Zyubin, V., Liakh, T., Rozov, A., Shilov, I., Baar, T., and Schulte, H. (2019). Model-driven methods to design of reliable multiagent cyber-physical systems. In CEUR Workshop Proceedings, volume 2478, 74–91. URL http://ceur-ws.org/Vol-2478/paper7.pdf.
  26. Staroletov, S. (2017). Design and implementation a software for water purification with using automata approach and specification based analysis. System Informatics, 10(33-34).
  27. Staroletov, S. and Shilov, N.V. (2019). Applying model checking approach with floating point arithmetic for verification of air collision avoidance maneuver hybrid model. In F. Biondi, T.
  28. Given-Wilson, and A. Legay (eds.), Model Checking Software - 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings, volume 11636 of Lecture Notes in Computer Science, 193–207. Springer. http://dx.doi.org/10.1007/978-3-030-30923-7 11.
  29. Thramboulidis, K. and Frey, G. (2011). An MDD Process for IEC 61131-based Industrial Automation Systems. In 16th IEEE International Conference on Emerging Technologies and Factory Automation, (ETFA11), September 5-9, 2011, Toulouse, France.
  30. Todorov, V., Boulanger, F., and Taha, S. (2018). Formal verification of automotive embedded software. In S. Gnesi, N. Plat, P. Spoletini, and P. Pelliccione (eds.), Proceedings of the 6th Conference on Formal Methods in Software Engineering, FormaliSE 2018, collocated with ICSE 2018, Gothenburg, Sweden, June 2, 2018, 84–87. ACM. http://dx.doi.org/10.1145/3193992.3194003. URL https://doi.org/10.1145/3193992.3194003.
  31. Torrisi, F.D. and Bemporad, A. (2004). HYSDEL - a tool for generating computational hybrid models for analysis and synthesis problems. IEEE Transactions on Control Systems Technology, 12, 235–249.
  32. Wagner, F., Schmuki, R., Wagner, T., and Wolstenholme, P. (2006). Modeling Software with Finite State Machines. Auerbach Publications, Boston, MA, USA.
  33. Zyubin, V.E. (2007). Hyper-automaton: A Model of Control Algorithms. In O. Stukach (ed.), IEEE International Siberian Conference on Control and Communications (SIBCON-2007). Proceedings., 51–57. IEEE, Tomsk, Russia. http://dx.doi.org/10.1109/SIBCON.2007.371297.