×

A formal approach to adaptive software: continuous assurance of non-functional requirements. (English) Zbl 1259.68123

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

MRMC; PRISM; JML
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] 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 (2006) Web services business process execution language version 2.0. OASIS Committee Draft, May 2006
[2] Avizienis A, Laprie J-C, Randell B, Landwehr CE (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Dependable Sec Comput 1(1): 11–33 · Zbl 05113026 · doi:10.1109/TDSC.2004.2
[3] Abreu J, Mazzanti F, Fiadeiro JL, Gnesi S (2009) A model-checking approach for service component architectures. In: FMOODS/FORTE, pp 219–224
[4] Blair G, Bencomo N, France RB (2009) Models@run.time. Computer 42(10): 22–27 · doi:10.1109/MC.2009.326
[5] Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Rustan K, Leino M, Poll E (2005) An overview of jml tools and applications. Int J Softw Tools Technol Transf 7: 212–232 · doi:10.1007/s10009-004-0167-4
[6] Barnett M, DeLine R, Fähndrich M, Jacobs B, Rustan K, Leino M, Schulte W, Venter H (2005) The spec# programming system: challenges and directions. In: VSTTE, pp 144–152
[7] Baresi L, Di Nitto E, Ghezzi C (2006) Toward open-world software: issue and challenges. Computer 39(10): 36–43 · Zbl 05332884 · doi:10.1109/MC.2006.362
[8] Bertolino A, Emmerich W, Inverardi P, Issarny V, Liotopoulos FK, Plaza P (2008) Plastic: providing lightweight & adaptable service technology for pervasive information & communication. In: ASE Workshops, pp 65–70
[9] Bézivin J (2006) Model driven engineering: an emerging technical space. In: Generative and Transformational Techniques in Software Engineering (GTTSE). LNCS, vol 4143. Springer, Berlin, pp 36–64
[10] Baier C, Haverkort B, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time markov chains. IEEE Trans Softw Eng 29: 524–541 · Zbl 05113886 · doi:10.1109/TSE.2003.1205180
[11] Baier C, Katoen J-P (2008) Principles of Model Checking. MIT Press, Cambridge · Zbl 1179.68076
[12] Belady LA, Lehman MM (1976) A model of large program development. IBM Syst J 15(3): 225–252 · Zbl 0329.68014 · doi:10.1147/sj.153.0225
[13] BPEL. http://www.oasis-open.org/
[14] Calinescu R (2009) General-purpose autonomic computing. In: Zhang Y, Yang LT, Denko MK (eds) Autonomic computing and networking. Springer, US, pp 3–30
[15] Cheng BHC, de Lemos R, Giese H, Inverardi P, Magee J (eds) (2009) Software Engineering for Self-Adaptive Systems [outcome of a Dagstuhl Seminar], Lecture Notes in Computer Science. vol 5525. Springer, Berlin
[16] Cavallaro L, Di Nitto E, Pelliccione P, Pradella M, Tivoli M (2010) Synthesizing adapters for conversational web-services from their wsdl interface. In: Proceedings of the 2010 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, SEAMS ’10. ACM, New York, pp 104–113
[17] Calinescu R, Grunske L, Kwiatkowska M, Mirandola R, Tamburrelli G Dynamic qos management and optimisation in service-based systems. IEEE Trans Softw Eng (to appear)
[18] Czarnecki K, Helsen S (2006) Feature-based survey of model transformation approaches. IBM Syst J 45(3): 621–646 · Zbl 05421244 · doi:10.1147/sj.453.0621
[19] Cheung RC (1980) A user-oriented software reliability model. IEEE Trans Softw Eng 6(2): 118–125 · Zbl 0432.68028 · doi:10.1109/TSE.1980.234477
[20] Calinescu R, Kwiatkowska M (2009) Using quantitative analysis to implement autonomic it systems. In: Proceedings of the 31st International Conference on Software Engineering (ICSE 2009), pp 100–110
[21] Di Nitto E, Ghezzi C, Metzger A, Papazoglou M, Pohl K (2008) A journey to highly dynamic, self-adaptive service-based applications. Autom Softw Eng 15(3-4): 313–341 · Zbl 05660991 · doi:10.1007/s10515-008-0032-x
[22] Epifani I, Ghezzi C, Mirandola R, Tamburrelli G (2009) Model evolution by run-time adaptation. In: Proceedings of the 31st International Conference on Software Engineering, IEEE Computer Society, pp 111–121
[23] Epifani I, Ghezzi C, Tamburrelli G (2010) Change-point detection for black-box services. In: Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, FSE ’10. ACM, New York, pp 227–236
[24] Fähndrich M, Barnett M, Logozzo F (2010) Embedded contract languages. In: SAC, pp 2103–2110
[25] Filieri A, Ghezzi C, Tamburrelli G (2011) Run-time efficient probabilistic model checking. In: Proceedings of the 33rd International Conference on Software Engineering (to appear)
[26] Gelman A (2004) Bayesian data analysis. CRC press, West Palm Beach · Zbl 1117.62343
[27] Gallotti S, Ghezzi C, Mirandola R, Tamburrelli G (2008) Quality prediction of service compositions through probabilistic model checking. In: QoSA ’08: Proceedings of the 4th International Conference on the Quality of Software Architectures, Karlsruhe, Germany
[28] Ghezzi C, Motta A, Panzica La Manna V, Tamburrelli G (2010) Qos driven dynamic binding in-the-many. In: Sixth International Conference on the Quality of Software Architectures, QoSA 2010
[29] Goseva-Popstojanova K, Trivedi KS (2001) Architecture-based approach to reliability assessment of software systems. Perform Eval 45(2-3): 179–204 · Zbl 1014.68018 · doi:10.1016/S0166-5316(01)00034-7
[30] Grunske L (2008) Specification patterns for probabilistic quality properties. In: Robby (ed) ICSE. ACM, pp 31–40
[31] Ghezzi C, Tamburrelli G (2009) Reasoning on Non-Functional Requirements for Integrated Services. In: Proceedings of the 17th International Requirements Engineering Conference. IEEE Computer Society, pp 69–78
[32] Ghezzi C, Tamburrelli G (2009) Predicting performance properties for open systems with KAMI. In: QoSA ’09: Proceedings of the 5th International Conference on the Quality of Software Architectures. Springer-Verlag, Berlin, pp 70–85
[33] Guide MU (1998) The mathworks. Inc., Natick, MA, 5
[34] Hellerstein JL (2004) Self-managing systems: a control theory foundation. In: Local Computer Networks, vol 0. Annual IEEE Conference, pp 708–708
[35] Hahn E, Hermanns H, Zhang L (2009) Probabilistic reachability for parametric markov models. In: Model Checking Software, pp 88–106
[36] Hinton A, Kwiatkowska M, Norman G, Parker D (2006) 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
[37] Huebscher MC, McCann JA (2008) A survey of autonomic computing–degrees, models, and applications. ACM Comput Surv 40(3):1–28. http://dl.acm.org/citation.cfm?id=1380585
[38] Immonen A, Niemela E (2008) Survey of reliability and availability prediction methods from the viewpoint of software architecture. Softw Syst Model 7(1): 49–65 · Zbl 05348737 · doi:10.1007/s10270-006-0040-x
[39] Jackson M, Zave P (1995) Deriving specifications from requirements: an example. In: ICSE ’95: Proceedings of the 17th international conference on Software engineering. ACM, New York, pp 15–24
[40] Kephart JO, Chess DM (2003) The vision of autonomic computing. COMPUTER, pp 41–50
[41] Katoen J-P, Kwiatkowska M, Norman G, Parker D (2001) Faster and symbolic ctmc model checking. In: de Alfaro L, Gilmore S (eds) Process Algebra and Probabilistic Methods. Performance Modelling and Verification, vol 2165. Lecture Notes in Computer Science. Springer, Berlin, pp 23–38 · Zbl 1007.68517
[42] Kramer J, Magee J (1990) The evolving philosophers problem: dynamic change management. IEEE Trans Softw Eng 16: 1293–1306 · Zbl 05114666 · doi:10.1109/32.60317
[43] Kramer J, Magee J (2007) Self-managed systems: an architectural challenge. In: Future of Software Engineering, pp 259–268
[44] Kwiatkowska M, Norman G, Parker D (2004) Prism 2.0: a tool for probabilistic model checking. In: Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings. First International Conference, pp 322–323
[45] Kwiatkowska MZ, Norman G, Parker D (2007) Stochastic model checking. In: SFM, pp 220–270 · Zbl 1323.68379
[46] Kwiatkowska M, Parker D, Qu H (2011) Incremental quantitative verificat ion for markov decision processes. (unpublished–submitted for publication)
[47] Kihl M, Robertsson A, Andersson M, Wittenmark B (2007) Control-theoretic analysis of admission control mechanisms for web server systems. World Wide Web J Springer 11(1-2008):93–116
[48] Kozine IO, Utkin LV (2002) Interval-valued finite markov chains. Reliab Comput 8:97–113 · Zbl 1001.65007
[49] Katoen J-P, Zapreev IS, Hahn EM, Hermanns H, Jansen DN (2010) The ins and outs of the probabilistic model checker mrmc. In: Performance Evaluation, Corrected Proof:–2010 (in Press)
[50] Lehman MM, Belady LA (eds) (1985) Program evolution: processes of software change. Academic Press, London
[51] Lehman MM (1980) On understanding laws, evolution, and conservation in the large-program life cycle. J Syst Softw 1: 213–221 · Zbl 05433254 · doi:10.1016/0164-1212(79)90022-0
[52] Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Program 78(5): 293–303 · Zbl 1192.68433 · doi:10.1016/j.jlap.2008.08.004
[53] Meyer B (2007) Contract-driven development. In: FASE
[54] Maggio M, Hoffmann H, Santambrogio MD, Agarwal A, Leva A (2010) Controlling software applications via resource allocation within the heartbeats framework. In: CDC, pp 3736–3741
[55] Ng KW, Tian GL, Tang ML (2011) Dirichlet and Related Distributions: Theory, Methods and Applications. Wiley Series in Probability and Statistics. Wiley, New York
[56] OpenID. http://www.openid.com
[57] Pezze M, Young M (2005) Software testing and analysis: process, principles and techniques. Wiley, New York
[58] Ross SM (1996) Stochastic processes. Wiley, New York · Zbl 0888.60002
[59] Skene J, Lamanna DD, Emmerich W (2004) Precise service level agreements. In: Proc. of 26th Intl. Conference on Software Engineering (ICSE). IEEE Press, USA, pp 179–188
[60] Salehie M, Tahvildari L (2009) Self-adaptive software: landscape and research challenges. TAAS 4(2):1–42. http://dl.acm.org/citation.cfm?id=1516533.1516538
[61] ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2007) An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: FMICS, pp 133–148
[62] Vandewoude Y, Ebraert P, Berbers Y, D’Hondt T (2007) Tranquility: a low disruptive alternative to quiescence for ensuring safe dynamic updates. IEEE Trans Softw Eng 33(12):856–868
[63] van Lamsweerde A (2009) Requirements engineering: from System goals to UML models to software specifications. Wiley, New York
[64] WSDL. http://www.w3.org/2002/ws/desc
[65] Zhang J, Cheng BHC (2006) Model-based development of dynamically adaptive software. In: ICSE, ACM, New York, pp 371–380
[66] Zave P, Jackson M (1997) Four dark corners of requirements engineering. ACM Trans Softw Eng Methodol 6(1): 1–30 · Zbl 01936070 · doi:10.1145/237432.237434
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.