Formal Development of Concurrent Systems using Algebraic High-Level Nets and Transformations
Resumo
Neste artigo são apresentadas redes algébricas de alto nível: uma combinação de especificações algébricas e redes de Petri. Especificações algébricas são usadas para a descrição da estrutura dos dados e redes de Petri para a descrição do fluxo dos dados. Esta combinação é uma técnica de especificação muito poderosa. Transformações de, fusões e uniões de redes também são introduzidas neste artigo como técnicas para a estruturação da especificação. Fusões e uniões são usadas como mecanismos de estruturação horizontal no sentido que redes são combinadas para se obter redes maiores. Transformações de redes são baseadas em conceitos de gramática de grafos, refinamentos de redes são definidos em termos de produções, e podem ser vistos como refinamentos de redes de alto nível. Em nosso formalismo existe compatibilidade entre refinamentos verticais e estruturação horizontal.
Referências
J. R. Abrial. Programming as a mathematical exercise. In C. A. R. HOARE, editor, Mathematical logic and programming languages. Prentice-Hall International, 1985.
G.A. Agha. ACTORS: A Model of Concurrent Computation in Distributed Systems. The MIT Press Cambridge, Massachusetts, London, England, 1988.
E. Astesiano and G. Reggio. An outline of the SMolCS approach. In M. Venturini Zilli, editor, Mathematical models for the semantics of parallelism, volume 280 of Lecture Notes in Computer Science. Springer Verlag Berlin, 1987.
J. A. Bergstra and J. W. Klop. Algebra of communicating processes. In CWI Monographs I, 1986. Proc. CWIU Symp. Math. and Comp. Sci.
D. Bjorner and C. B. Jones, editors. The Vienna Development Method: the meta-language, volume 61 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1978.
F. Cornelius, Marcus Klar, and Michael Löwe. Ein Fallbeispiel fir KORSO: Ist-Analyse HDMS-A. Technical report, Technical University of Berlin, 1993. To appear.
C. Dimitrovici and A. Heise. Transformation und Komposition von P/T-Netzen unter Erhaltung wesentlicher Eigenschaften. Technical Report 342/6/91, Technical University of Munich, jul. 1991.
C. Dimitrovici, U. Hummert, and L. Petrucci. Composition and net properties of algebraic high-level nets. In Advances of Petri-Nets, Lecture Notes in Computer Science 483. Springer, 1991.
H. Ehrig. Introduction to the algebraic theory of graph grammars. In 1st Int. Workshop on Graph Grammars and their Application to Computer Science and Biology, Lecture Notes in Computer Science 73, pages 1-69. Springer, 1979.
H. Ebrig, M. Grofe-Rhode, and A. Heise. Specification techniques for concurrent and distributed systems. Technical Report 92/5, Technical University of Berlin, jan. 1992. Invited paper for 2nd Maghr. Conference on Software Engineering and Artificial Intelligence, Tunis,1992.
H. Ebrig, A. Habel, H.-J. Kreowski, and F. Parisi-Presicce. Parallelism and concurrency in High Level Replacement Systems. Mathematical Structures in Comp. Sei., 1:361-404, 1992.
H. Ebrig, H.-J. Kreowski, and G. Taentzer. Canonical Derivations in High-Level Replacement Systems. Technical Report 6/92, University of Bremen, 1992.
H. Ebrig and B. Mahr. Fundamentals of algebraic specifications, volume 6 of EACTS-Monographs in Theoretical Computer Science. Springer, Berlin, 1985.
H. Ehrig, J. Padberg, and L. Ribeiro. Algebraic high-level nets: Petri nets revisited. Technical Report 93-06, Technical University of Berlin, 1993. To appear in the Proc. of the ADT-COMPASS Workshop'92, Caldes de Malavella, Spain.
H. Ehrig, F. Parisi-Presicce, P. Boehm, C. Rieckhoff, C. Dimitrovici, and M. Grofe-Rhode. Algebraic data type and process specifications based on projection spaces. Theoretical Computer Science, 332:23-43, 1987.
H.J. Genrich and K. Lautenbach. System modelling with high-level Petri nets. Theoretical Computer Science, 13:109-136, 1981.
D. Giesel, J. Kriger, and R. Jeschke. Grundkonzepte und Implementierung eines Netzw--erkzeugs für Algebraische High-Level Netze. Technical Report 90/34, Technical University of Berlin, 1990.
C. A. R. Hoare. Communicating sequential processes. Prentice-Hall International, London, 1985.
P. Huber, A. M. Jensen, L. O. Jepsen, and K. Jensen. Reachability trees for high-level Petri nets. High-level Petri nets: theory and application, pages 319-350, 1992.
P. Huber, K. Jensen, and R. M. Shapiro. Hierarquies in coloured Petri nets. High-level Petri nets: theory and application, pages 215-243, 1992.
U. Hummert. Algebraische High-Level Netze. PhD thesis, Technical University of Berlin, Department of Computer Science, 1989.
22]
K. Jensen. Coloured petri nets and the invariant method. Theoretical Computer Science, 14:317-336, 1981.
K. Jensen and G. Rozenberg, editors. High-level Petri nets: theory and application. Springer-Verlag, Berlin, 1992.
LOTOS - A formal description technique based on temporal ordering of observational behaviour. Information Processing Systems - Open Systems Interconnection ISO DIS 8807, jul. 1987. (ISO/TC 97/SC 21 N).
M. Löwe and M. Beyer. AGG - An Implementation of Algebraic Graph Rewriting. Accepted at the Fifth Int. Conf. on Rewriting Techniques and Applications, 1993.
J. Meseguer and U. Montanari. Petri nets are monoids. In Proc. Logic in computer science, Edinburgh, 1988.
R. Milner, editor. A calculus for communicationg systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
J. Padberg. Theory of High-Level Replacement Systems with Application to Petri Nets. Diplomarbeit, Technical University of Berlin, 1992.
J. Padberg, H. Ebrig, and L. Ribeiro. Algebraic High-Level Net-Transformation Systems. Technical Report 93-12, Technical University of Berlin, 1993. To appear in Mathematical Structures in Computer Science.
C.A. Petri. Kommunikation mit Automaten. PhD thesis, Schriften des Institutes fir Instrumentelle Mathematik, Bonn, 1962.
W. Reisig. Petri nets. Springer Verlag, 1985.
J. Vautherin. Parallel specification with coloured Petri nets and algebraic data types. In Proc. of the 7th European Workshop on Application and Theory of Petri nets, pages 5-23, Oxford, England, jul. 1986.
G.A. Agha. ACTORS: A Model of Concurrent Computation in Distributed Systems. The MIT Press Cambridge, Massachusetts, London, England, 1988.
E. Astesiano and G. Reggio. An outline of the SMolCS approach. In M. Venturini Zilli, editor, Mathematical models for the semantics of parallelism, volume 280 of Lecture Notes in Computer Science. Springer Verlag Berlin, 1987.
J. A. Bergstra and J. W. Klop. Algebra of communicating processes. In CWI Monographs I, 1986. Proc. CWIU Symp. Math. and Comp. Sci.
D. Bjorner and C. B. Jones, editors. The Vienna Development Method: the meta-language, volume 61 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1978.
F. Cornelius, Marcus Klar, and Michael Löwe. Ein Fallbeispiel fir KORSO: Ist-Analyse HDMS-A. Technical report, Technical University of Berlin, 1993. To appear.
C. Dimitrovici and A. Heise. Transformation und Komposition von P/T-Netzen unter Erhaltung wesentlicher Eigenschaften. Technical Report 342/6/91, Technical University of Munich, jul. 1991.
C. Dimitrovici, U. Hummert, and L. Petrucci. Composition and net properties of algebraic high-level nets. In Advances of Petri-Nets, Lecture Notes in Computer Science 483. Springer, 1991.
H. Ehrig. Introduction to the algebraic theory of graph grammars. In 1st Int. Workshop on Graph Grammars and their Application to Computer Science and Biology, Lecture Notes in Computer Science 73, pages 1-69. Springer, 1979.
H. Ebrig, M. Grofe-Rhode, and A. Heise. Specification techniques for concurrent and distributed systems. Technical Report 92/5, Technical University of Berlin, jan. 1992. Invited paper for 2nd Maghr. Conference on Software Engineering and Artificial Intelligence, Tunis,1992.
H. Ebrig, A. Habel, H.-J. Kreowski, and F. Parisi-Presicce. Parallelism and concurrency in High Level Replacement Systems. Mathematical Structures in Comp. Sei., 1:361-404, 1992.
H. Ebrig, H.-J. Kreowski, and G. Taentzer. Canonical Derivations in High-Level Replacement Systems. Technical Report 6/92, University of Bremen, 1992.
H. Ebrig and B. Mahr. Fundamentals of algebraic specifications, volume 6 of EACTS-Monographs in Theoretical Computer Science. Springer, Berlin, 1985.
H. Ehrig, J. Padberg, and L. Ribeiro. Algebraic high-level nets: Petri nets revisited. Technical Report 93-06, Technical University of Berlin, 1993. To appear in the Proc. of the ADT-COMPASS Workshop'92, Caldes de Malavella, Spain.
H. Ehrig, F. Parisi-Presicce, P. Boehm, C. Rieckhoff, C. Dimitrovici, and M. Grofe-Rhode. Algebraic data type and process specifications based on projection spaces. Theoretical Computer Science, 332:23-43, 1987.
H.J. Genrich and K. Lautenbach. System modelling with high-level Petri nets. Theoretical Computer Science, 13:109-136, 1981.
D. Giesel, J. Kriger, and R. Jeschke. Grundkonzepte und Implementierung eines Netzw--erkzeugs für Algebraische High-Level Netze. Technical Report 90/34, Technical University of Berlin, 1990.
C. A. R. Hoare. Communicating sequential processes. Prentice-Hall International, London, 1985.
P. Huber, A. M. Jensen, L. O. Jepsen, and K. Jensen. Reachability trees for high-level Petri nets. High-level Petri nets: theory and application, pages 319-350, 1992.
P. Huber, K. Jensen, and R. M. Shapiro. Hierarquies in coloured Petri nets. High-level Petri nets: theory and application, pages 215-243, 1992.
U. Hummert. Algebraische High-Level Netze. PhD thesis, Technical University of Berlin, Department of Computer Science, 1989.
22]
K. Jensen. Coloured petri nets and the invariant method. Theoretical Computer Science, 14:317-336, 1981.
K. Jensen and G. Rozenberg, editors. High-level Petri nets: theory and application. Springer-Verlag, Berlin, 1992.
LOTOS - A formal description technique based on temporal ordering of observational behaviour. Information Processing Systems - Open Systems Interconnection ISO DIS 8807, jul. 1987. (ISO/TC 97/SC 21 N).
M. Löwe and M. Beyer. AGG - An Implementation of Algebraic Graph Rewriting. Accepted at the Fifth Int. Conf. on Rewriting Techniques and Applications, 1993.
J. Meseguer and U. Montanari. Petri nets are monoids. In Proc. Logic in computer science, Edinburgh, 1988.
R. Milner, editor. A calculus for communicationg systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
J. Padberg. Theory of High-Level Replacement Systems with Application to Petri Nets. Diplomarbeit, Technical University of Berlin, 1992.
J. Padberg, H. Ebrig, and L. Ribeiro. Algebraic High-Level Net-Transformation Systems. Technical Report 93-12, Technical University of Berlin, 1993. To appear in Mathematical Structures in Computer Science.
C.A. Petri. Kommunikation mit Automaten. PhD thesis, Schriften des Institutes fir Instrumentelle Mathematik, Bonn, 1962.
W. Reisig. Petri nets. Springer Verlag, 1985.
J. Vautherin. Parallel specification with coloured Petri nets and algebraic data types. In Proc. of the 7th European Workshop on Application and Theory of Petri nets, pages 5-23, Oxford, England, jul. 1986.
Publicado
27/10/1993
Como Citar
RIBEIRO, Leila; EHRIG, Hartmut; PADBERG, Julia.
Formal Development of Concurrent Systems using Algebraic High-Level Nets and Transformations. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 7. , 1993, Rio de Janeiro/RJ.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1993
.
p. 1-16.
DOI: https://doi.org/10.5753/sbes.1993.24392.
