Incorporating Automatic Model Checking into GPenSIM

Reggie Davidrajuh; Bozena Skolud; Damian Krenczyk

doi:10.1007/978-3-030-27652-2_9

Incorporating Automatic Model Checking into GPenSIM

Reggie Davidrajuh
, Bozena Skolud
, Damian Krenczyk

Department of Engineering Processes Automation and Integrated Manufacturing Systems (RMT/RMT2)

University of Stavanger

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

1 Citation (Scopus)

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.

Original language	English
Title of host publication	Studies in Systems, Decision and Control
Publisher	Springer International Publishing
Pages	175-187
Number of pages	13
DOIs	https://doi.org/10.1007/978-3-030-27652-2_9
Publication status	Published - 2020

Publication series

Name	Studies in Systems, Decision and Control
Volume	241
ISSN (Print)	2198-4182
ISSN (Electronic)	2198-4190

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 9 Industry, Innovation, and Infrastructure

ASJC Scopus subject areas

Computer Science (miscellaneous)
Control and Systems Engineering
Automotive Engineering
Social Sciences (miscellaneous)
Economics, Econometrics and Finance (miscellaneous)
Control and Optimization
Decision Sciences (miscellaneous)

Access to Document

10.1007/978-3-030-27652-2_9

Cite this

@inbook{162d7b833665483b826e9c17e5defa86,

title = "Incorporating Automatic Model Checking into GPenSIM",

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.",

author = "Reggie Davidrajuh and Bozena Skolud and Damian Krenczyk",

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2020.",

year = "2020",

doi = "10.1007/978-3-030-27652-2\_9",

language = "English",

series = "Studies in Systems, Decision and Control",

publisher = "Springer International Publishing",

pages = "175--187",

booktitle = "Studies in Systems, Decision and Control",

address = "Switzerland",

}

TY - CHAP

T1 - Incorporating Automatic Model Checking into GPenSIM

AU - Davidrajuh, Reggie

AU - Skolud, Bozena

AU - Krenczyk, Damian

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85071464800

U2 - 10.1007/978-3-030-27652-2_9

DO - 10.1007/978-3-030-27652-2_9

M3 - Chapter

AN - SCOPUS:85071464800

T3 - Studies in Systems, Decision and Control

SP - 175

EP - 187

BT - Studies in Systems, Decision and Control

PB - Springer International Publishing

ER -

Incorporating Automatic Model Checking into GPenSIM

Abstract

Publication series

UN SDGs

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this