Abstract
Microservice based architectures have started to gain in popularity and are often adopted in the implementation of modern cloud, IoT, and large-scale distributed applications. Software life cycles, in this context, are characterized by short iterations, where several updates and new functionalities are continuously integrated many times a day. This paradigm shift calls for new formal approaches to systematic verification and testing of applications in production infrastructures. We introduce an approach to continuous, design- to run-time verification, of microservice based applications. This paper describes our envisioned approach, the current stage of this ongoing work, and the challenges ahead.
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
Similar content being viewed by others
Notes
- 1.
A list of all the available system tasks can be found in [5].
References
Dragoni, N., Giallorenzo, S., Lafuente, A.L., Mazzara, M., Montesi, F., Mustafin, R., Safina, L.: Microservices: yesterday, today, and tomorrow. Present and Ulterior Software Engineering, pp. 195–216. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67425-4_12
Microservices: a definition of this new architectural term, June 2017. https://martinfowler.com/articles/microservices.html
Erl, T.: Service-Oriented Architecture: Concepts, Technology, and Design. Prentice Hall PTR, Upper Saddle River (2005)
Netflix, Inc., June 2017. https://www.netflix.com/
Conductor, June 2017. https://netflix.github.io/conductor/
Ghezzi, C., Mandrioli, D., Morasca, S., Pezzè, M.: A unified high-level petri net formalism for time-critical systems. IEEE Trans. Softw. Eng. 17, 160–172 (1991)
Camilli, M., Gargantini, A., Scandurra, P.: Specifying and verifying real-time self-adaptive systems. In: 2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE), Nov 2015, pp. 303–313 (2015)
Camilli, M.: Petri nets state space analysis in the cloud. In: Proceedings of the 34th International Conference on Software Engineering, ser. ICSE 2012, pp. 1638–1640. IEEE Press, Piscataway (2012)
Camilli, M., Gargantini, A., Scandurra, P., Bellettini, C.: Event-based runtime verification of temporal properties using time basic petri nets. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 115–130. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_8
Uber Technologies, Inc., June 2017. https://www.uber.com/
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)
Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. SIGSOFT Softw. Eng. Notes 30(5), 273–282 (2005)
Conductor2Pn, June 2017. https://bitbucket.org/seresearch_unimi/conductor2pn
Camilli, M., Bellettini, C., Capra, L., Monga, M.: CTL model checking in the cloud using mapreduce. In: 2014 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 333–340, September 2014
Liang, H., Dong, J.S., Sun, J., Wong, W.E.: Software monitoring through formal specification animation. Innov. Syst. Softw. Eng. 5(4), 231–241 (2009)
Ramchandani, C.: Analysis of asynchronous concurrent systems by timed petri nets. Technical report, Cambridge, MA, USA (1974)
Lee, W.J., Cha, S.D., Kwon, Y.R.: Integration and analysis of use cases using modular petri nets in requirements engineering. IEEE Trans. Softw. Eng. 24(12), 1115–1130 (1998)
Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to petri nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 220–235. Springer, Heidelberg (2005). https://doi.org/10.1007/11538394_15
Montesi, F., Guidi, C., Lucchi, R., Zavattaro, G.: JOLIE: a java orchestration language interpreter engine. Electron. Notes Theor. Comput. Sci. 181, 19–33 (2007)
Fokkink, W.: Introduction to Process Algebra, 1st edn. Springer-Verlag, New York Inc., Secaucus (2000). https://doi.org/10.1007/978-3-662-04293-9. Ed. by W. Brauer, G. Rozenberg, and A. Salomaa
Bucchiarone, A., De Sanctis, M., Pistore, M.: Domain objects for dynamic and incremental service composition. In: Villari, M., Zimmermann, W., Lau, K.-K. (eds.) ESOCC 2014. LNCS, vol. 8745, pp. 62–80. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44879-3_5
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Camilli, M., Bellettini, C., Capra, L. (2018). Design-Time to Run-Time Verification of Microservices Based Applications. In: Cerone, A., Roveri, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10729. Springer, Cham. https://doi.org/10.1007/978-3-319-74781-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-74781-1_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-74780-4
Online ISBN: 978-3-319-74781-1
eBook Packages: Computer ScienceComputer Science (R0)