Blucher Mathematical Proceedings

Abril 2015, vol.1, num.1 - Congresso Nacional de Matemática Aplicada à Indústria
Artigo Completo - Open Access Idioma principal | Segundo principal

INDUSTRIAL PRODUCTION LINE MODELING AND REASONING BY PETRI NETS

INDUSTRIAL PRODUCTION LINE MODELING AND REASONING BY PETRI NETS

Costa, Vaston Gonçalves da; Vieira, Bruno Lopes; Souza, Leandro Rodrigues da Silva; Stoppa, Marcelo Henrique

Artigo Completo:

Petri Nets are a widely used formalism to execute and analyze concurrent procedures. It takes advantage of an intrinsic support to parallelism and concurrence as well as of the possibility of intuitive graphical interpretation. It can be used for modeling all the behavior of procedures and tracking resources flow. Petri-PDL is a logic formalism capable of making inferences on Petri Nets even in its concurrent dealings. Besides other works evolving reasoning in concurrent systems or those using Petri Nets, Petri-PDL is a decidable, sound and complete formalism that takes advantage of Petri Nets resources. The inspection method used in a VIN (vehicle identification number) validation does not meet the quality requirements demanded by the market. In some cases reported, the inspection is performed manually, by a visual checking operator, which exposes the company to the risk of commercializing a vehicle with differences between its VIN and the vehicle documentation. Due to the emotional factor and specially fatigue, the inspection should not be performed by a person. It requires a technological tool to assist on the transcription of the validating data to the chassis in order to avoid possible problems. This work presentes a new approach based on Petri Nets using Propositional Dynamic Logics to verify whether the model of a low cost system for validating the data transcribed to a chassis is correct – and therefore efficient.

Petri Nets are a widely used formalism to execute and analyze concurrent procedures. It takes advantage of an intrinsic support to parallelism and concurrence as well as of the possibility of intuitive graphical interpretation. It can be used for modeling all the behavior of procedures and tracking resources flow. Petri-PDL is a logic formalism capable of making inferences on Petri Nets even in its concurrent dealings. Besides other works evolving reasoning in concurrent systems or those using Petri Nets, Petri-PDL is a decidable, sound and complete formalism that takes advantage of Petri Nets resources. The inspection method used in a VIN (vehicle identification number) validation does not meet the quality requirements demanded by the market. In some cases reported, the inspection is performed manually, by a visual checking operator, which exposes the company to the risk of commercializing a vehicle with differences between its VIN and the vehicle documentation. Due to the emotional factor and specially fatigue, the inspection should not be performed by a person. It requires a technological tool to assist on the transcription of the validating data to the chassis in order to avoid possible problems. This work presentes a new approach based on Petri Nets using Propositional Dynamic Logics to verify whether the model of a low cost system for validating the data transcribed to a chassis is correct – and therefore efficient.

Download (PDF)

Palavras-chave:

DOI: 10.5151/mathpro-cnmai-0021

Referências bibliográficas
  • [1] Abrahamson, K. R. (1980), Decidability and Expressiveness of Logics of Processes, PhD thesis, Department of Computer Science, University of Washington.
  • [2] Alur, R., Courcoubetis, C. Andamp; Dill, D. (1990), Model-checking for real-time systems, in ‘Logic in Computer Science, 1990. LICS ’90, Proceedings., Fifth Annual IEEE Symposium on e’, pp. 414–425.
  • [3] Benevides, M., Haeusler, E. Andamp; Lopes, B. (2011), Propositional dynamic logic for petri nets, in ‘Annals of the 6th Workshop on Logical and Semantic Frameworks, with Applications’.
  • [4] Benevides, M. R. F. Andamp; Schechter, L. M. (2008), A propositional dynamic logic for CCS programs, in ‘Proceedings of the XV Workshop on Logic, Language’, Vol. 5110, pp. 83–97.
  • [5] Bertot, Y. Andamp; Castéran, P. (2004), Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. An EATCS Series, Springer.
  • [6] BRASIL (1988), ‘Resolução 691, de 05 de abril de 1988: identificação de veículos rodoviários’.
  • [7] Cecere, A. V. (2010), Estudo de medidas para a melhora da identificação veicular no Brasil, Master’s thesis, Escola Politécnica da Universidade de São Paulo, São Paulo.
  • [8] da Silva Souza, L. R., Oliveira, R. Andamp; Stoppa, M. H. (2014), Proposta de inspeção por câmera no processo de validação da gravação de chassi, in ‘Anais VIII CONEM - Congresso Nacional de Engrenharia Mecânica’, Uberlandia-MG - Brasil. To appear in august 2014.
  • [9] de Almeida, E. S. Andamp; Haeusler, E. H. (1999), ‘Proving properties in ordinary Petri Nets using LoRes logical language’,
  • [10] Petri Net Newsletter 57, 23–36.
  • [11] De Giacomo, G. Andamp; Massacci, F. (1998), ‘Combining deduction and model checking into tableaux and algorithms for Converse-PDL’, Information and Computation 160, 2000.
  • [12] Dijkstra, E. W. (1975), ‘Guarded commands, nondeterminacy and formal derivation of programs’, Commun. ACM
  • [13] 18(8), 453–457. URL: http://doi.acm.org/10.1145/360933.360975
  • [14] Fischer, M. J. Andamp; Ladner, R. E. (1979), ‘Propositional dynamic logic of regular programs’, Journal of Computer and System Sciences 18, 194–211. URL: http://www.sciencedirect.com/science/article/pii/0022000079900461
  • [15] Gabbar, H. (2006), Modern Formal Methods and Applications, Springer, New York.
  • [16] Goldblatt, R. (1992), ‘Parallel action: Concurrent dynamic logic with independent modalities’, Studia Logica 51, 551– 558.
  • [17] Hoare, C. (1972), ‘Proof of correctness of data representations’, Acta Informatica 1(4), 271–281. URL: http://dx.doi.org/10.1007/BF00289507
  • [18] Hou, Z. Andamp; Koh, T. (2003), ‘Robust edge detection’, Pattern Recognition 36(9), 2083 – 2091. Kernel and Subspace Methods for Computer Vision. URL: http://www.sciencedirect.com/science/article/pii/S0031320303000463
  • [19] Huth, M. Andamp; Ryan, M. (2004), Logic in Computer Science: Modelling and Reasoning About Systems, Cambridge Univer- sity Press.
  • [20] Lopes, B., Benevides, M. Andamp; Haeusler, E. H. (2014a), ‘Extending Propositional Dynamic Logic for petri nets’, Electronic Notes in Theoretical Computer Science 305, 67–83.
  • [21] Lopes, B., Benevides, M. Andamp; Haeusler, E. H. (2014b), ‘Propositional dynamic logic for petri nets’, Logic Journal of the IGPL .
  • [22] Lopes, B., Nalon, C., Hermann, E. Andamp; Dowek, G. (2014), A calculus for automatic verification of petri nets based on resolution and dynamic logics, in ‘17th Brazilian Logic Conference’, Laboratorio Nacional de Computação Científica (LNCC)- Petrópolis- Brazil.
  • [23] NASA (1997), Formal methods, specification and verification guidebook for the verification of software and computer systems. vol ii: A practitioner’s companion, Technical Report NASA-GB-001, NASA, Washington, DC.
  • [24] NASA (1998), Formal methods, specification and verification guidebook for the verification of software and computer systems. vol i: Planning and technology insertion, Technical Report NASA/TP-98-208193, NASA, Washington, DC. Owre, S., Rushby, J. Andamp; Shankar, N. (1992), Pvs: A prototype verification system, in D. Kapur, ed., ‘Automated Deduction—CADE-11’, Vol. 607 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 748–752.
  • [25] Rey, C. Andamp; Dugelay, J.-L. (2002), ‘A survey of watermarking algorithms for image authentication’, EURASIP J. Appl. Signal Process. 2002(1), 613–621. URL: http://dl.acm.org/citation.cfm?id=1283100.1283165
  • [26] Rushby, J. (1993), Formal methods and the certification of critical systems, Technical Report CSL-93-7, Computer Sci- ence Laboratory SRI International, Menlo Park, CA.
  • [27] Schmidt, R. A. (2004), ‘PDL-Tableau’. Accessed in February, 2013. URL: http://www.cs.man.ac.uk/ schmidt/pdl-tableau/
Como citar:

Costa, Vaston Gonçalves da; Vieira, Bruno Lopes; Souza, Leandro Rodrigues da Silva; Marcelo Stoppa; "INDUSTRIAL PRODUCTION LINE MODELING AND REASONING BY PETRI NETS", p-95-102. In: Anais do Congresso Nacional de Matemática Aplicada à Indústria [= Blucher Mathematical Proceedings, v.1, n.1]. São Paulo: Blucher, 2015.
ISSN soon, DOI 10.5151/mathpro-cnmai-0021

últimos 30 dias

87
downloads

335
visualizações

749
indexações