Self-Adaptive Systems Planning with Model Checking using MAPE-K
Resumo
This paper presents a model checking-based approach to support the autonomous planning of adaptation actions in Self-Adaptive Systems, designed in consonance with the MAPE-K reference architecture. We evaluated our approach with a case-study aiming at verifying self-healing and self-organizing properties in a distributed and decentralized traffic monitoring system. Results show that our approach is able to generate adaptation plans satisfying the goals for all expected scenarios in such a case-study, providing a flexible formal framework where adaptation strategies and goals can be inserted/removed.
Palavras-chave:
Self-Adaptive Systems, autonomous planning, model checking
Referências
Al-Zawi, M. M., Al-Jumeily, D., Hussain, A., and Taleb-Bendiab, A. (2011). Autonomiccomputing: Applications of self-healing systems. In 2011 Developments in E-systemsEngineering, pages 381-386. IEEE.
Andrade, S. S. (2014). Projeto arquitetural automatizado de sistemas self-adaptive-umaabordagem baseada em busca.
Arcaini, P., Riccobene, E., and Scandurra, P. (2017). Formal design and verification ofself-adaptive systems with decentralized control. ACM Transactions on Autonomousand Adaptive Systems (TAAS), 11(4):25.
Baier, C. and Katoen, J.-P. (2008). Principles of model checking. MIT press.
Behrmann, G., David, A., and Larsen, K. G. (2006). A tutorial on uppaal 4.0. Departmentof computer science, Aalborg university.
Berns, A. and Ghosh, S. (2009). Dissecting self-* properties. In 2009 Third IEEE In-ternational Conference on Self-Adaptive and Self-Organizing Systems, pages 10-19.IEEE.
Camilli, M., Gargantini, A., and Scandurra, P. (2015). Specifying and verifying real-time self-adaptive systems. In 2015 IEEE 26th International Symposium on SoftwareReliability Engineering (ISSRE), pages 303-313. IEEE.
da Silva Ferreira, M., Menezes, M. V., and de Barros, L. N. (2018). Plan existence verifi-cation as symbolic model checking. In Anais do XV Encontro Nacional de InteligênciaArtificial e Computacional, pages 116-127. SBC.
Ghallab, M., Nau, D., and Traverso, P. (2004). Automated Planning: theory and practice.Elsevier.
Giunchiglia, F. and Traverso, P. (1999). Planning as model checking. In European Con-ference on Planning, pages 1-20. Springer.
Grumberg, O., Clarke, E., and Peled, D. (1999). Model checking.
Huth, M. and Ryan, M. (2004). Logic in Computer Science: Modelling and reasoningabout systems. Cambridge university press.
Iftikhar, M. U. and Weyns, D. (2012). A case study on formal verification of self-adaptivebehaviors in a decentralized system. arXiv preprint arXiv:1208.4635.
Iglesia, D. G. D. L. and Weyns, D. (2015). Mape-k formal templates to rigorously designbehaviors for self-adaptive systems. ACM Transactions on Autonomous and AdaptiveSystems (TAAS), 10(3):15.
Kephart, J. O. and Chess, D. M. (2003). The vision of autonomic computing. Computer,(1):41-50.
Laddaga, R. (1997). Darpa broad agency announcement on self-adaptive software.
Momeni, H., Kashefi, O., and Sharifi, H. (2008). How to realize self-healing operatingsystems? In 2008 3rd International Conference on Information and CommunicationTechnologies: From Theory to Applications, pages 1-4. IEEE.
Naqvi, M. (2012). Claims and supporting evidence for self-adaptive systems-a literaturereview.
Oreizy, P., Medvidovic, N., and Taylor, R. N. (1998). Architecture-based runtime softwareevolution. In Proceedings of the 20th international conference on Software enginee-ring, pages 177-186. IEEE.
Pereira, S. L. and de Barros, L. N. (2008). A logic-based agent that plans for extendedreachability goals. Autonomous Agents and Multi-Agent Systems, 16(3):327-344.
Russell, S. J. and Norvig, P. (2016). Artificial intelligence: a modern approach. Malaysia;Pearson Education Limited,.
Salehie, M. and Tahvildari, L. (2009a). Self-adaptive software: Landscape and researchchallenges. ACM transactions on autonomous and adaptive systems (TAAS), 4(2):14.
Salehie, M. and Tahvildari, L. (2009b). Self-adaptive software: Landscape and researchchallenges. ACM transactions on autonomous and adaptive systems (TAAS), 4(2):14.
Sykes, D., Heaven, W., Magee, J., and Kramer, J. (2007). Plan-directed architecturalchange for autonomous systems. In Proceedings of the 2007 conference on Specifica-tion and verification of component-based systems: 6th Joint Meeting of the EuropeanConference on Software Engineering and the ACM SIGSOFT Symposium on the Foun-dations of Software Engineering, pages 15-21. ACM.
Sykes, D., Heaven, W., Magee, J., and Kramer, J. (2008). From goals to components:a combined approach to self-management. In Proceedings of the 2008 internationalworkshop on Software engineering for adaptive and self-managing systems, pages 1-8.ACM.
Weyns, D. (2012). Towards an integrated approach for validating qualities of self-adaptivesystems. In Proceedings of the Ninth International Workshop on Dynamic Analysis,pages 24-29. ACM.
Weyns, D., Iftikhar, M. U., De La Iglesia, D. G., and Ahmad, T. (2012). A survey offormal methods in self-adaptive systems. In Proceedings of the Fifth International C*Conference on Computer Science and Software Engineering, pages 67-79. ACM.
Wildermann, S. (2012). Systematic design of self-adaptive embedded systems with ap-plications in image processing.
Andrade, S. S. (2014). Projeto arquitetural automatizado de sistemas self-adaptive-umaabordagem baseada em busca.
Arcaini, P., Riccobene, E., and Scandurra, P. (2017). Formal design and verification ofself-adaptive systems with decentralized control. ACM Transactions on Autonomousand Adaptive Systems (TAAS), 11(4):25.
Baier, C. and Katoen, J.-P. (2008). Principles of model checking. MIT press.
Behrmann, G., David, A., and Larsen, K. G. (2006). A tutorial on uppaal 4.0. Departmentof computer science, Aalborg university.
Berns, A. and Ghosh, S. (2009). Dissecting self-* properties. In 2009 Third IEEE In-ternational Conference on Self-Adaptive and Self-Organizing Systems, pages 10-19.IEEE.
Camilli, M., Gargantini, A., and Scandurra, P. (2015). Specifying and verifying real-time self-adaptive systems. In 2015 IEEE 26th International Symposium on SoftwareReliability Engineering (ISSRE), pages 303-313. IEEE.
da Silva Ferreira, M., Menezes, M. V., and de Barros, L. N. (2018). Plan existence verifi-cation as symbolic model checking. In Anais do XV Encontro Nacional de InteligênciaArtificial e Computacional, pages 116-127. SBC.
Ghallab, M., Nau, D., and Traverso, P. (2004). Automated Planning: theory and practice.Elsevier.
Giunchiglia, F. and Traverso, P. (1999). Planning as model checking. In European Con-ference on Planning, pages 1-20. Springer.
Grumberg, O., Clarke, E., and Peled, D. (1999). Model checking.
Huth, M. and Ryan, M. (2004). Logic in Computer Science: Modelling and reasoningabout systems. Cambridge university press.
Iftikhar, M. U. and Weyns, D. (2012). A case study on formal verification of self-adaptivebehaviors in a decentralized system. arXiv preprint arXiv:1208.4635.
Iglesia, D. G. D. L. and Weyns, D. (2015). Mape-k formal templates to rigorously designbehaviors for self-adaptive systems. ACM Transactions on Autonomous and AdaptiveSystems (TAAS), 10(3):15.
Kephart, J. O. and Chess, D. M. (2003). The vision of autonomic computing. Computer,(1):41-50.
Laddaga, R. (1997). Darpa broad agency announcement on self-adaptive software.
Momeni, H., Kashefi, O., and Sharifi, H. (2008). How to realize self-healing operatingsystems? In 2008 3rd International Conference on Information and CommunicationTechnologies: From Theory to Applications, pages 1-4. IEEE.
Naqvi, M. (2012). Claims and supporting evidence for self-adaptive systems-a literaturereview.
Oreizy, P., Medvidovic, N., and Taylor, R. N. (1998). Architecture-based runtime softwareevolution. In Proceedings of the 20th international conference on Software enginee-ring, pages 177-186. IEEE.
Pereira, S. L. and de Barros, L. N. (2008). A logic-based agent that plans for extendedreachability goals. Autonomous Agents and Multi-Agent Systems, 16(3):327-344.
Russell, S. J. and Norvig, P. (2016). Artificial intelligence: a modern approach. Malaysia;Pearson Education Limited,.
Salehie, M. and Tahvildari, L. (2009a). Self-adaptive software: Landscape and researchchallenges. ACM transactions on autonomous and adaptive systems (TAAS), 4(2):14.
Salehie, M. and Tahvildari, L. (2009b). Self-adaptive software: Landscape and researchchallenges. ACM transactions on autonomous and adaptive systems (TAAS), 4(2):14.
Sykes, D., Heaven, W., Magee, J., and Kramer, J. (2007). Plan-directed architecturalchange for autonomous systems. In Proceedings of the 2007 conference on Specifica-tion and verification of component-based systems: 6th Joint Meeting of the EuropeanConference on Software Engineering and the ACM SIGSOFT Symposium on the Foun-dations of Software Engineering, pages 15-21. ACM.
Sykes, D., Heaven, W., Magee, J., and Kramer, J. (2008). From goals to components:a combined approach to self-management. In Proceedings of the 2008 internationalworkshop on Software engineering for adaptive and self-managing systems, pages 1-8.ACM.
Weyns, D. (2012). Towards an integrated approach for validating qualities of self-adaptivesystems. In Proceedings of the Ninth International Workshop on Dynamic Analysis,pages 24-29. ACM.
Weyns, D., Iftikhar, M. U., De La Iglesia, D. G., and Ahmad, T. (2012). A survey offormal methods in self-adaptive systems. In Proceedings of the Fifth International C*Conference on Computer Science and Software Engineering, pages 67-79. ACM.
Wildermann, S. (2012). Systematic design of self-adaptive embedded systems with ap-plications in image processing.
Publicado
07/12/2020
Como Citar
DA SILVA, Aristóteles Esteves Marçal; ANDRADE, Aline Maria Santos; ANDRADE, Sandro Santos.
Self-Adaptive Systems Planning with Model Checking using MAPE-K. In: WORKSHOP DE TESTES E TOLERÂNCIA A FALHAS (WTF), 21. , 2020, Rio de Janeiro.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2020
.
p. 69-82.
ISSN 2595-2684.
DOI: https://doi.org/10.5753/wtf.2020.12488.
