nach oben

Erschienen in:

2012 | OriginalPaper | Buchkapitel

12. Conquering Complexity via Seamless Integration of Design-Time and Run-Time Verification

verfasst von : Antonio Filieri, Carlo Ghezzi, Raffaela Mirandola, Giordano Tamburrelli

Erschienen in: Conquering Complexity

Verlag: Springer London

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The complexity of modern software systems has grown enormously in the past years with users always demanding for new features and better quality of service. Software applications evolved not only in terms of size, but also in the criticality of the services supported. At the same time, software artifacts changed from being monolithic and centralized to modular, distributed, and dynamic. Systems are now composed of heterogeneous components and infrastructures on which software is configured and deployed. Interactions with the external environment and the structure of the application, in terms of components and interconnections, are often required to change dynamically. All these causes challenge our ability to achieve acceptable levels of dependability. To guarantee system dependability, it is necessary to combine off-line (development-time) analysis techniques with run-time mechanisms for continuous verification. Off-line verification checks the correct behavior of the various components of the application under given assumptions on the embedding environment. But because verification can be incomplete, the assumptions about reality it relies upon are subject to uncertainty and variability and, in addition, the various parts of a complex system may evolve independently, it is necessary to extend verification to also cope with the runtime behavior of software. This paper motivates the need for continuous verification to guarantee dependability and shows how this goal may be tackled. In particular, it focuses attention on two important dependability attributes: reliability and performance.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Ten Commandments of Formal Methods… Ten Years On

Nächstes Kapitel Modelling Temporal Behaviour in Complex Systems with Timebands

Nur mit Berechtigung zugänglich

http://www.dependability.org/wg10.4/.

The OASIS website is here: http://www.oasis-open.org.

Alves, A., Arkin, A., Askary, S., Bloch, B., Curbera, F., Goland, Y., Kartha, N., Sterling, König, D., Mehta, V., Thatte, S., van der Rijn, D., Yendluri, P., Yiu, A.: Web services business process execution language version 2.0. OASIS Committee Draft (2006)

Ardagna, D., Ghezzi, C., Mirandola, R.: Rethinking the use of models in software architecture. In: 4th International Conference on the Quality of Software-Architectures, QoSA 2008. LNCS, vol. 5281, pp. 1–27. Springer, Berlin (2008)

Ardagna, D., Mirandola, R.: Per-flow optimal service selection for web services based processes. J. Syst. Softw. 83(8), 1512–1523 (2010) CrossRef

Aziz, A., Singhal, V., Balarin, F.: It usually works: the temporal logic of stochastic systems. In: Wolper, P. (ed.) Proc. 7th International Conference on Computer Aided Verification, CAV 95. LNCS, vol. 939, pp. 155–165. Springer, Berlin (1995)

Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) Proc. 10th International Conference on Concurrency Theory, CONCUR 99. LNCS, vol. 1664, pp. 146–161. Springer, Berlin (1999)

Balsamo, S., Di Marco, A., Inverardi, P., Simeoni, M.: Model-based performance prediction in software development: a survey. IEEE Trans. Softw. Eng. 30(5), 295–310 (2004) CrossRef

Baresi, L., Bianculli, D., Ghezzi, C., Guinea, S., Spoletini, P.: Validation of web service compositions. IET Softw. 1(6), 219–232 (2007) CrossRef

Baresi, L., Di Nitto, E., Ghezzi, C.: Toward open-world software: issue and challenges. Computer 39(10), 36–43 (2006) CrossRef

Baresi, L., Ghezzi, C., Guinea, S.: Smart monitors for composed services. In: Proceedings of the 2nd International Conference on Service Oriented Computing, ICSOC ’04, pp. 193–202. ACM, New York (2004) CrossRef

10.

Baskett, F., Chandy, K.M., Muntz, R.R., Palacios, F.G.: Open, closed, and mixed networks of queues with different classes of customers. J. ACM 22(2), 248–260 (1975) CrossRefMathSciNetMATH

11.

Becker, S., Grunske, L., Mirandola, R., Overhage, S.: Performance prediction of component-based systems—a survey from an engineering perspective. In: Architecting Systems with Trustworthy Components. LNCS, vol. 3938, pp. 169–192. Springer, Berlin (2006) CrossRef

12.

Becker, S., Koziolek, H., Reussner, R.: Model-based performance prediction with the Palladio component model. In: WOSP ’07: Proceedings of the 6th International Workshop on Software and Performance, pp. 54–65. ACM, New York (2007) CrossRef

13.

Bernardi, S., Merseguer, J., Petriu, D.: Adding dependability analysis capabilities to the MARTE profile. In: Model Driven Engineering Languages and Systems, Proceedings 11th International Conference, MoDELS 2008, Toulouse, France, September 28–October 3, 2008. LNCS, vol. 5301, pp. 736–750. Springer, Berlin (2008) CrossRef

14.

Bertoli, M., Casale, G., Serazzi, G.: The JMT simulator for performance evaluation of non-product-form queueing networks. In: Annual Simulation Symposium, pp. 3–10. IEEE Computer Society, Norfolk (2007)

15.

Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. Wiley-Interscience, New York (1998) CrossRefMATH

16.

Brooks, F.P.: The Mythical Man-Month: Essays on Software Engineering. Pearson Education, London (1975)

17.

Calinescu, R.: General-purpose autonomic computing. In: Denko, M.K., Yang, L.T., Zhang, Y. (eds.) Autonomic Computing and Networking, pp. 3–30. Springer, Berlin (2009) CrossRef

18.

Calinescu, R., Kwiatkowska, M.: Using quantitative analysis to implement autonomic it systems. In: ICSE ’09: Proceedings of the 31st International Conference on Software Engineering, pp. 100–110. IEEE Computer Society, Washington (2009)

19.

Canfora, G., Di Penta, M., Esposito, R., Villani, M.L.: A framework for QoS-aware binding and re-binding of composite web services. J. Syst. Softw. 81(10), 1754–1769 (2008) CrossRef

20.

Caporuscio, M., Funaro, M., Ghezzi, C.: Architectural issues of adaptive pervasive systems. In: Graph Transformations and Model-Driven Engineering, pp. 492–511 (2010) CrossRef

21.

Cardellini, V., Casalicchio, E., Grassi, V., Lo Presti, F., Mirandola, R.: QoS-driven runtime adaptation of service oriented architectures. In: Proceedings ESEC/FSE 2009, pp. 131–140. ACM, New York (2009) CrossRef

22.

Casale, G., Muntz, R., Serazzi, G.: Geometric bounds: a noniterative analysis technique for closed queueing networks. IEEE Trans. Comput. 57(6), 780–794 (2008) CrossRefMathSciNet

23.

Cavallaro, L., Di Nitto, E., Pelliccione, P., Pradella, M., Tivoli, M.: Synthesizing adapters for conversational web-services from their WSDL interface. In: ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, SEAMS ’10, pp. 104–113. ACM, New York (2010)

24.

Chafle, G., Doshi, P., Harney, J., Mittal, S., Srivastava, B.: Improved adaptation of web service compositions using value of changed information. In: ICWS, pp. 784–791. IEEE Comput. Soc., Los Alamitos (2007)

25.

Cheng, B., de Lemos, R., Giese, G., Inverardi, P., Magee, J. (eds.): Software Engineering for Self-Adaptive Systems [outcome of a Dagstuhl Seminar]. LNCS, vol. 5525. Springer, Berlin (2009)

26.

Clark, A., Gilmore, S., Hillston, J., Tribastone, M.: Stochastic process algebras. In: 7th Intern. School on Formal Methods, SFM. LNCS, vol. 4486, pp. 132–179. Springer, Berlin (2007)

27.

Di Nitto, E., Ghezzi, C., Metzger, A., Papazoglou, M.P., Pohl, K.: A journey to highly dynamic, self-adaptive service-based applications. Autom. Softw. Eng. 15(3–4), 313–341 (2008) CrossRef

28.

Dwyer, M.B., Avrunin, J.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. 21th International Conference on Software Engineering (ICSE99), pp. 411–420. ACM, New York (1999)

29.

Epifani, I., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Model evolution by run-time parameter adaptation. In: Proc. 31st International Conference on Software Engineering (ICSE09), pp. 111–121. IEEE Comput. Soc., Los Alamitos (2009)

30.

Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Taylor, R.N., Gall, H., Medvidovic, N. (eds.) ICSE, pp. 341–350 (2011)

31.

Gallotti, S., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Quality prediction of service compositions through probabilistic model checking. In: QoSA, Quality of Software Architecture. LNCS. Springer, Berlin (2008)

32.

Garlan, D., Cheng, S.-W., Huang, A.C., Schmerl, B., Steenkiste, P.: Rainbow: architecture-based self-adaptation with reusable infrastructure. IEEE Comput. 37(10), 46–54 (2004) CrossRef

33.

Ghezzi, C., Guinea, S.: Run-time monitoring in service-oriented architectures. In: Test and Analysis of Web Services, pp. 237–264. Springer, Berlin (2007) CrossRef

34.

Ghezzi, C., Motta, A., Manna, V.P.L., Tamburrelli, G.: QoS driven dynamic binding in-the-many. In: Heineman, G.T., Kofron, J., Plasil, F. (eds.) Research into Practice—Reality and Gaps, 6th International Conference on the Quality of Software Architectures, QoSA 2010, Prague, Czech Republic, June 23–25, 2010, pp. 68–83. Springer, Berlin (2010)

35.

Ghezzi, C., Tamburrelli, G.: Reasoning on non-functional requirements for integrated services. In: RE ’09: Proceedings of the 17th International Conference on Requirements Engineering, Atlanta, USA (2009)

36.

Grassi, V.: Architecture-based reliability prediction for service-oriented computing. In: Workshop on Architecting Dependable Systems, WADS. LNCS, vol. 3549, pp. 279–299. Springer, Berlin (2004) CrossRef

37.

Gruhn, V., Laue, R.: Patterns for timed property specifications. Electron. Notes Theor. Comput. Sci. 153(2), 117–133 (2006) CrossRef

38.

Grunske, L.: Specification patterns for probabilistic quality properties. In: Robbie (ed.) 30th International Conference on Software Engineering (ICSE 2008), pp. 31–40. ACM, New York (2008)

39.

Guo, H., Huai, J., Li, H., Deng, T., Li, Y., Du, Z.: ANGEL: optimal configuration for high available service composition. In: IEEE International Conference on Web Services (ICWS 2007), pp. 280–287. IEEE Comput. Soc., Los Alamitos (2007) CrossRef

40.

Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994) CrossRefMATH

41.

Harney, J., Doshi, P.: Speeding up adaptation of web service compositions using expiration times. In: World Wide Web (WWW), pp. 1023–1032. ACM, New York (2007)

42.

Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: Prism: a tool for automatic verification of probabilistic systems. In: Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), vol. 3920, pp. 441–444 (2006) CrossRef

43.

Immonen, A., Niemelä, E.: Survey of reliability and availability prediction methods from the viewpoint of software architecture. Softw. Syst. Model. 7(1), 49–65 (2008) CrossRef

44.

Jain, R.: The Art of Computer Systems Performance Analysis—Techniques for Experimental Design, Measurement, Simulation, and Modeling. Wiley-Interscience, New York (1991) MATH

45.

Katoen, J.-P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems TACAS 2007, Proceedings. LNCS, vol. 4424, pp. 87–101. Springer, Berlin (2007) CrossRef

46.

Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243–244. IEEE Comput. Soc., Los Alamitos (2005)

47.

Kephart, J.O., Chess, D.M.: The vision of autonomic computing. IEEE Comput. 36(1), 41–50 (2003) CrossRef

48.

Kerola, T.: The composite bound method for computing throughput bounds in multiple class environments. Perform. Eval. 6(1), 1–9 (1986) CrossRefMathSciNet

49.

Konrad, S., Cheng, B.: Real-time specification patterns. In: Roman, G.-C., Griswold, W.G., Nuseibeh, B. (eds.) 27th International Conference on Software Engineering (ICSE 05), pp. 372–381. ACM, New York (2005) CrossRef

50.

Kramer, J., Magee, J.: The evolving philosophers problem: dynamic change management. IEEE Trans. Softw. Eng. 16, 1293–1306 (1990) CrossRef

51.

Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pp. 449–458. ACM Press, New York (2007) CrossRef

52.

Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Int. J. Softw. Tools Technol. Transf. 6(2), 128–142 (2004) CrossRef

53.

Kwiatkowska, M.Z., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, Proceedings 18th International Conference, CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Berlin (2006)

54.

Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Form. Methods Syst. Des. 29(1), 33–78 (2006) CrossRefMATH

55.

Lazowska, E.D., Zahorjan, J., Graham, G.S., Sevcik, K.C.: Quantitative System Performance: Computer System Analysis Using Queueig Network Models. Prentice Hall, New York (1984)

56.

Maoz, S.: Using model-based traces as runtime models. IEEE Comput. 42(10), 28–36 (2009) CrossRef

57.

Marsan, M.A.: Stochastic petri nets: an elementary introduction. In: Advances in Petri Nets, pp. 1–29. Springer, Berlin (1989)

58.

Martens, A., Koziolek, H., Becker, S., Reussner, R.: Automatically improve software architecture models for performance, reliability, and cost using evolutionary algorithms. In: 1st Joint WOSP/SIPEW International Conference on Performance Engineering, pp. 105–116. ACM, New York (2010) CrossRef

59.

Marzolla, M., Mirandola, R.: Performance aware reconfiguration of software systems. In: Computer Performance Engineering—Proceedings 7th European Performance Engineering Workshop, EPEW 2010, Bertinoro, Italy, September 23–24, 2010. LNCS, vol. 6342, pp. 51–66. Springer, Berlin (2010)

60.

Menascé, D.A., Ewing, J.M., Gomaa, H., Malek, S., Sousa, J.P.: A framework for utility-based service oriented design in sassy. In: Proc. First Joint WOSP/SIPEW Int. Conf. on Performance Engineering, pp. 27–36. ACM, New York (2010) CrossRef

61.

Morin, B., Barais, O., Jézéquel, J.-M., Fleurey, F., Solberg, A.: Models@ run.time to support dynamic adaptation. IEEE Comput. 42(10), 44–51 (2009) CrossRef

62.

Puterman, M.L.: Markov Decision Processes. Wiley, New York (1994) CrossRefMATH

63.

Raimondi, F., Skene, J., Emmerich, W.: Efficient online monitoring of web-service slas. In: SIGSOFT FSE, pp. 170–180. ACM, New York (2008)

64.

Ross, S.M.: Stochastic Processes. Wiley, New York (1996) MATH

65.

Salehie, M., Li, S., Asadollahi, R., Tahvildari, L.: Change support in adaptive software: a case study for fine-grained adaptation. In: EASE ’09: Proc. Sixth IEEE Conf. and Workshops on Engineering of Autonomic and Autonomous Systems, pp. 35–44. IEEE Comput. Soc., Washington (2009) CrossRef

66.

Sato, N., Trivedi, K.S.: Stochastic modeling of composite web services for closed-form analysis of their performance and reliability bottlenecks. In: ICSOC. LNCS, vol. 4749, pp. 107–118. Springer, Berlin (2007)

67.

Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification. LNCS, vol. 3576, pp. 266–280. Springer, Berlin (2005) CrossRef

68.

Taylor, R.N., Medvidovic, N., Oreizy, P.: Architectural styles for runtime software adaptation. In: WICSA/ECSA, pp. 171–180. IEEE Press, New York (2009)

69.

Vandewoude, Y., Ebraert, P., Berbers, Y., D’Hondt, T.: Tranquility: a low disruptive alternative to quiescence for ensuring safe dynamic updates. IEEE Trans. Softw. Eng. 33(12), 856–868 (2007) CrossRef

70.

Wang, L., Dingle, N.J., Knottenbelt, W.J.: Natural language specification of performance trees. In: Thomas, N., Juiz, C. (eds.) Proceedings of the 5th European Performance Engineering Workshop, EPEW 2008. LNCS, vol. 5261, pp. 141–151 (2008)

71.

WOSP International Workshops on Software and Performance. ACM, New York (1998–2008)

72.

Zeng, L., Benatallah, B., Ngu, A.H., Dumas, M., Kalagnanam, J., Chang, H.: QoS-aware middleware for web services composition. IEEE Trans. Softw. Eng. 30(5), 311–327 (2004) CrossRef

73.

Zheng, T., Woodside, M., Litoiu, M.: Performance model estimation and tracking using optimal filters. IEEE Trans. Softw. Eng. 34(3), 391–406 (2008) CrossRef

Titel: Conquering Complexity via Seamless Integration of Design-Time and Run-Time Verification
verfasst von: Antonio Filieri
Carlo Ghezzi
Raffaela Mirandola
Giordano Tamburrelli
Verlag: Springer London
Buch: Conquering Complexity
Print ISBN: 978-1-4471-2296-8

Electronic ISBN: 978-1-4471-2297-5

Copyright-Jahr: 2012
DOI: https://doi.org/10.1007/978-1-4471-2297-5_12

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner