Abstract
We present MoDeS3, a complex research demonstrator illustrating the combined use of model-driven development, formal verification, safety engineering and IoT technologies for smart and safe cyber-physical systems. MoDeS3 represents a smart transportation system-of-systems composed of a model railway and a crane which may automatically load and unload cargo from trains where both subsystems need to fulfill functional and safety requirements. The demonstrator is built by using the model-based software engineering principle, while the system level safety is ensured by the combined use of design-time and runtime verification and validation techniques.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Balogh, L., et al.: Distributed and heterogeneous event-based monitoring in smart cyber-physical systems. In: MT CPS Workshop (CPS Week 2016) (2016)
Behrmann, G., et al.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems, pp. 125–126. IEEE (2006)
Búr, M., et al.: Distributed graph queries for runtime monitoring of cyber-physical systems. In: International Conference on Fundamental Approaches to Software Engineering (2018, accepted)
Cheng, B.H.C., et al.: Using models at runtime to address assurance for self-adaptive systems. In: Bencomo, N., France, R., Cheng, B.H.C., Aßmann, U. (eds.) Models@run.time. LNCS, vol. 8378, pp. 101–136. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08915-7_4
Dávid, I., Ráth, I., Varró, D.: Foundations for streaming model transformations by complex event processing. Softw. Syst. Model. 17(1), 1–28 (2016)
Dubey, A., et al.: Resilience at the edge in cyber-physical systems. In: FMEC, pp. 139–146, May 2017
Havelund, K.: Rule-based runtime verification revisited. STTT 17(2), 143–170 (2015)
Lee, E.A.: Cyber physical systems: design challenges. In: 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing, pp. 363–369 (2008)
Lee, E.A., et al.: The swarm at the edge of the cloud. IEEE Des. Test 31(3), 8–20 (2014)
Medhat, R., et al.: Runtime monitoring of cyber-physical systems under timing and memory constraints. ACM T. Embed. Comput. Syst. 14(4), 1–29 (2015)
Molnár, V., et al.: The gamma statechart composition framework. In: ICSE 2018: Demonstrations (2018, accepted)
Nielsen, C.B., et al.: Systems of systems engineering: basic concepts, model-based techniques, and research directions. ACM Comput. Surv. 48(2), 18 (2015)
Rushby, J.: Runtime certification. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 21–35. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89247-2_2
Tóth, T., Vörös, A.: Verification of a real-time safety-critical protocol using a modelling language with formal data and behaviour semantics. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds.) SAFECOMP 2014. LNCS, vol. 8696, pp. 207–218. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10557-4_24
Vierhauser, M., et al.: Reminds: a flexible runtime monitoring framework for systems of systems. J. Syst. Softw. 112, 123–136 (2016)
Acknowledgment
MoDeS3 is a joint effort of many participants. It was partially supported by MTA-BME Lendület Research Group on Cyber-Physical Systems the ARTEMIS JU R5-COP project and the NSERC RGPIN-04573-16 project. MoDeS3 also received financial and technical support from our industrial partners: IncQuery Labs Ltd., Quanopt Ltd., Ericsson Hungary and Miniversum. The TITAN Xp used for this research was donated by the NVIDIA Corporation. Colleagues at Dept. of Measurement and Information Systems (BME) worked on the project beside the authors: István Majzik, Gábor Szárnyas, and Oszkár Semeráth. We also thank the hard work of our students: Flórán Deé, Márton Elekes, Anna Gujgiczer, Bence Graics, Raimund Konnerth, Gergő Somos, and Sámuel Várallyay.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Vörös, A. et al. (2018). MoDeS3: Model-Based Demonstrator for Smart and Safe Cyber-Physical Systems. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science(), vol 10811. Springer, Cham. https://doi.org/10.1007/978-3-319-77935-5_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-77935-5_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-77934-8
Online ISBN: 978-3-319-77935-5
eBook Packages: Computer ScienceComputer Science (R0)