Análise qualitativa e quantitativa de WorkFlow nets utilizando Lógica Linear
Resumo
Este artigo apresenta um método para a análise qualitativa e quantitativa de WorkFlow nets baseada na construção de árvores de prova canônica da lógica linear. A análise qualitativa proposta neste trabalho diz respeito à prova do critério de corretude para WorkFlow nets denominado Soundness. Aanálise quantitativa basea-se no cálculo de intervalos de datas simbólicas para a execução de cada tarefa do processo de workflow modelado, possibilitando, assim, o planejamento dos recursos a serem utilizados em todas as tarefas do processo.
Referências
Girard, J.-Y. (1987). Linear logic. Theor. Comput. Sci., 50(1):1–102.
Girault, F. (1997). A logic for Petri nets, volume 31. Eddition Hermes.
Gochet, P. and Gribomont, P. (1990). Logique: méthodes pour l’informatique fondamentale, volume Vol 1. Hermès.
Julia, S. and Soares, M. S. (2003). Verification of real time uml specifications through a specialized inference mechanism based on a token player algorithm and the sequent calculus of linear logic. In Proceedings of the 15th European Simulation Symposium and Exhibition, pages 65–70, Delft, The Netherlands.
Khansa, W. (1997). R´eseaux de Petri p-temporels contribution `a l’ étude des systèmes à évenements discrets. PhD thesis, Université de Savoie, France.
Kotb, Y. T. and Badreddin, E. (2005). Synchronization among activities in a workflow using extended workflow petri nets. In CEC ’05: Proceedings of the Seventh IEEE International Conference on E-Commerce Technology, pages 548–551, Washington, DC, USA. IEEE Computer Society.
Lin, C. and Qu, Y. (2004). Temporal inference of workflow systems based on time petri nets: Quantitative and qualitative analysis. Int. J. Intell. Syst., 19(5):417–442.
Ling, S. and Schmidt, H. (2000). Time petri nets for workflow modelling and analysis. In Systems, Man, and Cybernetics, 2000 IEEE International Conference on, pages 3039–3044 vol.4.
Mantel, H. and Otten, J. (1999). lintap: A tableau prover for linear logic. In TABLEAUX ’99: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 217–231, London, UK. Springer-Verlag.
Marsan, M. A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G., Computing, P., Wiley, J., Almeida, V., Almeida, J., and Analysis, C. M. P. (1995). Modelling with generalized stochastic petri nets. In Series in Parallel Computing. Wiley.
Merlin, P. (1974). A study of recoverability of computer systems. PhD thesis, University of California, Irvine.
Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580.
Pradin-Chezalviel, B., Valette, R., and Kunzle, L. A. (1999). Scenario durations characterization of t-timed petri nets using linear logic. In PNPM ’99: Proceedings of the The 8th International Workshop on Petri Nets and Performance Models, page 208, Washington, DC, USA. IEEE Computer Society.
Ramchandani, C. (1974). Analysis of asynchronous concurrent systems by timed petri nets. Technical report, Cambridge, MA, USA.
Riviere, N., Valette, R., Pradin-Chezalviel, B., and Ups, I. A. . (2001). Reachability and temporal conflicts in t-time petri nets. In PNPM ’01: Proceedings of the 9th international Workshop on Petri Nets and Performance Models (PNPM’01), page 229, Washington, DC, USA. IEEE Computer Society.
Sifakis, J. (1977). Use of petri nets for performance evaluation. In Proceedings of the Third International Symposium on Measuring, Modelling and Evaluating Computer Systems, pages 75–93, Amsterdam, The Netherlands, The Netherlands. North-Holland Publishing Co.
Tammet, T. and Tammet, T. (1994). Proof strategies in linear logic. Journal of Automated Reasoning, 12:273–304.
Tamura, N. (1997). A linear logic prover (llprover). Disponível em: http://bach.istc.kobeu. ac.jp/llprover. Acesso em 26 Fev. 2009.
Valette, R. (1979). Analysis of Petri Nets by Stepwise Refinements. Journal of Computer and System Sciences, 18:35–46.
van der Aalst, W. M. P. (1998). The aplication of petri nets to workflow management. In The Journal of Circuits, Systems and Computers, pages 21–66.
van der Aalst, W. M. P. and van Hee, K. (2004). Workflow Management: Models, Methods, and Systems. The MIT Press.
Vilallonga, G., Riesco, D., Montejano, G., and Uzal, R. (2003). Petri nets with clocks for the analytical validation of business process. pages 11–25.
Girault, F. (1997). A logic for Petri nets, volume 31. Eddition Hermes.
Gochet, P. and Gribomont, P. (1990). Logique: méthodes pour l’informatique fondamentale, volume Vol 1. Hermès.
Julia, S. and Soares, M. S. (2003). Verification of real time uml specifications through a specialized inference mechanism based on a token player algorithm and the sequent calculus of linear logic. In Proceedings of the 15th European Simulation Symposium and Exhibition, pages 65–70, Delft, The Netherlands.
Khansa, W. (1997). R´eseaux de Petri p-temporels contribution `a l’ étude des systèmes à évenements discrets. PhD thesis, Université de Savoie, France.
Kotb, Y. T. and Badreddin, E. (2005). Synchronization among activities in a workflow using extended workflow petri nets. In CEC ’05: Proceedings of the Seventh IEEE International Conference on E-Commerce Technology, pages 548–551, Washington, DC, USA. IEEE Computer Society.
Lin, C. and Qu, Y. (2004). Temporal inference of workflow systems based on time petri nets: Quantitative and qualitative analysis. Int. J. Intell. Syst., 19(5):417–442.
Ling, S. and Schmidt, H. (2000). Time petri nets for workflow modelling and analysis. In Systems, Man, and Cybernetics, 2000 IEEE International Conference on, pages 3039–3044 vol.4.
Mantel, H. and Otten, J. (1999). lintap: A tableau prover for linear logic. In TABLEAUX ’99: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 217–231, London, UK. Springer-Verlag.
Marsan, M. A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G., Computing, P., Wiley, J., Almeida, V., Almeida, J., and Analysis, C. M. P. (1995). Modelling with generalized stochastic petri nets. In Series in Parallel Computing. Wiley.
Merlin, P. (1974). A study of recoverability of computer systems. PhD thesis, University of California, Irvine.
Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580.
Pradin-Chezalviel, B., Valette, R., and Kunzle, L. A. (1999). Scenario durations characterization of t-timed petri nets using linear logic. In PNPM ’99: Proceedings of the The 8th International Workshop on Petri Nets and Performance Models, page 208, Washington, DC, USA. IEEE Computer Society.
Ramchandani, C. (1974). Analysis of asynchronous concurrent systems by timed petri nets. Technical report, Cambridge, MA, USA.
Riviere, N., Valette, R., Pradin-Chezalviel, B., and Ups, I. A. . (2001). Reachability and temporal conflicts in t-time petri nets. In PNPM ’01: Proceedings of the 9th international Workshop on Petri Nets and Performance Models (PNPM’01), page 229, Washington, DC, USA. IEEE Computer Society.
Sifakis, J. (1977). Use of petri nets for performance evaluation. In Proceedings of the Third International Symposium on Measuring, Modelling and Evaluating Computer Systems, pages 75–93, Amsterdam, The Netherlands, The Netherlands. North-Holland Publishing Co.
Tammet, T. and Tammet, T. (1994). Proof strategies in linear logic. Journal of Automated Reasoning, 12:273–304.
Tamura, N. (1997). A linear logic prover (llprover). Disponível em: http://bach.istc.kobeu. ac.jp/llprover. Acesso em 26 Fev. 2009.
Valette, R. (1979). Analysis of Petri Nets by Stepwise Refinements. Journal of Computer and System Sciences, 18:35–46.
van der Aalst, W. M. P. (1998). The aplication of petri nets to workflow management. In The Journal of Circuits, Systems and Computers, pages 21–66.
van der Aalst, W. M. P. and van Hee, K. (2004). Workflow Management: Models, Methods, and Systems. The MIT Press.
Vilallonga, G., Riesco, D., Montejano, G., and Uzal, R. (2003). Petri nets with clocks for the analytical validation of business process. pages 11–25.
Publicado
20/05/2009
Como Citar
PASSOS, Lígia Maria Soares; JULIA, Stéphane.
Análise qualitativa e quantitativa de WorkFlow nets utilizando Lógica Linear. In: SIMPÓSIO BRASILEIRO DE SISTEMAS DE INFORMAÇÃO (SBSI), 5. , 2009, Brasília.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2009
.
p. 24-36.
DOI: https://doi.org/10.5753/sbsi.2009.6163.
