A Translation from Object-Based Hypergraph Grammars into π-Calculus
Resumo
Object-based models offer abstract constructions to describe complex systems. The Object-Based Graph Grammar (OBGG) is a very intuitive formalism that may be used to describe this kind of systems. To be really useful in practice, there should be a (preferably automatic) way to verify whether the desired properties of a system are fulfilled by the model constructed using graph grammars. However, up to now, there are no automatic tools for verification of OBGGs. In this work we propose a translation from Object-Based Graph Grammars into π-Calculus. So, we may be able to prove properties of systems modeled in OBGGs using existing automatic checkers for π-calculus.Referências
Copstein, B., Móra, M. d. C., and Ribeiro, L. (2000). An Environment for Formal Modeling and Simulation of Control Systems. In Proc. 33rd Annual Simulation Symposium, pages 74–82, Washington. Institute of Electrical and Electronics Engineers.
Dotti, F. L. and Ribeiro, L. (2000). Specification of Mobile Code Systems Using Graph Grammars. In 4 IFIF TC6 WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, pages 45–63, Stanford. Boston: Kluwer Academic.
Duarte, L. (2001). Development of distributed systems with mobile code through formal specification (in portuguese). Master’s thesis, Pontifícia Universicade Católica do Rio Grande do Sul.
Ehrig, H. (1978). Introduction to the Algebraic Theory of Graph Grammars. In Proc. International Workshop on Graph-Grammars and Their Application to Computer Science and Biology, volume 73 of Lecture Notes in Computer Science, pages 1–69, Bad Honnef. Berlin: Springer Verlag.
Ferrari, G., Gnesi, S., Montanari, U., Pistore, M., and G.Ristori (1998). Verifying Mobile Processes in the HAL Environment. In International Conference on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 511–515, Vancouver, CA. Berlin: Springer Verlag.
Milner, R. and Parrow, J. (1992). A Calculus for Mobile Processes I and II. Information and Computation, 100:1–77.
Victor, B. and Moller, F. (1994). The Mobility Workbench - a tool for the π-calculus. In Dill, D., editor, Proc. International Conference on Computer Aided Verification, CAV, volume 818 of Lecture Notes in Computer Science, pages 428–440. Berlin: Springer-Verlag.
Dotti, F. L. and Ribeiro, L. (2000). Specification of Mobile Code Systems Using Graph Grammars. In 4 IFIF TC6 WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, pages 45–63, Stanford. Boston: Kluwer Academic.
Duarte, L. (2001). Development of distributed systems with mobile code through formal specification (in portuguese). Master’s thesis, Pontifícia Universicade Católica do Rio Grande do Sul.
Ehrig, H. (1978). Introduction to the Algebraic Theory of Graph Grammars. In Proc. International Workshop on Graph-Grammars and Their Application to Computer Science and Biology, volume 73 of Lecture Notes in Computer Science, pages 1–69, Bad Honnef. Berlin: Springer Verlag.
Ferrari, G., Gnesi, S., Montanari, U., Pistore, M., and G.Ristori (1998). Verifying Mobile Processes in the HAL Environment. In International Conference on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 511–515, Vancouver, CA. Berlin: Springer Verlag.
Milner, R. and Parrow, J. (1992). A Calculus for Mobile Processes I and II. Information and Computation, 100:1–77.
Victor, B. and Moller, F. (1994). The Mobility Workbench - a tool for the π-calculus. In Dill, D., editor, Proc. International Conference on Computer Aided Verification, CAV, volume 818 of Lecture Notes in Computer Science, pages 428–440. Berlin: Springer-Verlag.
Publicado
31/07/2004
Como Citar
FOSS, Luciana; RIBEIRO, Leila.
A Translation from Object-Based Hypergraph Grammars into π-Calculus. In: CONCURSO DE TESES E DISSERTAÇÕES (CTD), 17. , 2004, Salvador/BA.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2004
.
p. 69-73.
ISSN 2763-8820.
