A Probabilistic Model Checking Technique for the Verification of Self-Organising Emergent Systems
Resumo
O desenvolvimento de sistemas emergentes auto-organizáveis (SEAOs) constitui-se em um grande desafio para as atuais abordagens de engenharia de software. Realizar verificação de modelos para estes sistemas é difícil, visto que seu comportamento não pode ser descrito linearmente e sua estrutura pode mudar dinamicamente. Neste artigo, propomos uma técnica para modelar e verificar SEAOs que utiliza verificação de modelos probabilística. Esta técnica foi aplicada a um problema envolvendo um SEAO, possibilitando a obtenção de resultados de verificação de propriedades relevantes. Tais resultados mostram que nossas abstrações são adequadas para descrever este SEAO e indicam que a mesma ideia pode ser aplicada a outros sistemas similares.Referências
Applegate, D., Bixby, R. E., Chvátal, V., and Cook, W. (2006). The Traveling Salesman Problem: A Computational Study. Princeton University Press.
Ben-Ari, M., Manna, Z., and Pnueli, A. (1983). The temporal logic of branching time. Acta Informatica, 20(3):207–226.
Casadei, M. and Viroli, M. (2009). Using probabilistic model checking and simulation for designing self-organizing systems. In SAC, pages 2103–2104.
Clarke, E. M., Grumberg, O., and Peled, D. A. (1999). Model Checking. The MIT Press, Cambridge, Massachusetts, USA.
Cormen, T., Leiserson, C., Rivest, R., and Stein, C. (2001). Introduction to Algorithms. The MIT Press.
De Wolf, T. and Holvoet, T. (2005a). Emergence versus self-organisation: Different concepts but promising when combined. In Engineering Self-Organising Systems: Methodologies and Applications, volume 3464 of LNCS, pages 1–15. Springer-Verlag.
De Wolf, T. and Holvoet, T. (2005b). Towards a methodolgy for engineering self-organising emergent systems. In SOAS 2005, volume 135 of Frontiers in Artificial Intelligence and Applications, pages 18–34, Glasgow, Scotland. IOS Press.
De Wolf, T., Holvoet, T., and Samaey, G. (2006). Development of self-organising emergent applications with simulation-based numerical analysis. In Engineering Self-Organising Systems, volume 3910 of LNCS, pages 138–152. Springer.
Dorigo, M. and Gambardella, L. (1997). Ant colony system: A cooperative learning approach to the traveling salesman problem. IEEE Trans. on Evol. Comp., 1(1):53–66.
Duarte, L. M., Kramer, J., and Uchitel, S. (2008). Towards faithful model extraction based on contexts. In Proceedings of FASE 2008, volume 4961 of Lecture Notes in Computer Science, pages 101–115, Budapest, Hungary. Springer.
Gardelli, L. (2008). Engineering Self-Organising Systems with the Multiagent Paradigm. Phd thesis, Alma Mater Studiorum-Università di Bologna, DEIS-Dipartimento di Elettronica, Informatica e Sistemistica.
Gould, R. (1991). Updating the hamiltonian problem - a survey. Journal of Graph Theory, 15:121–157.
Hansson, H. and Jonsson, B. (1994). A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535.
Hong, J., Lu, S., and Chen, D. (2008). Towards bio-inspired self-organization in sensor networks: Applying the ant colony algorithm. In 22nd AINA, pages 1054–1061.
Kwiatkowska, M., Norman, G., and Parker, D. (2002). PRISM: Probabilistic symbolic model checker. In TOOLS’02, volume 2324 of LNCS, pages 200–204. Springer.
Mano, J.-P., Bourjot, C., Lopardo, G., and Glize, P. (2006). Bio-inspired mechanisms for artificial self-organised systems. Informatica, 30:55–62.
Soares, B., Gatti, M., and Lucena, C. (2008). Towards verifying and optimizing self-organizing systems through an autonomic convergence method. In Proc. of 4th Workshop on Soft. Eng. for Agent-oriented Systems, pages 73–84, Campinas, Brazil.
Vardi, M. (1985). Automatic verification of probabilistic concurrent finite state programs. In Proc. of the 26th Annual Symp. on Found. of Comp. Sci., pages 327–338.
Wagner, F. R., Duarte, L. M., Heimfarth, T., and Foss, L. e. a. (2009). Uma metodologia de engenharia de software para o desenvolvimento de sistemas emergentes auto-organizáveis. In II Seminário da SBC sobre Grandes Desafios da Computação no Brasil.
Ben-Ari, M., Manna, Z., and Pnueli, A. (1983). The temporal logic of branching time. Acta Informatica, 20(3):207–226.
Casadei, M. and Viroli, M. (2009). Using probabilistic model checking and simulation for designing self-organizing systems. In SAC, pages 2103–2104.
Clarke, E. M., Grumberg, O., and Peled, D. A. (1999). Model Checking. The MIT Press, Cambridge, Massachusetts, USA.
Cormen, T., Leiserson, C., Rivest, R., and Stein, C. (2001). Introduction to Algorithms. The MIT Press.
De Wolf, T. and Holvoet, T. (2005a). Emergence versus self-organisation: Different concepts but promising when combined. In Engineering Self-Organising Systems: Methodologies and Applications, volume 3464 of LNCS, pages 1–15. Springer-Verlag.
De Wolf, T. and Holvoet, T. (2005b). Towards a methodolgy for engineering self-organising emergent systems. In SOAS 2005, volume 135 of Frontiers in Artificial Intelligence and Applications, pages 18–34, Glasgow, Scotland. IOS Press.
De Wolf, T., Holvoet, T., and Samaey, G. (2006). Development of self-organising emergent applications with simulation-based numerical analysis. In Engineering Self-Organising Systems, volume 3910 of LNCS, pages 138–152. Springer.
Dorigo, M. and Gambardella, L. (1997). Ant colony system: A cooperative learning approach to the traveling salesman problem. IEEE Trans. on Evol. Comp., 1(1):53–66.
Duarte, L. M., Kramer, J., and Uchitel, S. (2008). Towards faithful model extraction based on contexts. In Proceedings of FASE 2008, volume 4961 of Lecture Notes in Computer Science, pages 101–115, Budapest, Hungary. Springer.
Gardelli, L. (2008). Engineering Self-Organising Systems with the Multiagent Paradigm. Phd thesis, Alma Mater Studiorum-Università di Bologna, DEIS-Dipartimento di Elettronica, Informatica e Sistemistica.
Gould, R. (1991). Updating the hamiltonian problem - a survey. Journal of Graph Theory, 15:121–157.
Hansson, H. and Jonsson, B. (1994). A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535.
Hong, J., Lu, S., and Chen, D. (2008). Towards bio-inspired self-organization in sensor networks: Applying the ant colony algorithm. In 22nd AINA, pages 1054–1061.
Kwiatkowska, M., Norman, G., and Parker, D. (2002). PRISM: Probabilistic symbolic model checker. In TOOLS’02, volume 2324 of LNCS, pages 200–204. Springer.
Mano, J.-P., Bourjot, C., Lopardo, G., and Glize, P. (2006). Bio-inspired mechanisms for artificial self-organised systems. Informatica, 30:55–62.
Soares, B., Gatti, M., and Lucena, C. (2008). Towards verifying and optimizing self-organizing systems through an autonomic convergence method. In Proc. of 4th Workshop on Soft. Eng. for Agent-oriented Systems, pages 73–84, Campinas, Brazil.
Vardi, M. (1985). Automatic verification of probabilistic concurrent finite state programs. In Proc. of the 26th Annual Symp. on Found. of Comp. Sci., pages 327–338.
Wagner, F. R., Duarte, L. M., Heimfarth, T., and Foss, L. e. a. (2009). Uma metodologia de engenharia de software para o desenvolvimento de sistemas emergentes auto-organizáveis. In II Seminário da SBC sobre Grandes Desafios da Computação no Brasil.
Publicado
20/07/2010
Como Citar
DUARTE, Lucio Mauro; FOSS, Luciana; WAGNER, Flávio Rech; HEIMFARTH, Tales.
A Probabilistic Model Checking Technique for the Verification of Self-Organising Emergent Systems. In: SEMINÁRIO INTEGRADO DE SOFTWARE E HARDWARE (SEMISH), 37. , 2010, Belo Horizonte/MG.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2010
.
p. 410-424.
ISSN 2595-6205.
