Especificação e Verificação Formal de Sistemas Distribuídos

• Fernando L. Dotti PUCRS
• Luciana Foss UFRGS
• Leila Ribeiro UFRGS
• Osmar M. dos Santos PUCRS

DOI: https://doi.org/10.5753/sbes.2003.23863

Resumo

Neste artigo utilizamos uma linguagem visual de especificação formal, chamada Gramáticas de Grafos Baseadas em Objetos (GGBO), para especificar sistemas distribuídos. A GGBO é comparada com a linguagem PROMELA (a PROcess MEta LAnguage), usada como entrada pelo verificador de modelos SPIN. Com base nesta comparação, define-se um mapeamento de GGBO para PROMELA. É visto como especificar e verificar propriedades sobre os modelos mapeados para PROMELA. Um algoritmo de eleição em anel é utilizado, no decorrer do artigo, para ilustrar a GGBO, a tradução e a verificação de propriedades.

Palavras-chave: Gramática de grafos, verificação de modelos, sistemas distribuídos

Referências

F. M. A. Silva. A transaction model based on mobile agents. Tese de doutorado, Technical University Berlin FB-Informatik, Germany, 1999.

E. M. Clarke, J. M. Wing, R. Alur, et al. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626-643, 1996.

F. L. Dotti and L. Ribeiro. Specification of mobile code systems using graph grammars. In 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, volume 177 of IFIP Conference Proceedings, pages 45-63, USA, 2000. Kluwer.

B. Copstein, M. C. Móra, and L. Ribeiro. An environment for formal modeling and simulation of control systems. In 33rd Annual Simulation Symposium, pages 74-82, USA, 2000. IEEE Computer Society.

F. L. Dotti, L. M. Duarte, B. Copstein, and L. Ribeiro. Simulation of mobile applications. In Communication Networks and Distributed Systems Modeling and Simulation Conference, pages 261-267, USA, 2002. The Society for Modeling and Simulation International.

L. Foss. Uma tradução de gramáticas de hipergrafos baseados em objetos para cálculo-π . Dissertação de mestrado, UFRGS II PPGC, Brasil, 2003.

A. B. Loreto, L. Ribeiro, and L. Toscani. Complexity analysis of reactive graph grammars. Revista de Informática Teórica e Aplicada UFRGS, 7(1):109-128, 2000.

N. A. Lynch. Distributed algorithms, pages 476-482. Morgan Kaufmann, USA, 1996.

G. Booch, J. Rumbaugh, and I Jacobson. The unified modeling language users guide. Addison Wesley, USA, 1999.

H. Ehrig. 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 of LNCS, pages 1-69. Springer, 1979.

G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.

Research Bell-Labs. PROMELA language reference. http://cm.bell-labs.com/cm/cs/what/spin/Man/promela.html, 2003.

L. M. Duarte. Desenvolvimento de sistemas distribuídos com código móvel a partir de especificação formal. Dissertação de mestrado, PUCRS - FACIN - PPGCC, Brasil, 2001.

S. Leue and G. Holzmann. v-Promela: a visual, object oriented language for SPIN. In 2nd International Symposium on Object-Oriented Real-Time Distributed Computing, pages 14-23, France, 1999. IEEE Computer Society.

S. M. Cho, D. H. Bae, S. D. Cha, et al. Applying model checking to concurrent object-oriented software. In 4th International Symposium on Autonomous Decentralized Systems, pages 380- 383, Japan, 1999. IEEE Computer Society.

J. Lilius and I. P. Paltor. vUML: a tool for verifying UML models. In 14th International Conference on Automated Software Engineering, pages 255-258, USA, 1999. IEEE Computer Society.

K. Winter and R. Duke. Model checking Object-Z using ASM. In 3rd International Conference on Integrated Formal Methods, volume 2335 of LNCS, pages 165-184. Springer, 2002.

K. L. MacMillan. Symbolic model checking: an approach to the state explosion problem. Tese de doutorado, Carnegie Mellon University, USA, 1992.