Adaptando Verificadores de Modelos para a Geração Automática de Objetivos de Teste para Sistemas Reativos

• Daniel Aguiar da Silva UFCG
• Patricia D. L. Machado UFCG

DOI: https://doi.org/10.5753/wtf.2006.23348

Abstract

Test purposes are properties that specify behaviours an implementation under test (IUT) should exhibit. Such properties are usually specified through analyses performed over a model for the IUT. When performed over formal specifications, these analyses can be automated through formal techniques, such as model checking. This paper presents the adaption of the algorithms of a model checker in order to provide a new approach for model analyses aimed at the test purpose generation.

References

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.