Proposta de uma abordagem para a verificação formal de Sistemas Distribuídos Baseados em Objetos
Resumo
Este artigo propõe uma abordagem para a verificação formal, através da técnica de verificação de modelos, de Sistemas Distribuídos Baseados em Objetos (SDBOs). A linguagem de descrição utilizada para modelar SDBOs é uma forma restrita de Gramática de Grafos, um formalismo gráfico, declarativo, e que suporta paralelismo implícito. Esta linguagem, chamada Gramática de Grafos Baseada em Objetos (GGBO), é brevemente apresentada. Os modelos descritos na GGBO são mapeados para a linguagem de descrição PROMELA (PROtocol/PROcess MEta LAnguage), usada pelo verificador de modelos SPIN (Simple Promela INterpreter). Este mapeamento é descrito. A partir disso, propriedades sobre modelos descritos na GGBO podem ser especificadas e verificadas através do SPIN. Um exemplo de descrição na GGBO é apresentado e mapeado.
Referências
Avizienis, A., Laprie, J.-C., and Randell, B. (2001). Fundamental concepts of dependability. Technical Report 01-145, LAAS (Laboratory for Analysis and Architecture of Systems), Taulosse, France.
Cho, S. M., Bae, D. H., Cha, S. D., Kim, Y. G., Yoo, B., and Kim, S. (1999). Applying Model Checking to Concurrent Object-oriented Software. In 4th International Symposium on Autonomous Decentralized Systems, pages 380–383, Tokyo, Japan. IEEE Computer Society Press.
Clarke, E. M., Grumberg, O., and Peled, D. A. (1999). Model Checking. MIT Press, Cambridge, MA, USA.
Clarke, E. M., Wing, J. M., Alur, R., Cleaveland, R., and et al (1996). Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 28(4):626–643.
Copstein, B., da Costa Móra, M., and Ribeiro, L. (2000). An Environment for Formal Modeling and Simulation of Control Systems. In 33rd Annual Simulation Symposium, pages 74–82, Washington, USA. IEEE Computer Society Press.
Dotti, F. L. and Ribeiro, L. (2000). Specification of Mobile Code Systems Using Graph Grammars. In 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 177, pages 45–63, Stanford, CA, USA. Kluwer - IFIP Conference Proceedings.
Duarte, L. M. (2001). Desenvolvimento de Sistemas Distribuídos com Código Móvel a partir de Especificação Formal. Dissertação de mestrado, Pontifícia Universidade Católica do Rio Grande do Sul, Faculdade de Informática - Programa de Pós-Graduação em Ciência da Computação, Porto Alegre, RS, Brasil.
Ehrig, H. (1979). 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, pages 1–69, Berlin, Germany. Springer-Verlag - Lecture Notes in Computer Science.
Holzmann, G. J. (1997). The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295.
Leue, S. and Holzmann, G. (1999). v-Promela: a visual, object oriented language for SPIN. In 2nd International Symposium on Object-Oriented Real-Time Distributed Computing, SaintMalo, France. IEEE Computer Society Press.
Lilius, J. and Paltor, I. P. (1999). vUML: A Tool for Verifying UML Models. In 14th In ternational Conference on Automated Software Engineering, pages 255–258, Cocoa Beach, Florida, USA. IEEE Computer Society Press.
Lynch, N. A. (1996). Distributed Algorithms, pages 476–482. Morgan Kaufmann Publishers, San Francisco, CA, USA.
Manna, Z. and Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer-Verlag, New York, NY, USA.
Rödel, E. T. (2003). Modelagem Formal de Falhas em Sistemas Distribuídos envolvendo Mobilidade. Dissertação de mestrado, Pontifícia Universidade Católica do Rio Grande do Sul, Faculdade de Informática - Programa de Pós-Graduação em Ciência da Computação, Porto Alegre, RS, Brasil.
Winter, K. and Duke, R. (2002). Model Checking Object-Z using ASM. In 3rd International Conference on Integrated Formal Methods, volume 2335, pages 165–184. Lecture Notes in Computer Science, Spinger-Verlag.
Cho, S. M., Bae, D. H., Cha, S. D., Kim, Y. G., Yoo, B., and Kim, S. (1999). Applying Model Checking to Concurrent Object-oriented Software. In 4th International Symposium on Autonomous Decentralized Systems, pages 380–383, Tokyo, Japan. IEEE Computer Society Press.
Clarke, E. M., Grumberg, O., and Peled, D. A. (1999). Model Checking. MIT Press, Cambridge, MA, USA.
Clarke, E. M., Wing, J. M., Alur, R., Cleaveland, R., and et al (1996). Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 28(4):626–643.
Copstein, B., da Costa Móra, M., and Ribeiro, L. (2000). An Environment for Formal Modeling and Simulation of Control Systems. In 33rd Annual Simulation Symposium, pages 74–82, Washington, USA. IEEE Computer Society Press.
Dotti, F. L. and Ribeiro, L. (2000). Specification of Mobile Code Systems Using Graph Grammars. In 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 177, pages 45–63, Stanford, CA, USA. Kluwer - IFIP Conference Proceedings.
Duarte, L. M. (2001). Desenvolvimento de Sistemas Distribuídos com Código Móvel a partir de Especificação Formal. Dissertação de mestrado, Pontifícia Universidade Católica do Rio Grande do Sul, Faculdade de Informática - Programa de Pós-Graduação em Ciência da Computação, Porto Alegre, RS, Brasil.
Ehrig, H. (1979). 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, pages 1–69, Berlin, Germany. Springer-Verlag - Lecture Notes in Computer Science.
Holzmann, G. J. (1997). The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295.
Leue, S. and Holzmann, G. (1999). v-Promela: a visual, object oriented language for SPIN. In 2nd International Symposium on Object-Oriented Real-Time Distributed Computing, SaintMalo, France. IEEE Computer Society Press.
Lilius, J. and Paltor, I. P. (1999). vUML: A Tool for Verifying UML Models. In 14th In ternational Conference on Automated Software Engineering, pages 255–258, Cocoa Beach, Florida, USA. IEEE Computer Society Press.
Lynch, N. A. (1996). Distributed Algorithms, pages 476–482. Morgan Kaufmann Publishers, San Francisco, CA, USA.
Manna, Z. and Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer-Verlag, New York, NY, USA.
Rödel, E. T. (2003). Modelagem Formal de Falhas em Sistemas Distribuídos envolvendo Mobilidade. Dissertação de mestrado, Pontifícia Universidade Católica do Rio Grande do Sul, Faculdade de Informática - Programa de Pós-Graduação em Ciência da Computação, Porto Alegre, RS, Brasil.
Winter, K. and Duke, R. (2002). Model Checking Object-Z using ASM. In 3rd International Conference on Integrated Formal Methods, volume 2335, pages 165–184. Lecture Notes in Computer Science, Spinger-Verlag.
Publicado
19/05/2003
Como Citar
SANTOS, Osmar Marchi dos; DOTTI, Fernando Luís.
Proposta de uma abordagem para a verificação formal de Sistemas Distribuídos Baseados em Objetos. In: WORKSHOP DE TESTES E TOLERÂNCIA A FALHAS (WTF), 4. , 2003, Natal/RN.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2003
.
p. 61-68.
ISSN 2595-2684.
DOI: https://doi.org/10.5753/wtf.2003.23391.
