Um Verificador de Modelos Descritos em Redes de Autômatos Estocásticos - Correa, Claiton M.; Dotti, Fernando L.; Fernandes, Paulo; Maruani, Eli; Oleksinski, Lucas G.; Sales, Afonso (Anais do Workshop de Testes e Tolerância a Falhas (WTF); 2012: Anais do XIII Workshop de Testes e Tolerância a FalhasDO - 10.5753/wtf.2012.23084, 2012)
Durante a construção de sistemas modernos, tanto a satisfação de propriedades funcionais quanto a habilidade de afirmar níveis de desempenho e disponibilidade destes sistemas são necessárias. Neste sentido, vários formalismos de modelagem contam com abstrações e ferramentas para apoiar tanto a verificação da funcionalidade como realizar análises quantitativas. Redes de Autômatos Estocásticos são um formalismo voltado para a avaliação de desempenho, o qual é atrativo tanto devido a seu conjunto de abstrações como pelo potencial tratamento de amplo espaço de estados. Este artigo descreve a primeira versão de um verificador de modelos descritos em Redes de Autômatos Estocásticos. Este verificador faz uso de técnicas de verificação simbólica e verifica propriedades escritas na lógica temporal Computation Tree Logic. Relato do seu uso em estudos de casos clássicos são feitos.