Uma Metodologia para a Verificação de Sistemas Parciais Modelados na Gramática de Grafos Baseada em Objetos
Resumo
O desenvolvimento de sistemas distribuídos é considerado uma tarefa complexa. Em especial, garantir que estes sistemas apresentam certas propriedades, fundamentais para o seu correto funcionamento, torna-se muito difícil em ambientes abertos, como, por exemplo, a Internet. Neste artigo utilizamos uma linguagem visual de especificação formal, chamada Gramática de Grafos Baseadas em Objetos (GGBO), para a especificação e verificação de sistemas distribuídos. É proposta uma metodologia para a verificação de sistemas parciais, baseada no raciocínio assume-guarantee, definidos na GGBO. Na metodologia proposta, uma transformação é realizada sobre o objeto a ser verificado. A transformação tem como objetivo fechar (completar) o comportamento do objeto, de forma que a técnica de verificação de modelos possa ser aplicada ao mesmo. Um objeto que implementa a ordenação de mensagens é utilizado, no decorrer do artigo, para ilustrar a metodologia definida.
Referências
Silva, F. A. A transaction model based on mobile agents. Tese de doutorado, Technical University Berlin - FB Informatik, Alemanha, 1999.
Dotti, F. L., Ribeiro, L. Specification of mobile code systems using graph grammars. In: 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 177, IFIP Conference Proceedings, p. 45-63, EUA, 2000. Kluwer Academic Publishers.
Copstein, B., Móra, M. C., Ribeiro, L. An environment for formal modeling and simulation of control systems. In: 33rd Annual Simulation Symposium, p. 74-82, EUA, 2000. IEEE Computer Society Press.
Dotti, F. L., Duarte, L. M., Copstein, B., Ribeiro, L. Simulation of mobile applications. In: 2002 Communication Networks and Distributed Systems Modeling and Simulation Conference, p. 261-267, EUA, 2002. The Society for Modeling and Simulation International.
Dotti, F. L., Foss, L., Ribeiro, L., Santos, O. M. Verification of object-based distributed systems. In: 6th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 2884, LNCS, p. 261-275, França, 2003. Springer-Verlag.
Santos, O. M., Dotti, F. L., Ribeiro, L. Verifying object-based graph grammars (aceito para publicação). ENTCS, p. 1-12, 2004.
Pasareanu, C. S., Dwyer, M. B., and Huth, M. Assume-guarantee model checking of software: a comparative case study. In: 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, volume 1680, LNCS, p. 168-183, França, 1999. Springer-Verlag.
Colby, C., Godefroid, P., Jagadeesan, L. J. Automatically closing open reactive programs. ACM SIGPLAN Notices, 33(5):345-357, 1998.
Pnueli, A. In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, NATO ASI F13, p. 123-144, EUA, 1985. Springer-Verlag.
Ehrig, H. Introduction to the algebraic theory of graph grammars. In: 1st International Workshop on Graph Grammars and Their Application to Computer Science and Biology, volume 73, LNCS, p. 1-69, Alemanha, 1979. Springer-Verlag.
Holzmann, G. J. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.
Clarke, E. M., Grumberg, O., Peled, D. A. Model checking. MIT Press, EUA, 1999.
Kupferman, O., Vardi, M. Y., Wolper, P. Module checking. Information and Computation, 164(2):322-344, 2001.
Vardi, M. Y. Branching vs linear time: final showdown. In: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031, LNCS, p. 1-22, Itália, 2001. Springer-Verlag.
Dwyer, M. B., Pasareanu, C. S. Filter-based model checking of partial systems. In: 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering, p. 189-202, EUA, 1998. ACM Press.
Paun, D. O., Chechik, M. Events in linear-time properties. In: 4th International Conference on Requirements Engineering, p. 123-132, Irlanda, 1999. IEEE Computer Society Press.
Dwyer, M. B., Pasareanu, C. S. Model checking generic container implementations. In: Selected Papers from the International Seminar on Generic Programming, volume 1766, LNCS, p. 162-177, Reino Unido, 2000. Springer-Verlag.
Avrunin, G. S., Corbett, J. C., Dillon, L. K. Analyzing partially-implemented real-time systems. IEEE Transactions on Software Engineering, 24(8):602-614, 1998.
Xie, F., Browne, J. C. Verified systems by composition from verified components. In: 10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, p. 277-286, Finlândia, 2003. ACM Press.
Graf, S., Steffen, B. Compositional minimization of finite state systems. In: 2nd International Workshop on Computer Aided Verification, volume 531, LNCS, p. 186-196. Springer-Verlag, 1991.
Yeh, W. J., Young, M. Compositional reachability analysis using process algebra. In: Symposium on Testing, Analysis, and Verification, p. 49-59, Canadá, 1991. ACM Press.
Cheung, S. C., Kramer, J. Context constraints for compositional reachability analysis. ACM Transactions Software Engineering Methodology, 5(4):334-377, 1996.
Cheung, S. C., Kramer, J. Checking safety properties using compositional reachability analysis. ACM Transactions Software Engineering Methodology, 8(1):49-78, 1999.
Godefroid, P. Model checking for programming languages using VeriSoft. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 174-186, França, 1997. ACM Press.
Giannakopoulou, D., Pasareanu, C. S., Barringer, H. Assumption generation for software component verification. In: 17th IEEE International Conference on Automated Software Engineering, p. 3-12, Reino Unido, 2002. IEEE Computer Society.
Manna, Z., Pnueli, A. The temporal logic of reactive and concurrent systems - specification. Springer-Verlag, Alemanha, 1992.
Kupferman, O., Vardi, M. Y. On the complexity of branching modular model checking (extended abstract). In: 6th International Conference on Concurrency Theory, volume 962, LNCS, p. 408-422, EUA, 1995. Springer-Verlag.
Kupferman, O., Vardi, M. Y. An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages Systems, 22(1):87-128, 2000.
Dotti, F. L., Ribeiro, L. Specification of mobile code systems using graph grammars. In: 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 177, IFIP Conference Proceedings, p. 45-63, EUA, 2000. Kluwer Academic Publishers.
Copstein, B., Móra, M. C., Ribeiro, L. An environment for formal modeling and simulation of control systems. In: 33rd Annual Simulation Symposium, p. 74-82, EUA, 2000. IEEE Computer Society Press.
Dotti, F. L., Duarte, L. M., Copstein, B., Ribeiro, L. Simulation of mobile applications. In: 2002 Communication Networks and Distributed Systems Modeling and Simulation Conference, p. 261-267, EUA, 2002. The Society for Modeling and Simulation International.
Dotti, F. L., Foss, L., Ribeiro, L., Santos, O. M. Verification of object-based distributed systems. In: 6th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 2884, LNCS, p. 261-275, França, 2003. Springer-Verlag.
Santos, O. M., Dotti, F. L., Ribeiro, L. Verifying object-based graph grammars (aceito para publicação). ENTCS, p. 1-12, 2004.
Pasareanu, C. S., Dwyer, M. B., and Huth, M. Assume-guarantee model checking of software: a comparative case study. In: 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, volume 1680, LNCS, p. 168-183, França, 1999. Springer-Verlag.
Colby, C., Godefroid, P., Jagadeesan, L. J. Automatically closing open reactive programs. ACM SIGPLAN Notices, 33(5):345-357, 1998.
Pnueli, A. In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, NATO ASI F13, p. 123-144, EUA, 1985. Springer-Verlag.
Ehrig, H. Introduction to the algebraic theory of graph grammars. In: 1st International Workshop on Graph Grammars and Their Application to Computer Science and Biology, volume 73, LNCS, p. 1-69, Alemanha, 1979. Springer-Verlag.
Holzmann, G. J. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.
Clarke, E. M., Grumberg, O., Peled, D. A. Model checking. MIT Press, EUA, 1999.
Kupferman, O., Vardi, M. Y., Wolper, P. Module checking. Information and Computation, 164(2):322-344, 2001.
Vardi, M. Y. Branching vs linear time: final showdown. In: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031, LNCS, p. 1-22, Itália, 2001. Springer-Verlag.
Dwyer, M. B., Pasareanu, C. S. Filter-based model checking of partial systems. In: 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering, p. 189-202, EUA, 1998. ACM Press.
Paun, D. O., Chechik, M. Events in linear-time properties. In: 4th International Conference on Requirements Engineering, p. 123-132, Irlanda, 1999. IEEE Computer Society Press.
Dwyer, M. B., Pasareanu, C. S. Model checking generic container implementations. In: Selected Papers from the International Seminar on Generic Programming, volume 1766, LNCS, p. 162-177, Reino Unido, 2000. Springer-Verlag.
Avrunin, G. S., Corbett, J. C., Dillon, L. K. Analyzing partially-implemented real-time systems. IEEE Transactions on Software Engineering, 24(8):602-614, 1998.
Xie, F., Browne, J. C. Verified systems by composition from verified components. In: 10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, p. 277-286, Finlândia, 2003. ACM Press.
Graf, S., Steffen, B. Compositional minimization of finite state systems. In: 2nd International Workshop on Computer Aided Verification, volume 531, LNCS, p. 186-196. Springer-Verlag, 1991.
Yeh, W. J., Young, M. Compositional reachability analysis using process algebra. In: Symposium on Testing, Analysis, and Verification, p. 49-59, Canadá, 1991. ACM Press.
Cheung, S. C., Kramer, J. Context constraints for compositional reachability analysis. ACM Transactions Software Engineering Methodology, 5(4):334-377, 1996.
Cheung, S. C., Kramer, J. Checking safety properties using compositional reachability analysis. ACM Transactions Software Engineering Methodology, 8(1):49-78, 1999.
Godefroid, P. Model checking for programming languages using VeriSoft. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 174-186, França, 1997. ACM Press.
Giannakopoulou, D., Pasareanu, C. S., Barringer, H. Assumption generation for software component verification. In: 17th IEEE International Conference on Automated Software Engineering, p. 3-12, Reino Unido, 2002. IEEE Computer Society.
Manna, Z., Pnueli, A. The temporal logic of reactive and concurrent systems - specification. Springer-Verlag, Alemanha, 1992.
Kupferman, O., Vardi, M. Y. On the complexity of branching modular model checking (extended abstract). In: 6th International Conference on Concurrency Theory, volume 962, LNCS, p. 408-422, EUA, 1995. Springer-Verlag.
Kupferman, O., Vardi, M. Y. An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages Systems, 22(1):87-128, 2000.
Publicado
18/10/2004
Como Citar
DOTTI, Fernando L.; PASINI, Fábio; SANTOS, Osmar M. dos.
Uma Metodologia para a Verificação de Sistemas Parciais Modelados na Gramática de Grafos Baseada em Objetos. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 18. , 2004, Brasília/DF.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2004
.
p. 86-101.
DOI: https://doi.org/10.5753/sbes.2004.23835.
