Exploiting assumption-based verification for the adaptation of service-based applications

ABSTRACT

Service-based applications (SBAs) need to operate in a highly dynamic world, in which their constituent services could fail or become unavailable. Monitoring is typically used to identify such failures and, if needed, to trigger an adaptation of the SBA to compensate for those failures.

However, existing monitoring approaches exhibit several limitations: (1) Monitoring individual services can uncover failures of services. Yet, it remains open whether those individual failures lead to a violation of the SBA's requirements, which would necessitate an adaptation. (2) Monitoring the SBA can uncover requirements deviations. However, it will not provide information about the failures leading to this deviation, which constitutes important information needed for the adaptation activities. Even a combination of (1) and (2) is limited. For instance, a requirements deviation will only be identified after it has occurred, e. g., after the execution of the whole SBA, which then in case of failures might require costly compensation actions.

In this paper we introduce an approach that addresses those limitations by augmenting monitoring techniques for individual services with formal verification techniques. The approach explicitly encodes assumptions that the constituent services of an SBA will perform as expected. Based on those assumptions, formal verification is used to assess whether the SBA requirements are satisfied and whether a violation of those assumptions during run-time leads to a violation of the SBA requirements. Thereby, our approach allows for (a) pro-actively deciding whether the SBA requirements will be violated based on monitored failures, and (b) identifying the specific root cause for the violated requirements.

References

1. L. Ardissono, R. Furnari, A. Goy, G. Petrone, and M. Segnan. Fault tolerant web service orchestration by means of diagnosis. In V. Gruhn and F. Oquendo, editors, EWSA, volume 4344 of Lecture Notes in Computer Science, pages 2--16. Springer, 2006.
2. M. Autili, P. Inverardi, and P. Pelliccione. Graphical scenarios for specifying temporal properties: an automated approach. Automated Software Eng., 14(3):293--340, 2007.
3. F. Barbon, P. Traverso, M. Pistore, and M. Trainotti. Run-Time Monitoring of Instances and Classes of Web Service Compositions. In IEEE International Conference on Web Services (ICWS 2006), pages 63--71, 2006.
4. L. Baresi, C. Ghezzi, and S. Guinea. Smart monitors for composed services. In ICSOC '04: Proceedings of the 2nd international conference on Service oriented computing, pages 193--202, New York, NY, USA, 2004. ACM.
5. L. Baresi and S. Guinea. Towards dynamic monitoring of ws-bpel processes. In ICSOC, pages 269--282, 2005.
6. L. Baresi, S. Guinea, M. Trainotti, and M. Pistore. Dynamo + ASTRO: An integrated approach for bpel monitoring. In 7th International Conference on Web Services (ICWS 2009), 2009.
7. J. R. Büchi. On a decision method in restricted second-order arithmetic. In Proc. 1960 Int. Congr. for Logic, Methodology, and Philosophy of Science, pages 1--1. Stanford Univ. Press, 1962.
8. A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. Nusmv: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2:2000, 2000.
9. D. Cohen, M. S. Feather, K. Narayanaswamy, and S. S. Fickas. Automatic monitoring of software requirements. In ICSE '97: Proceedings of the 19th international conference on Software engineering, pages 602--603, New York, NY, USA, 1997. ACM.
10. A. Dardenne, A. V. Lamsweerde, and S. Fickas. Goal-directed requirements acquisition. In Science of Computer Programming, pages 3--50, 1993.
11. S. Fickas, T. Beauchamp, and N. A. R. Mamy. Monitoring requirements: A case study. In ASE '02: Proceedings of the 17th IEEE international conference on Automated software engineering, page 299, Washington, DC, USA, 2002. IEEE Computer Society.
12. S. Fickas and M. S. Feather. Requirements monitoring in distributed environments. In SDNE '95: Proceedings of the 2nd International Workshop on Services in Distributed and Networked Environments, page 93, Washington, DC, USA, 1995. IEEE Computer Society.
13. S. Fickas and M. S. Feather. Requirements monitoring in dynamic environments. In RE '95: Proceedings of the Second IEEE International Symposium on Requirements Engineering, page 140, Washington, DC, USA, 1995. IEEE Computer Society.
14. H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of web service compositions. In ASE '03, pages 152--161. IEEE, 2003.
15. C. Ghezzi and S. Guinea. Run-time monitoring in service-oriented architectures. In Test and Analysis of Web Services, pages 237--264, 2007.
16. O. Grumberg and D. E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16, 1991.
17. M. R. Hansen and Z. Chaochen. Duration calculus: Logical foundations. Formal Asp. Comput., 9(3):283--330, 1997.
18. P. Inverardi, P. Pelliccione, and M. Tivoli. Towards an assume-guarantee theory for adaptable systems. Software Engineering for Adaptive and Self-Managing Systems, International Workshop on, 0:106--115, 2009.
19. M. Jackson and P. Zave. Deriving specifications from requirements: an example. In ICSE '95: Proceedings of the 17th international conference on Software engineering, pages 15--24, New York, NY, USA, 1995. ACM.
20. R. Kazhamiakin, A. Metzger, and M. Pistore. Towards correctness assurance in adaptive service-based applications. In ServiceWave 2008, number 5377 in LNCS. Springer, 10--13 December 2008.
21. R. Kazhamiakin, P. Pandya, and M. Pistore. Representation, verification, and computation of timed properties. International Conference on Web Services, pages 497--504, 2006.
22. R. Kazhamiakin and M. Pistore. Static verification of control and data in web service compositions. In ICWS '06: Proceedings of the IEEE International Conference on Web Services, pages 83--90, Washington, DC, USA, 2006. IEEE Computer Society.
23. Z. Lu, S. Li, A. Ghose, and P. Hyland. Extending semantic web service description by service assumption. In WI '06: Proceedings of the 2006 IEEE/WIC/ACM International Conference on Web Intelligence, pages 637--643, Washington, DC, USA, 2006. IEEE Computer Society.
24. K. Mahbub and G. Spanoudakis. Run-time monitoring of requirements for systems composed of web-services: Initial implementation and evaluation experience. In ICWS '05: Proceedings of the IEEE International Conference on Web Services, pages 257--265, Washington, DC, USA, 2005. IEEE Computer Society.
25. S. Nakajima. Model-checking verification for reliable web service. OOPSLA Workshop on Object-Oriented Web Services (OOWS 2002), 2002.
26. S. Narayanan and S. A. McIlraith. Simulation, verification and automated composition of web services. In WWW '02: Proceedings of the 11th international conference on World Wide Web, pages 77--88, New York, NY, USA, 2002. ACM.
27. G. Newton, J. Pollock, and D. L. McGuinness. Semantic web rule language (SWRL), 2004.
28. E. D. Nitto, C. Ghezzi, A. Metzger, M. Papazoglou, and K. Pohl. A journey to highly dynamic, self-adaptive service-based applications. Automated Software Engineering, 15(3--4):257--402, 2008.
29. M. Pistore and P. Traverso. Assumption-based composition and monitoring of web services. In Test and Analysis of Web Services, pages 307--335, 2007.
30. A. van Lamsweerde. Requirements engineering in the year 00: a research perspective. In ICSE '00: Proceedings of the 22nd international conference on Software engineering, pages 5--19, New York, NY, USA, 2000. ACM.
31. A. van Lamsweerde, E. Letier, and R. Darimont. Managing conflicts in goal-driven requirements engineering. IEEE Trans. Softw. Eng., 24(11):908--926, 1998.

Index Terms

• Information systems

  • Data management systems

    • Middleware for databases

      • Distributed transaction monitors

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Contextual software domains

      • Operating systems

        • Process management

          • Monitors

    • Software functional properties

      • Formal methods