A formal approach to adaptive software: continuous assurance of non-functional requirements

Formal Aspects of Computing - Tập 24 Số 2 - Trang 163-186 - 2012
Antonio Filieri1, Carlo Ghezzi1, Giordano Tamburrelli1
1DEI, Politecnico di Milano, DeepSE Group, Piazza L. da Vinci, 32, 20133, Milan, Italy

Tóm tắt

Abstract Modern software systems are increasingly requested to be adaptive to changes in the environment in which they are embedded. Moreover, adaptation often needs to be performed automatically, through self-managed reactions enacted by the application at run time. Off-line, human-driven changes should be requested only if self-adaptation cannot be achieved successfully. To support this kind of autonomic behavior, software systems must be empowered by a rich run-time support that can monitor the relevant phenomena of the surrounding environment to detect changes, analyze the data collected to understand the possible consequences of changes, reason about the ability of the application to continue to provide the required service, and finally react if an adaptation is needed. This paper focuses on non-functional requirements, which constitute an essential component of the quality that modern software systems need to exhibit. Although the proposed approach is quite general, it is mainly exemplified in the paper in the context of service-oriented systems, where the quality of service (QoS) is regulated by contractual obligations between the application provider and its clients. We analyze the case where an application, exported as a service, is built as a composition of other services. Non-functional requirements—such as reliability and performance—heavily depend on the environment in which the application is embedded. Thus changes in the environment may ultimately adversely affect QoS satisfaction. We illustrate an approach and support tools that enable a holistic view of the design and run-time management of adaptive software systems. The approach is based on formal (probabilistic) models that are used at design time to reason about dependability of the application in quantitative terms. Models continue to exist at run time to enable continuous verification and detection of changes that require adaptation.

Từ khóa


Tài liệu tham khảo

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

10.1109/TDSC.2004.2

Abreu J Mazzanti F Fiadeiro JL Gnesi S (2009) A model-checking approach for service component architectures. In: FMOODS/FORTE pp 219–224

10.1109/MC.2009.326

10.1007/s10009-004-0167-4

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

10.1109/MC.2006.362

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

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.1109/TSE.2003.1205180

Baier C, 2008, Principles of Model Checking

10.1147/sj.153.0225

BPEL. http://www.oasis-open.org/

Calinescu R (2009) General-purpose autonomic computing. In: Zhang Y Yang LT Denko MK (eds) Autonomic computing and networking. Springer US pp 3–30

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

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

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)

10.1147/sj.453.0621

10.1109/TSE.1980.234477

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

10.1007/s10515-008-0032-x

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

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

Fähndrich M Barnett M Logozzo F (2010) Embedded contract languages. In: SAC pp 2103–2110

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)

Gelman A, 2004, Bayesian data analysis

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

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

10.1016/S0166-5316(01)00034-7

Grunske L (2008) Specification patterns for probabilistic quality properties. In: Robby (ed) ICSE. ACM pp 31–40

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

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

Guide MU (1998) The mathworks. Inc. Natick MA 5

Hellerstein JL (2004) Self-managing systems: a control theory foundation. In: Local Computer Networks vol 0. Annual IEEE Conference pp 708–708

Hahn E Hermanns H Zhang L (2009) Probabilistic reachability for parametric markov models. In: Model Checking Software pp 88–106

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

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

10.1007/s10270-006-0040-x

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

Kephart JO Chess DM (2003) The vision of autonomic computing. COMPUTER pp 41–50

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

10.1109/32.60317

Kramer J Magee J (2007) Self-managed systems: an architectural challenge. In: Future of Software Engineering pp 259–268

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

Kwiatkowska MZ Norman G Parker D (2007) Stochastic model checking. In: SFM pp 220–270

Kwiatkowska M Parker D Qu H (2011) Incremental quantitative verificat ion for markov decision processes. (unpublished—submitted for publication)

Kihl M, 2007, Control-theoretic analysis of admission control mechanisms for web server systems, World Wide Web J Springer, 11, 93, 10.1007/s11280-007-0030-0

10.1023/A:1014745904458

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)

Lehman MM Belady LA (eds) (1985) Program evolution: processes of software change. Academic Press London

10.1016/0164-1212(79)90022-0

10.1016/j.jlap.2008.08.004

Meyer B (2007) Contract-driven development. In: FASE

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

Ng KW Tian GL Tang ML (2011) Dirichlet and Related Distributions: Theory Methods and Applications. Wiley Series in Probability and Statistics. Wiley New York

OpenID. http://www.openid.com

Pezze M, 2005, Software testing and analysis: process, principles and techniques

Ross SM, 1996, Stochastic processes

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

10.1145/1516533.1516538

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

10.1109/TSE.2007.70733

van Lamsweerde A, 2009, Requirements engineering: from System goals to UML models to software specifications

WSDL. http://www.w3.org/2002/ws/desc

Zhang J Cheng BHC (2006) Model-based development of dynamically adaptive software. In: ICSE ACM New York pp 371–380

10.1145/237432.237434

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Tập 24 Số 2

163-186

Thông tin tác giả