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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)
    94 Downloads (Pure)

    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 languageUndefined
    Title of host publication17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014
    Place of PublicationSwitzerland
    PublisherSpringer
    Pages255-259
    Number of pages5
    ISBN (Print)978-3-319-05358-5
    DOIs
    Publication statusPublished - 17 Mar 2014

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer International Publishing
    Volume8376
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    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). Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. In 17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014 (pp. 255-259). (Lecture Notes in Computer Science; Vol. 8376). Switzerland: Springer. 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. 17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014. Switzerland : Springer, 2014. pp. 255-259 (Lecture Notes in Computer Science).
    @inproceedings{d803a596bc6c4209bdba1fe077731fb7,
    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 = "Undefined",
    isbn = "978-3-319-05358-5",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "255--259",
    booktitle = "17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014",

    }

    Postema, BF, Remke, AKI, Haverkort, BRHM & Ghasemieh, H 2014, Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. in 17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014. Lecture Notes in Computer Science, vol. 8376, Springer, Switzerland, pp. 255-259. 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.

    17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014. Switzerland : Springer, 2014. p. 255-259 (Lecture Notes in Computer Science; Vol. 8376).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    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 - Conference contribution

    SN - 978-3-319-05358-5

    T3 - Lecture Notes in Computer Science

    SP - 255

    EP - 259

    BT - 17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014

    PB - Springer

    CY - Switzerland

    ER -

    Postema BF, Remke AKI, Haverkort BRHM, Ghasemieh H. Fluid Survival Tool: A Model Checker for Hybrid Petri Nets. In 17th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, MMB & DFT 2014. Switzerland: Springer. 2014. p. 255-259. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-05359-2_18