Recently, algorithms for model checking Stochastic Timed Logic (STL) on Hybrid Petri nets with a general one-shot transition (HPNG) have been introduced. Currently, an actual tool is being developed for model checking HPNG models against STL formulas. A graphical user interface (GUI) helps to demonstrate and validate existing algorithms. Additionally, the tool gives insight into model checking by generating a Stochastic Timed Diagram. Moreover, from the output of the model checker 2D and 3D plots can be generated for the transient probability distributions to be in a state that fulfils a certain property. An extendable object-oriented tool design with a GUI has been carried out that uses the Model-View-Controller and Facade patterns, Doxygen for documentation and Qt for GUI development in C++. Furthermore, an approach for the general case of model checking formulas has been developed, which is based on generating and traversing the data structure of an Abstract Syntax Tree. Still, the general case offers more challenges for example with respect to nesting inside until formulas. Moreover, in cooperation with bachelor students from the mathematics department, the implementation and algorithms have been tested and validated with simulations on an elaborated case study of sewage water cleaning. Additionally, the number of continuous variables in this case study has been scaled in this master thesis to show the feasibility of the approach.