Um Verificador de Modelos Descritos em Redes de Autômatos Estocásticos
Resumo
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.Referências
Baier, C. and Katoen, J.-P. (2008). Principles of Model Checking. MIT Press.
Benoit, A., Brenner, L., Fernandes, P., Plateau, B., Sbeity, I., and Stewart, W. J. (2007). Peps 2007 user manual.
Benoit, A., Brenner, L., Fernandes, P., Plateau, B., and Stewart, W. J. (2003). The peps software tool. In Computer Performance Evaluation/TOOLS, pages 98–115.
Brenner, L., Fernandes, P., Plateau, B., and Sbeity, I. (2007). Peps 2007 - stochastic automata networks software tool. Quantitative Evaluation of Systems, International Conference on, 0:163–164.
Brenner, L., Fernandes, P., and Sales, A. (2005). The Need for and the Advantages of Generalized Tensor Algebra for Kronecker Structured Representations. International Journal of Simulation: Systems, Science & Technology (IJSIM), 6(3-4):52–60.
Clarke, E. M., Grumberg, O., and Peled, A. D. (1999). Model Checking. MIT Press, Cambridge, Massachusetts.
Czekster, R. (2010). Solução numérica de descritores markovianos a partir de reestruturações de termos tensoriais. PhD thesis, Pontifı́cia Universidade Católica do Rio Grande do Sul, Brasil.
Fernandes, P., Plateau, B., and Stewart, W. J. (1998). Efficient descriptor-vector multiplication in Stochastic Automata Networks. Journal of the ACM, 45(3):381–414.
Hadzic, T., Hooker, J. N., O’Sullivan, B., and Tiedemann, P. (2008). Approximate compilation of constraints into multivalued decision diagrams. In Proceedings of the 14th international conference on Principles and Practice of Constraint Programming, CP ’08, pages 448–462, Berlin, Heidelberg. Springer-Verlag.
Hurth, M. and Ryan, M. (2004). Logic In Computer Science. Cambridge University Press.
Miller, D. and Drechsler, R. (1998). Implementing a multiple-valued decision diagram package. In 28th IEEE International Symposium on Multiple-Valued Logic, pages 52–57.
Plateau, B. (1985). On the stochastic structure of parallelism and synchronization models for distributed algorithms. SIGMETRICS Perform. Eval. Rev., 13:147–154.
Sales, A. and Plateau, B. (2009). Reachable state space generation for structured models which use functional transitions. In 6th International Conference on the Quantitative Evaluation of Systems (QEST’09), pages 269–278, Budapest, Hungary. IEEE Computer Society.
Stewart, W. J. (2009). Probability, Markov Chains, Queues, and Simulation: The Mathematical Basis of Performance Modeling. Princeton University Press, USA.
Benoit, A., Brenner, L., Fernandes, P., Plateau, B., Sbeity, I., and Stewart, W. J. (2007). Peps 2007 user manual.
Benoit, A., Brenner, L., Fernandes, P., Plateau, B., and Stewart, W. J. (2003). The peps software tool. In Computer Performance Evaluation/TOOLS, pages 98–115.
Brenner, L., Fernandes, P., Plateau, B., and Sbeity, I. (2007). Peps 2007 - stochastic automata networks software tool. Quantitative Evaluation of Systems, International Conference on, 0:163–164.
Brenner, L., Fernandes, P., and Sales, A. (2005). The Need for and the Advantages of Generalized Tensor Algebra for Kronecker Structured Representations. International Journal of Simulation: Systems, Science & Technology (IJSIM), 6(3-4):52–60.
Clarke, E. M., Grumberg, O., and Peled, A. D. (1999). Model Checking. MIT Press, Cambridge, Massachusetts.
Czekster, R. (2010). Solução numérica de descritores markovianos a partir de reestruturações de termos tensoriais. PhD thesis, Pontifı́cia Universidade Católica do Rio Grande do Sul, Brasil.
Fernandes, P., Plateau, B., and Stewart, W. J. (1998). Efficient descriptor-vector multiplication in Stochastic Automata Networks. Journal of the ACM, 45(3):381–414.
Hadzic, T., Hooker, J. N., O’Sullivan, B., and Tiedemann, P. (2008). Approximate compilation of constraints into multivalued decision diagrams. In Proceedings of the 14th international conference on Principles and Practice of Constraint Programming, CP ’08, pages 448–462, Berlin, Heidelberg. Springer-Verlag.
Hurth, M. and Ryan, M. (2004). Logic In Computer Science. Cambridge University Press.
Miller, D. and Drechsler, R. (1998). Implementing a multiple-valued decision diagram package. In 28th IEEE International Symposium on Multiple-Valued Logic, pages 52–57.
Plateau, B. (1985). On the stochastic structure of parallelism and synchronization models for distributed algorithms. SIGMETRICS Perform. Eval. Rev., 13:147–154.
Sales, A. and Plateau, B. (2009). Reachable state space generation for structured models which use functional transitions. In 6th International Conference on the Quantitative Evaluation of Systems (QEST’09), pages 269–278, Budapest, Hungary. IEEE Computer Society.
Stewart, W. J. (2009). Probability, Markov Chains, Queues, and Simulation: The Mathematical Basis of Performance Modeling. Princeton University Press, USA.
Publicado
30/04/2012
Como Citar
CORREA, Claiton M.; DOTTI, Fernando L.; FERNANDES, Paulo; MARUANI, Eli; OLEKSINSKI, Lucas G.; SALES, Afonso.
Um Verificador de Modelos Descritos em Redes de Autômatos Estocásticos. In: WORKSHOP DE TESTES E TOLERÂNCIA A FALHAS (WTF), 13. , 2012, Ouro Preto/MG.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2012
.
p. 115-128.
ISSN 2595-2684.
DOI: https://doi.org/10.5753/wtf.2012.23084.
