Fluid Survival Tool: A Model Checker for Hybrid Petri Nets

Björn Frits Postema, Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, Hamed Ghasemieh

Research output: Other contributionOther research output

Abstract

Recently, algorithms for model checking Stochastic Time Logic (STL) on Hybrid Petri nets with a single general one-shot transition (HPNG) have been introduced. This paper presents a tool for model checking HPNG models against STL formulas. A graphical user interface (GUI) not only helps to demonstrate and validate existing algorithms, it also eases use. From the output of the model checker, 2D and 3D plots can be generated. The extendable object-oriented tool has been developed using the Model-View-Controller and Facade patterns, Doxygen for documentation and Qt for GUI development written in C++.
Original languageEnglish
PublisherSpringer International Publishing AG
Number of pages5
Place of PublicationSwitzerland
ISBN (Print)978-3-319-05358-5
DOIs
Publication statusPublished - 17 Mar 2014
Externally publishedYes

Fingerprint

Model checking
Graphical user interfaces
Petri nets
Fluids
Facades
Stochastic models
Controllers

Keywords

  • EWI-24675
  • Hybrid Petri nets
  • IR-91064
  • Critical Infrastructures
  • METIS-305868
  • Model Checking

Cite this

Postema, B. F., Remke, A. K. I., Haverkort, B. R. H. M., & Ghasemieh, H. (2014, Mar 17). Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. Switzerland: Springer International Publishing AG. https://doi.org/10.1007/978-3-319-05359-2_18
Postema, Björn Frits ; Remke, Anne Katharina Ingrid ; Haverkort, Boudewijn R.H.M. ; Ghasemieh, Hamed. / Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. 2014. Switzerland : Springer International Publishing AG. 5 p.
@misc{d07d052d2037413e99983a8446aea481,
title = "Fluid Survival Tool: A Model Checker for Hybrid Petri Nets",
abstract = "Recently, algorithms for model checking Stochastic Time Logic (STL) on Hybrid Petri nets with a single general one-shot transition (HPNG) have been introduced. This paper presents a tool for model checking HPNG models against STL formulas. A graphical user interface (GUI) not only helps to demonstrate and validate existing algorithms, it also eases use. From the output of the model checker, 2D and 3D plots can be generated. The extendable object-oriented tool has been developed using the Model-View-Controller and Facade patterns, Doxygen for documentation and Qt for GUI development written in C++.",
keywords = "EWI-24675, Hybrid Petri nets, IR-91064, Critical Infrastructures, METIS-305868, Model Checking",
author = "Postema, {Bj{\"o}rn Frits} and Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.} and Hamed Ghasemieh",
note = "10.1007/978-3-319-05359-2_18",
year = "2014",
month = "3",
day = "17",
doi = "10.1007/978-3-319-05359-2_18",
language = "English",
isbn = "978-3-319-05358-5",
publisher = "Springer International Publishing AG",
address = "Switzerland",
type = "Other",

}

Postema, BF, Remke, AKI, Haverkort, BRHM & Ghasemieh, H 2014, Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. Springer International Publishing AG, Switzerland. https://doi.org/10.1007/978-3-319-05359-2_18

Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. / Postema, Björn Frits; Remke, Anne Katharina Ingrid; Haverkort, Boudewijn R.H.M.; Ghasemieh, Hamed.

5 p. Switzerland : Springer International Publishing AG. 2014, .

Research output: Other contributionOther research output

TY - GEN

T1 - Fluid Survival Tool: A Model Checker for Hybrid Petri Nets

AU - Postema, Björn Frits

AU - Remke, Anne Katharina Ingrid

AU - Haverkort, Boudewijn R.H.M.

AU - Ghasemieh, Hamed

N1 - 10.1007/978-3-319-05359-2_18

PY - 2014/3/17

Y1 - 2014/3/17

N2 - Recently, algorithms for model checking Stochastic Time Logic (STL) on Hybrid Petri nets with a single general one-shot transition (HPNG) have been introduced. This paper presents a tool for model checking HPNG models against STL formulas. A graphical user interface (GUI) not only helps to demonstrate and validate existing algorithms, it also eases use. From the output of the model checker, 2D and 3D plots can be generated. The extendable object-oriented tool has been developed using the Model-View-Controller and Facade patterns, Doxygen for documentation and Qt for GUI development written in C++.

AB - Recently, algorithms for model checking Stochastic Time Logic (STL) on Hybrid Petri nets with a single general one-shot transition (HPNG) have been introduced. This paper presents a tool for model checking HPNG models against STL formulas. A graphical user interface (GUI) not only helps to demonstrate and validate existing algorithms, it also eases use. From the output of the model checker, 2D and 3D plots can be generated. The extendable object-oriented tool has been developed using the Model-View-Controller and Facade patterns, Doxygen for documentation and Qt for GUI development written in C++.

KW - EWI-24675

KW - Hybrid Petri nets

KW - IR-91064

KW - Critical Infrastructures

KW - METIS-305868

KW - Model Checking

U2 - 10.1007/978-3-319-05359-2_18

DO - 10.1007/978-3-319-05359-2_18

M3 - Other contribution

SN - 978-3-319-05358-5

PB - Springer International Publishing AG

CY - Switzerland

ER -