A Probabilistic Model Checking Technique for the Verification of Self-Organising Emergent Systems - Duarte, Lucio Mauro; Foss, Luciana; Wagner, Flávio Rech; Heimfarth, Tales (Anais do Seminário Integrado de Software e Hardware (SEMISH); 2010: Anais do XXXVII Seminário Integrado de Software e Hardware, 2010)
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.