Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Cyclic Data Flows in Computers and Embedded Systems Read chapter Read first chapter

2020 | OriginalPaper | Chapter

Incorporating Automatic Model Checking into GPenSIM

Authors : Reggie Davidrajuh, Bozena Skolud, Damian Krenczyk

Published in: Modelling and Performance Analysis of Cyclic Systems

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Large-scale manufacturing systems involve hardware and software that are highly interconnected and complex. Unexpected failures in these systems can cause material damages and can risk human lives too. The definite way of avoiding unexpected failures is to make a model of the system and to perform model verification and validation on it. Petri nets are a highly effective way of modelling discrete-event systems. Model checking is the terminology that is used for model verification on Petri Nets. General-purpose Petri Net Simulator (GPenSIM) is a tool for modelling, simulation, performance evaluation, and control of discrete-event systems (GPenSIM: a general purpose Petri net simulator, http://​www.​davidrajuh.​net/​gpensim, 2019, [15]). GPenSIM is developed by one of the authors of this chapter. This chapter explores the potentials of incorporating the model checking functions to GPenSIM. In this chapter, the problem of model checking is presented. The chapter introduces Activity-Oriented Petri Nets (AOPN) and GPenSIM for model checking of cyclic production systems.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Max-Plus Algebraic Modelling of Cyclical Multi-assortment Manufacturing System
Literature
1.
Antunes, R., González, V.A., Walsh, K.: Identification of repetitive processes at steady- and unsteady-state: transfer function. In: Proceedings of the 23rd Annual Conference of the Int’l. Group for Lean Construction, Perth, Australia, 28–31 July 2017, pp. 793–802 (2017)
2.
Araki, T., Kasami, T.: Some decision problems related to the reachability problem for Petri nets. Theor. Comput. Sci. 3(1), 85–104 (1977)MathSciNetCrossRef
3.
Banaszak, Z.A., Polak, M.: Deadlock-free distributed control for repetitive flows. In: Sixth International Workshop on Discrete Event Systems, Proceedings, Zaragoza, Spain, 4 October 2002, pp. 273–278. IEEE (2002)
4.
Bocewicz, G., Nielsen, P., Banaszak, Z.A., Dang, V.Q.: Cyclic steady state refinement: multimodal processes perspective. In: Frick, J., Laugen, B.T. (eds.) Advances in Production Management Systems. Value Networks: Innovation, Technologies, and Management. APMS 2011, pp. 18–26. Springer, Berlin (2012)
5.
Bocewicz, G., Wójcik, R., Banaszak, Z.A., Pawlewski, P.: Multimodal processes rescheduling: cyclic steady states space approach. Math. Probl. Eng. 2013 (2013)
6.
Bocewicz, G., Janardhanan, M.N., Krenczyk, D., Banaszak, Z.: Traffic flow routing and scheduling in a food supply network. Ind. Manag. Data Syst. 117(9), 1972–1994 (2017)CrossRef
7.
Cameron, A., Stumptner, M., Nandagopal, N., Mayer, W., Mansell, T.: Rule-based peer-to-peer framework for decentralised real-time service oriented architectures. Sci. Comput. Program. 97, 202–234 (2015)CrossRef
8.
Chang, H.: A method of gameplay analysis by Petri net model simulation. J. Korea Game Soc. 15, 49–56 (2015)CrossRef
9.
Cheng, A., Christensen, S., Mortensen, K.: Model checking coloured Petri nets – exploiting strongly connected components. DAIMI Rep. Ser. 26, 519 (1997)
10.
Davidrajuh, R.: ACtivity-oriented Petri net for scheduling of resources. In: 2012 IEEE International Conference on Systems, Man, and Cybernetics (SMC), Seoul, South Korea, 14–17 October 2012, pp. 1201–1206. IEEE (2012)
11.
Davidrajuh, R.: Developing a Petri nets based real-time control simulator. Int. J. Simul. Syst. Sci. Technol. 12(3), 28–36 (2012)
12.
Davidrajuh, R.: Outperforming genetic algorithm with a brute force approach based on activity-oriented Petri nets. In: Graña, M., López-Guede, J., Etxaniz, O., Herrero, Á., Quintián, H., Corchado, E. (eds.) International Joint Conference SOCO-16-CISIS-16-ICEUTE-16. SOCO 2016, ICEUTE 2016, CISIS 2016, pp. 454–463 (2017)
13.
Davidrajuh, R.: Activity-oriented Petri nets: aligning real-world buffers with virtual places. Int. J. Simul. Syst. Sci. Technol. 18(3), 7.1–7.6 (2017)
14.
Davidrajuh, R.: Modeling Discrete-Event Systems with GPenSIM. Springer, Cham (2018)CrossRef
15.
16.
Hillion, H.P., Proth, J.M.: Performance evaluation of job-shop systems using timed event graphs. IEEE Trans. Autom. Control 34(1), 3–9 (1989)MathSciNetCrossRef
17.
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3–4), 213–254 (2007)CrossRef
18.
Jones, N.D., Landweber, L., Lien, Y.E.: Complexity of some problems in Petri nets. Theor. Comput. Sci. 4(3), 277–299 (1977)MathSciNetCrossRef
19.
Jyothi, S.D.: Scheduling flexible manufacturing system using Petri-nets and genetic algorithm. Technical report, Department of Aerospace Engineering, Indian Institute of Space Science and Technology, Thiruvananthapuram, India (2012)
20.
Korbaa, O., Camus, H., Gentina, J.C.: FMS cyclic scheduling with overlapping production cycles. In: Proceedings of the International Conference on Application and Theory of Petri Nets, Workshop on Manufacturing and Petri Nets, pp. 35–52 (1997)
21.
Korbaa, O., Camus, H., Gentina, J.C.: A new cyclic scheduling algorithm for flexible manufacturing systems. Int. J. Flex. Manuf. Syst. 14(2), 173–187 (2002)CrossRef
22.
Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef
23.
Mutarraf, U., Barkaoui, K., Li, Z., Wu, N., Qu, T.: Transformation of business process model and notation models onto Petri nets and their analysis. Adv. Mech. Eng. 10(12), 1–21 (2018)CrossRef
24.
Ohl, H., Camus, H., Castelain, E., Gentina, J.C.: A heuristic algorithm for the computation of cyclic schedules and the necessary WIP to obtain optimum cycle time. In: Proceedings of the Fourth International Conference on Computer Integrated Manufacturing and Automation Technology, Troy, NY, USA, 10–12 October 1994, pp. 339–344. IEEE (1994)
25.
Szpyrka, M.: Petri Nets in Modeling and Analysis of Concurrent Systems (in Polish). WNT, Warszawa (2008)MATH
26.
Valentin, C.: Modeling and analysis methods for a class of hybrid dynamic systems. In: Proceedings of ADPM ’94, Brussels, Belgium, pp. 221–226 (1994)
27.
Wójcik, R.: Constraint programming approach to designing conflict-free schedules for repetitive manufacturing processes. In: Cunha, P.F., Maropoulos, P.G. (eds.) Digital Enterprise Technology, pp. 267–274. Springer, Boston (2007)CrossRef
28.
Metadata
Title
Incorporating Automatic Model Checking into GPenSIM
Authors
Reggie Davidrajuh
Bozena Skolud
Damian Krenczyk
Copyright Year
2020
Book
Modelling and Performance Analysis of Cyclic Systems

Print ISBN: 978-3-030-27651-5

Electronic ISBN: 978-3-030-27652-2

Copyright Year: 2020

DOI
https://doi.org/10.1007/978-3-030-27652-2_9

Premium Partners

    Image Credits