skip to main content
research-article
Free Access

Self-adaptive software needs quantitative verification at runtime

Published:01 September 2012Publication History
Skip Abstract Section

Abstract

Continually verify self-adaptation decisions taken by critical software in response to changes in the operating environment.

References

  1. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhotak, O., de Moor, O., Sereni, D., Sittampalam, G., and Tibble, J. Adding trace matching with free variables to AspectJ. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (San Diego, Oct. 16--20). ACM Press, New York, 2005, 345--364. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. Barringer, H. and Havelund, K. A Scala DSL for trace analysis. In FM 2011: Formal Methods, Volume 6664 of Lecture Notes in Computer Science, M. Butler and W. Schulte, Eds. Springer, Berlin/Heidelberg, 2011, 57--72. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Barringer, H., Havelund, K., Rydeheard, D., and Groce, A. Rule systems for runtime verification: A short tutorial. In Run-time Verification, Volume 5779 of Lecture Notes in Computer Science, S. Bensalem and D. Peled, Eds. Springer, Berlin/Heidelberg, 2009, 1--24. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Brun, Y., Di Marzo Serugendo, G., Gacek, C., Giese, H., Kienle, H.M., Litoiu, M., Muller, H.A., Pezze, M., and Shaw, M. Engineering self-adaptive systems through feedback loops. In Software Engineering for Self-Adaptive Systems, Volume 5525 of Lecture Notes in Computer Science. Springer, Berlin/Heidelberg, 2009, 48--70. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., and Tamburrelli, G. Dynamic QoS management and optimization in service-based systems. IEEE Transactions on Software Engineering 37, 3 (May--June 2011), 387--409. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Calinescu, R., Johnson, K., and Rafiq, Y. Using observation ageing to improve Markovian model learning in QoS engineering. In Proceedings of the second ACM/SPEC International Conference on Performance Engineering (Karlsruhe, Germany, Mar. 14--16). ACM Press, New York, 2011, 505--510. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Calinescu, R. and Kwiatkowska, M. CADS*: Computer-aided development of self-* systems. In Fundamental Approaches to Software Engineering, Volume 5503 of Lecture Notes in Computer Science, M. Chechik and M. Wirsing, Eds. Springer, Berlin/Heidelberg, 2009, 421--424. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Calinescu, R. and Kwiatkowska, M. Using quantitative analysis to implement autonomic IT systems. In Proceedings of the 31st International Conference on Software Engineering (Vancouver, Canada, May 16--24). IEEE Computer Society Press, Washington, D.C., 2009, 100--110. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Cheng, B.H. et al. Software engineering for self-adaptive systems: A research roadmap. In Software Engineering for Self-Adaptive Systems, B.H. Cheng, R. Lemos, H. Giese, P. Inverardi, and J. Magee, Eds. Springer-Verlag, Berlin/Heidelberg, 2009, 1--26. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Clarke. E.M. and Lerda, F. Model checking: Software and beyond. Journal of Universal Computer Science 13, 5 (May 2007), 639--649.Google ScholarGoogle Scholar
  11. Crow, J. and Rushby, J. Model-Based Reconfiguration: Diagnosis and Recovery. NASA Contractor Report 4596. NASA Langley Research Center, Hampton, VA, May 1994; work performed by SRI International. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Epifani, I., Ghezzi, C., Mirandola, R., and Tamburrelli, G. Model evolution by run-time adaptation. In Proceedings of the 31st International Conference on Software Engineering (Vancouver, Canada, May 16--24). IEEE Computer Society Press, Washington, D.C., 2009, 111--121. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Filieri, A., Ghezzi, C., and Tamburrelli, G. Run-time efficient probabilistic model checking. In Proceedings of the 33rd International Conference on Software Engineering (Honolulu, May 21--28). IEEE Computer Society Press, New York, 2011, 341--350. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Floch, J., Hallsteinsen, S., Stav, E., Eliassen, F., Lund, K., and Gjorven, E. Using architecture models for runtime adaptability. IEEE Software 23, 2 (Mar. 2006), 62--70. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. Garlan, D. and Schmerl, B.R. Using architectural models at runtime: Research challenges. In Proceedings of the first European Workshop on Software Architecture, Volume 3047 of Lecture Notes in Computer Science, F. Oquendo, B. Warboys, and R. Morrison, Eds. (St. Andrews, Scotland, May 21--22). Springer-Verlag, Berlin/Heidelberg, 2004, 200--205.Google ScholarGoogle Scholar
  16. Ghezzi, C., Mocci, A., and Monga, M. Synthesizing intensional behavior models by graph transformation. In Proceedings of the 31st International Conference on Software Engineering (Vancouver, Canada, May 16--24). IEEE Computer Society, Washington, D.C., 2009, 430--440. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Ghezzi, C., Mocci, A., and Salvaneschi, G. Automatic cross-validation of multiple specifications: A case study. In Proceedings of Fundamental Approaches to Software Engineering, Volume 6013 of Lecture Notes in Computer Science. Springer, Berlin/Heidelberg, 2010, 233--247. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Hinton, A., Kwiatkowska, M., Norman, G., and Parker, D. PRISM: A tool for automatic verification of probabilistic systems. In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Volume 3920 of Lecture Notes in Computer Science, H. Hermanns and J. Palsberg, Eds. Springer, Berlin/Heidelberg, 2006, 441--444. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Huebscher, M.C. and McCann, J.A. A survey of autonomic computing: Degrees, models, and applications. ACM Computing Surveys 40, 3 (Aug. 2008), 1--28. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Kephart, J.O. and Chess, D.M. The vision of autonomic computing. Computer 36, 1 (Jan. 2003), 41--50. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Kwiatkowska, M. Quantitative verification: Models, techniques, and tools. In Proceedings of the Sixth Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium Foundations of Software Engineering (Dubrovnik, Croatia, Sept. 3--7). ACM Press, New York, 2007, 449--458. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Kwiatkowska, M., Parker, D., and Qu, H. Incremental quantitative verification for Markov decision processes. In Proceedings of the 2011 IEEE/IFIP International Conference on Dependable Systems and Networks (Hong Kong, June 27--30). IEEE Computer Society, Los Alamitos, CA, 2011, 359--370. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Kyas, M., Prisacariu, C., and Schneider, G. Run-time monitoring of electronic contracts. In Proceedings of the Sixth International Symposium on Automated Technology for Verification and Analysis (Seoul, Oct. 20--23). Springer-Verlag, Berlin/Heidelberg, 2008, 397--407. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Lehman, M.M. and Belady, L.A., Eds. Program Evolution: Processes of Software Change. Academic Press Professional, Inc., San Diego, 1985. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. Leucker, M. and Schallhart, C. A brief account of runtime verification. Journal of Logic and Algebraic Programming 78, 5 (May 2009), 293--303.Google ScholarGoogle ScholarCross RefCross Ref
  26. Morin, B., Barais, O., Jezequel, J.-M., Fleurey, F., and Solberg, A. [email protected] to support dynamic adaptation. Computer 42, 10 (Oct. 2009), 44--51. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Pnueli, A. and Zaks, A. PSL model checking and runtime verification via testers. In Proceedings of the 14th International Symposium on Formal Methods (Hamilton, Canada, Aug. 21--27). Springer-Verlag, Berlin/Heidelberg, 2006, 573--586. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Rao, J. and Su, X. A survey of automated Web service composition methods. In Semantic Web Services and Web Process Composition, Volume 3387 of Lecture Notes in Computer Science, J. Cardoso and A. Sheth, Eds. Springer, Berlin/Heidelberg, 2005, 43--54. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Rushby, J.M. Runtime certification. In Proceedings of the Eighth International Workshop on Runtime Verification, Volume 5289 of Lecture Notes in Computer Science, M. Leucker, Ed. (Budapest, Mar. 30). Springer-Verlag, Berlin/Heidelberg, 2008, 21--35. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. Salehie, M. and Tahvildari, L. Self-adaptive software: Landscape and research challenges. ACM Transactions on Autonomous and Adaptive Systems 4, 2 (May 2009), 14:1--14:42. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. Zave, P. and Jackson, M. Four dark corners of requirements engineering. Transactions on Software Engineering and Methodology 6, 1 (Jan. 1997), 1--30. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. Zheng, T., Woodside, M., and Litoiu, M. Performance model estimation and tracking using optimal filters. IEEE Transactions on Software Engineering 34, 3 (May-June 2008), 391--406. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Self-adaptive software needs quantitative verification at runtime

                    Recommendations

                    Comments

                    Login options

                    Check if you have access through your login credentials or your institution to get full access on this article.

                    Sign in

                    Full Access

                    • Published in

                      cover image Communications of the ACM
                      Communications of the ACM  Volume 55, Issue 9
                      September 2012
                      104 pages
                      ISSN:0001-0782
                      EISSN:1557-7317
                      DOI:10.1145/2330667
                      Issue’s Table of Contents

                      Copyright © 2012 ACM

                      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                      Publisher

                      Association for Computing Machinery

                      New York, NY, United States

                      Publication History

                      • Published: 1 September 2012

                      Permissions

                      Request permissions about this article.

                      Request Permissions

                      Check for updates

                      Qualifiers

                      • research-article
                      • Popular
                      • Refereed

                    PDF Format

                    View or Download as a PDF file.

                    PDF

                    eReader

                    View online with eReader.

                    eReader

                    HTML Format

                    View this article in HTML Format .

                    View HTML Format