Skip to main content
SpringerLink
Log in

Formalizing Monitoring Processes for Large-Scale Distributed Systems Using Abstract State Machines

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10729))

Included in the following conference series:

  • 1939 Accesses

Abstract

Large-Scale Distributed Systems are characterized by high complexity and heterogeneity, which might lead to unexpected failures. The role of a robust monitoring framework is to gather low-level data and assess the status of the components of the system. The framework collaborates with adapters for ensuring steady recovery plans and improving the availability of services. Monitors, as part of the system, are also affected by unavailability or random failures. In order to increase the reliability of the solution we verify the trustworthiness of the monitors and emphasize the need of redundancy. This paper introduces a formal approach for modeling and verifying a monitoring solution for Large-Scale Distributed Systems. We formalize the behavior of the monitors with the aid of Abstract State Machines and employ the ASMETA toolset for simulating and analyzing properties of the model. The tool also supports the verification process by translating a simplified version of the model to an NuSMV specification, on top of which model checking can be applied. Properties of the model are expressed with the aid of computation tree logic.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 107.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Arcaini, P., Riccobene, E., Scandurra, P.: Modeling and analyzing MAPE-K feedback loops for self-adaptation. In: 2015 IEEE/ACM 10th International Symposium on Software Engineering for Adaptive and Self-managing Systems, pp. 13–23, May 2015

    Google Scholar 

  2. Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61–74. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_6

    Chapter  Google Scholar 

  3. Arcaini, P., Gargantini, A., Riccobene, E.: Automatic review of abstract state machines by meta property verification. In: Proceedings of Second NASA Formal Methods Symposium - NFM 2010, 13–15 April 2010, Washington D.C., USA, pp. 4–13 (2010)

    Google Scholar 

  4. Arcaini, P., Holom, R.-M., Riccobene, E.: ASM-based formal design of an adaptivity component for a cloud system. Form. Asp. Comput. 28(4), 567–595 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bianchi, A., Manelli, L., Pizzutilo, S.: An ASM-based model for grid job management. Informatica (Slovenia) 37(3), 295–306 (2013)

    Google Scholar 

  6. Bolis, F., Gargantini, A., Guarnieri, M., Magri, E., Musto, L.: Model-driven testing for web applications using abstract state machines. In: Grossniklaus, M., Wimmer, M. (eds.) ICWE 2012. LNCS, vol. 7703, pp. 71–78. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35623-0_7

    Chapter  Google Scholar 

  7. Börger, E., Stark, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, New York Inc., Secaucus (2003). https://doi.org/10.1007/978-3-642-18216-7

    Book  MATH  Google Scholar 

  8. Börger, E.: Modeling distributed algorithms by abstract state machines compared to petri nets. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 3–34. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_1

    Chapter  Google Scholar 

  9. Bósa, K., Holom, R.-M., Vleju, M.B.: A formal model of client-cloud interaction. In: Thalheim, B., Schewe, K.D., Prinz, A., Buchberger, B. (eds.) Correct Software in Web Applications and Web Services, pp. 83–144. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17112-8_4

    Chapter  Google Scholar 

  10. Buga, A., Nemes, S.T.: A formal approach for failure detection in large-scale distributed systems using abstract state machines. In: Benslimane, D., Damiani, E., Grosky, W.I., Hameurlain, A., Sheth, A., Wagner, R.R. (eds.) DEXA 2017. LNCS, vol. 10438, pp. 505–513. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-64468-4_38

    Chapter  Google Scholar 

  11. Buga, A., Nemes, S.T.: Towards modeling monitoring of smart traffic services in a large-scale distributed system. In: CLOSER 2017 - Proceedings of the 7th International Conference on Cloud Computing and Services Science, 24–26 April 2017, Porto, Portugal, pp. 455–462 (2017)

    Google Scholar 

  12. Buga, A., Nemes, S.T.: Towards modeling monitoring services for large-scale distributed systems with abstract state machines. In: Radar Track at the 22nd International Working Conference on Evaluation and Modeling Methods for Systems Analysis and Development (EMMSAD) Co-located with the 29th International Conference on Advanced Information Systems Engineering 2017 (CAiSE 2017), June 2017, Essen, Germany, vol. 1859. CEUR (2017)

    Google Scholar 

  13. Clayman, S., Galis, A., Mamatas, L.: Monitoring virtual networks with Lattice. In: Network Operations and Management Symposium Workshops (NOMS Wksps), pp. 239–246. IEEE/IFIP, April 2010

    Google Scholar 

  14. Fugini, M., Siadat, H.: SLA contract for cross-layer monitoring and adaptation. In: Rinderle-Ma, S., Sadiq, S., Leymann, F. (eds.) BPM 2009. LNBIP, vol. 43, pp. 412–423. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12186-9_39

    Chapter  Google Scholar 

  15. Kossak, F., Mashkoor, A.: How to select the suitable formal method for an industrial application: a survey. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 213–228. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_13

    Chapter  Google Scholar 

  16. Ma, H., Schewe, K.D., Wang, Q.: An abstract model for service provision, search and composition. In: 2009 IEEE Asia-Pacific Services Computing Conference (APSCC), pp. 95–102, December 2009

    Google Scholar 

  17. Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds.): Computer Aided Systems Theory - EUROCAST 2015. Lecture Notes in Computer Science, vol. 9520. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27340-2

    Google Scholar 

  18. Nemes, S.T., Buga, A.: Towards a case-based reasoning approach to dynamic adaptation for large-scale distributed systems. In: Aha, D.W., Lieber, J. (eds.) ICCBR 2017. LNCS (LNAI), vol. 10339, pp. 257–271. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61030-6_18

    Chapter  Google Scholar 

  19. Nemes, S.T., Buga, A.: Towards modeling adaptation services for large-scale distributed systems with abstract state machines. In: Proceedings of the Seventh International Symposium on Business Modeling and Software Design, BMSD, vol. 1, pp. 193–198. INSTICC, SciTePress (2017)

    Google Scholar 

  20. Németh, Z.N., Sunderam, V.: A formal framework for defining grid systems. In: 2002 14th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing, p. 202 (2002). http://dblp.uni-trier.de/rec/bibtex/conf/ccgrid/NemethS02

  21. Petcu, D., Crăciun, C., Neagul, M., Panica, S., Di Martino, B., Venticinque, S., Rak, M., Aversa, R.: Architecturing a sky computing platform. In: Cezon, M., Wolfsthal, Y. (eds.) ServiceWave 2010. LNCS, vol. 6569, pp. 1–13. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22760-8_1

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Christian Doppler Laboratory for Client-Centric Cloud Computing, Johannes Kepler University of Linz, Software Park 35, 4232, Hagenberg, Austria

    Andreea Buga & Sorana Tania Nemeș

Authors
  1. Andreea Buga
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sorana Tania Nemeș
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andreea Buga .

Editor information

Editors and Affiliations

  1. Nazarbayev University, Astana, Kazakhstan

    Antonio Cerone

  2. Fondazione Bruno Kessler, Povo, Italy

    Marco Roveri

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Buga, A., Nemeș, S.T. (2018). Formalizing Monitoring Processes for Large-Scale Distributed Systems Using Abstract State Machines. 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_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-74781-1_11

  • 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)

Publish with us

Policies and ethics

Search

Navigation