Abstract
Modern CPS should process large amount of data with high speed and reliability. To ensure that the system can handle varying volumes of data, the system designers usually rely on the architectures with the dynamically scaling degree of parallelism. However, to guarantee resilience of data processing, we should also ensure system fault tolerance, i.e., integrate the mechanisms for dynamic reconfiguration. In this paper, we present an approach to formal modelling and assessment of reconfigurable dynamically scaling systems that guarantees resilience of data processing. We rely on modelling in Event-B to formally define the dynamic system architecture with the integrated dynamically scaling parallelism and reconfiguration. The formal development allows us to derive a complex system architecture and verify its correctness. To quantitatively assess resilience of data processing architecture, we rely on statistical model checking and evaluate the likelihood of successful data processing under different system parameters. The proposed integrated approach facilitates design space exploration and improves predictability in the development of complex data processing capabilities.
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: Modelling in Event-B. Cambridge University Press (2010)
Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A., Latvala, T.: Augmenting Event-B Modelling with Real-Time Verification. In: Proceedings of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches, FormSERA 2012 (2012)
Laibinis, L., Klionskiy, D., Troubitsyna, E., Dorokhov, A., Lilius, J., Kupriyanov, M.: The Final Report on the Development Project “Development of Information Preprocessing Algorithms”. LETI Reports. Saint Petersburg, Russian Federation (2013)
Lee, E.A.: Cyber Physical Systems: Design Challenges. In: 1st IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pp. 363–369. IEEE (2008)
Naidu, P.: Modern spectrum analysis of time series. CRC Press, New York (1996)
Rodin platform: Automated tool environment for Event-B, http://rodin-b-sharp.sourceforge.net/
Statistical UPPAAL: SMC extension of UPPAAL, http://www.cs.aau.dk/~adavid/smc
Su, L.: Resource efficient information integration in cyber-physical systems. PhD Thesis. Univ. of Urbana Champain, USA (2014)
Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Towards Probabilistic Modelling in Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 275–289. Springer, Heidelberg (2010)
Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 237–252. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Laibinis, L., Klionskiy, D., Troubitsyna, E., Dorokhov, A., Lilius, J., Kupriyanov, M. (2014). Modelling Resilience of Data Processing Capabilities of CPS. In: Majzik, I., Vieira, M. (eds) Software Engineering for Resilient Systems. SERENE 2014. Lecture Notes in Computer Science, vol 8785. Springer, Cham. https://doi.org/10.1007/978-3-319-12241-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-12241-0_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12240-3
Online ISBN: 978-3-319-12241-0
eBook Packages: Computer ScienceComputer Science (R0)