Adaptando Verificadores de Modelos para a Geração Automática de Objetivos de Teste para Sistemas Reativos
Resumo
Objetivos de teste são artefatos utilizados como guias da geração de casos de teste. Representam propriedades que definem os comportamentos a serem exibidos por uma implementação sob teste (IST). São especificados com base em análises sobre um modelo da IST. Quando realizadas sobre especificações formais, estas análises podem ser automatizadas por técnicas rigorosas, como a verificação de modelos. Este artigo apresenta uma adaptação dos algoritmos de um verificador de modelos para a realização de análises voltadas para a geração de objetivos de teste.Referências
Ammann, P. E., Black, P. E., and Majursky, W. (1998). Using model checking to generate tests from specifications. In Society, I. C., editor, In Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM’98), pages 46–54.
Clarke, E., Grumberg, O., and Peled, D. (1999). Model Checking. MIT Press.
de Vries, R. G. and Tretmans, J. (1998). On-the-fly conformance testing using spin. In G. Holzmann, E. N. and Serhrouchni, A., editors, Fourth Workshop on Automata Theoretic Verification with the Spin Model Checker, ENST 98 S 002, Paris, France. Ecole Nationale Supérieure des Télécommunications, pages 115–128.
de Vries, R. G. and Tretmans, J. (2001). Towards formal test purposes. In Proc. 1st International Workshop on Formal Approaches to Testing of Software (FATES), Aalborg, Denmark, pages 61–76.
Fernandez, J.-C., Jard, C., Jéron, T., and Viho, G. (1997). An experiment in automatic generation of conformance test suites for protocols with verification technology. Science of Computer Programming, 29:123–146.
Guerra, F. V. d. A., de Figueiredo, J. C. A., and Guerrero, D. D. S. (2004). Timed extension of an object oriented petri net language. In Simpósio Brasileiro de Métodos Formais - SBMF 2004, pages 132–148, Recife - Brasil.
Heljanko, K. (1997). Model checking the branching time temporal logic ctl. Technical Report A45, Helsinki University of Technology.
Henniger, O., Lu, M., and Ural, H. (2003). Automatic generation of test purposes for testing distributed systems. In Formal Approaches to Software Testing, Proceedings of FATES’03, volume 2931 of Lecture Notes in Computer Science, pages 178–191. Springer.
Hoare, C. A. R. (1985). Communicating Sequential Processes. Prentice-Hall.
Jard, C. and Jéron, T. (2004). TGV: theory, principles and algorithms – A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Software Tools for Technology Transfer (STTT), 6.
Jensen, K. (1992). Coloured Petri Nets 1: Basic Concepts, Analysis Methods and Practical Use, volume 1. Springer-Verlag, Berlin, Alemanha.
Perkins, C. (2002). Rfc 3344:IP mobility support for IPv4. Status: Proposed Standard.
Rodrigues, C. L., Guerra, F. V., de Figueiredo, J. C. A., Guerrero, D. D. S., and Morais, T. S. (2004). Modeling and verification of mobility issues using object-oriented petrinets. In Proc. of 3rd International Information and Telecommunication Technologies Symposium (I2TS2004).
Silva, D. A. and Machado, P. D. L. (2006). Towards Test Purpose Generation from CTL Properties for Reactive Systems. In Proc. of the 2nd International Workshop on Model Based Testing (MBT), Vienna, Austria. To appear.
Tretmans, J. (1996). Test Generation with Inputs, Outputs and Repetitive Quiescence. Software—Concepts and Tools, 17(3):103–120.
Vergauwen, B. and Lewi, J. (1993). A linear local model checking algorithm for ctl. In Best, E., editor, CONCUR’93: Proc. of the 4th International Conference on Concurrency Theory, pages 447–461. Springer, Berlin, Heidelberg.
Clarke, E., Grumberg, O., and Peled, D. (1999). Model Checking. MIT Press.
de Vries, R. G. and Tretmans, J. (1998). On-the-fly conformance testing using spin. In G. Holzmann, E. N. and Serhrouchni, A., editors, Fourth Workshop on Automata Theoretic Verification with the Spin Model Checker, ENST 98 S 002, Paris, France. Ecole Nationale Supérieure des Télécommunications, pages 115–128.
de Vries, R. G. and Tretmans, J. (2001). Towards formal test purposes. In Proc. 1st International Workshop on Formal Approaches to Testing of Software (FATES), Aalborg, Denmark, pages 61–76.
Fernandez, J.-C., Jard, C., Jéron, T., and Viho, G. (1997). An experiment in automatic generation of conformance test suites for protocols with verification technology. Science of Computer Programming, 29:123–146.
Guerra, F. V. d. A., de Figueiredo, J. C. A., and Guerrero, D. D. S. (2004). Timed extension of an object oriented petri net language. In Simpósio Brasileiro de Métodos Formais - SBMF 2004, pages 132–148, Recife - Brasil.
Heljanko, K. (1997). Model checking the branching time temporal logic ctl. Technical Report A45, Helsinki University of Technology.
Henniger, O., Lu, M., and Ural, H. (2003). Automatic generation of test purposes for testing distributed systems. In Formal Approaches to Software Testing, Proceedings of FATES’03, volume 2931 of Lecture Notes in Computer Science, pages 178–191. Springer.
Hoare, C. A. R. (1985). Communicating Sequential Processes. Prentice-Hall.
Jard, C. and Jéron, T. (2004). TGV: theory, principles and algorithms – A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Software Tools for Technology Transfer (STTT), 6.
Jensen, K. (1992). Coloured Petri Nets 1: Basic Concepts, Analysis Methods and Practical Use, volume 1. Springer-Verlag, Berlin, Alemanha.
Perkins, C. (2002). Rfc 3344:IP mobility support for IPv4. Status: Proposed Standard.
Rodrigues, C. L., Guerra, F. V., de Figueiredo, J. C. A., Guerrero, D. D. S., and Morais, T. S. (2004). Modeling and verification of mobility issues using object-oriented petrinets. In Proc. of 3rd International Information and Telecommunication Technologies Symposium (I2TS2004).
Silva, D. A. and Machado, P. D. L. (2006). Towards Test Purpose Generation from CTL Properties for Reactive Systems. In Proc. of the 2nd International Workshop on Model Based Testing (MBT), Vienna, Austria. To appear.
Tretmans, J. (1996). Test Generation with Inputs, Outputs and Repetitive Quiescence. Software—Concepts and Tools, 17(3):103–120.
Vergauwen, B. and Lewi, J. (1993). A linear local model checking algorithm for ctl. In Best, E., editor, CONCUR’93: Proc. of the 4th International Conference on Concurrency Theory, pages 447–461. Springer, Berlin, Heidelberg.
Publicado
29/05/2006
Como Citar
SILVA, Daniel Aguiar da; MACHADO, Patricia D. L..
Adaptando Verificadores de Modelos para a Geração Automática de Objetivos de Teste para Sistemas Reativos. In: WORKSHOP DE TESTES E TOLERÂNCIA A FALHAS (WTF), 7. , 2006, Curitiba/PR.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2006
.
p. 13-24.
ISSN 2595-2684.
DOI: https://doi.org/10.5753/wtf.2006.23348.
